Intro Equiv in Iso

[WenrongZou]

Add some levels to introduce Equiv in planet Iso.

[TentativeConvert]

It seems to me that plain refine works just as well as refine' here. Using refine ⟨f, g, ?_, ?_⟩ is much shorter than the previous line, and we don't need to remember variables for this.

[TentativeConvert]

Some remaining work to do here:

• Introduce fin_cases in some set theory planet rather than here.
• Make sure the notations ![…, …, …] and (t.1, t.2.1, t.2.2) needed in current L03 are actually known at this point of the game.
• Connect, at least in words, the curry content in L06 to the currying that's already happening in Epo L02 and all over Cantor.
• Possibly swap L03 and L06 here, so that L03 becomes the Boss level. L06 has a much shorter solution.
• Check that the theorems I deleted from L04 in 7528771 are not needed elsewhere.
• Update the docs (in particular: replace docu of refine' with docu of refine.)

[WenrongZou]

For the first two TODOs, I would like to introduce fin_cases and vector notation in the planet related to matrix. The reason why I choose refine' rather than refine is that this Preamble. I am happy to change this to refine.

[TentativeConvert]

For the first two TODOs, I would like to introduce fin_cases and vector notation in the planet related to matrix.

Ok, that sounds good!

The reason why I choose refine' rather than refine is that this leanprover-community/lean4game#46 (comment). I am happy to change this to refine.

I suspect we simply weren't aware of the refine ⟨f, g, ?_, ?_⟩ syntax. The last suggestion in that thread before "we settled on …" is from March 2023, when we were still struggling with the Lean3→Lean4 transition.

[WenrongZou]

Thanks for your comments! Let's use refine then. I think there are some refine's in other open PRs. I will replace them asap.