From 1c832170149b7903df6c49eb24590f058aa8c62a Mon Sep 17 00:00:00 2001
From: WenrongZou <141128015+WenrongZou@users.noreply.github.com>
Date: Tue, 18 Aug 2026 00:54:35 +0800
Subject: [PATCH 1/6] WIP

---
 Game/Doc/Definition.lean                      | 21 +++++++++
 Game/Doc/Tactic.lean                          | 29 ++++++++++--
 Game/Levels/Iso.lean                          |  8 ++--
 Game/Levels/Iso/L03_Equivalence.lean          | 44 +++++++++++++++++++
 ...ion.lean => L04_EquivalenceBijection.lean} | 15 ++++---
 Game/Levels/Iso/L05_BijectionEquivalence.lean | 25 +++++++++++
 ...06_CurryEquiv.lean => L06_CurryEquiv.lean} | 22 +++-------
 Game/Levels/Iso/X03_Equivalence.lean          | 41 -----------------
 Game/Levels/Iso/X05_BijectionEquivalence.lean | 26 -----------
 Game/Metadata/Tactic/simp_list.lean           |  6 +++
 10 files changed, 142 insertions(+), 95 deletions(-)
 create mode 100644 Game/Levels/Iso/L03_Equivalence.lean
 rename Game/Levels/Iso/{X04_EquivalenceBijection.lean => L04_EquivalenceBijection.lean} (54%)
 create mode 100644 Game/Levels/Iso/L05_BijectionEquivalence.lean
 rename Game/Levels/Iso/{X06_CurryEquiv.lean => L06_CurryEquiv.lean} (65%)
 delete mode 100644 Game/Levels/Iso/X03_Equivalence.lean
 delete mode 100644 Game/Levels/Iso/X05_BijectionEquivalence.lean

diff --git a/Game/Doc/Definition.lean b/Game/Doc/Definition.lean
index 8c93e558..16cc8f37 100644
--- a/Game/Doc/Definition.lean
+++ b/Game/Doc/Definition.lean
@@ -677,3 +677,24 @@ You can `rw` with `hasDerivAt_iff_tendsto_slope` (`rw [hasDerivAt_iff_tendsto_sl
 to expand this into the usual definition of the derivative in terms of the `slope` of f.
 -/
 DefinitionDoc HasDerivAt as "HasDerivAt" in "Function"
+
+/--
+Let `α, β` be two types, `α ≃ β` is the type of functions from `α → β` with a two-sided inverse.
+-/
+DefinitionDoc Equiv as "≃" in "Logic"
+
+/--
+For a function of two arguments `f : A → B → C`, `Function.uncurry f : A × B → C` is the
+function of a single pair-shaped argument with `uncurry f (a, b) = f a b`.
+
+Its inverse is `Function.curry`, see `Function.curry_uncurry` and `Function.uncurry_curry`.
+-/
+DefinitionDoc Function.uncurry as "Function.uncurry" in "Function"
+
+/--
+For a function of a single pair-shaped argument `f : A × B → C`, `Function.curry f : A → B → C`
+is the function of two arguments with `curry f a b = f (a, b)`.
+
+Its inverse is `Function.uncurry`, see `Function.curry_uncurry` and `Function.uncurry_curry`.
+-/
+DefinitionDoc Function.curry as "Function.curry" in "Function"
diff --git a/Game/Doc/Tactic.lean b/Game/Doc/Tactic.lean
index ac313439..bcab332e 100644
--- a/Game/Doc/Tactic.lean
+++ b/Game/Doc/Tactic.lean
@@ -157,7 +157,7 @@ x ∈ A ↔ x ∈ B
 -/
 TacticDoc ext
 
-/-
+/--
 `fin_cases i` führt eine Fallunterscheidung, wenn `i` ein endlicher Typ ist.
 
 ## Details
@@ -165,9 +165,8 @@ TacticDoc ext
 endlich dimensionalen Vektorräumen.
 
 In diesem Fall bewirkt `fin_cases i`, dass du komponentenweise arbeitest.
--
-TacticDoc fin_cases
 -/
+TacticDoc fin_cases
 
 /--
 Two mappings with the same range and domain are equal if
@@ -430,6 +429,30 @@ bei dieser Syntax.)
 TacticDoc refine'
 -/
 
+/--
+`refine' { .. }` splits a proof goal that asks for a *structure* — for example an
+equivalence `A ≃ B`, or an $R$-module — into one proof goal per field of that structure.
+
+Each field you leave as `_` becomes a new proof goal, while fields you fill in directly
+do not.
+
+## Example
+
+The proof goal `⊢ A ≃ B` is turned by
+```
+refine' { toFun := f, invFun := g, left_inv := _, right_inv := _ }
+```
+into the two proof goals `⊢ LeftInverse g f` and `⊢ RightInverse g f`.
+
+## Friends and relatives
+
+* `constructor` also splits a structure into one goal per field, but it does not let you
+  supply any of the fields yourself.
+* (*Remark*: Lean offers various nicer ways to do this, e.g. term mode or anonymous
+  constructors, but for the purposes of this game we stick to this syntax.)
+-/
+TacticDoc refine'
+
 /--
 The tactic `revert h` adds the assumption `h` as an implication premise to the proof goal:
 from `h : A` and `⊢ B`, we get `⊢ A → B`.
diff --git a/Game/Levels/Iso.lean b/Game/Levels/Iso.lean
index fb0de40a..c26b346e 100644
--- a/Game/Levels/Iso.lean
+++ b/Game/Levels/Iso.lean
@@ -1,9 +1,9 @@
 import Game.Levels.Iso.L01_Bijective
 import Game.Levels.Iso.L02_Inverse
--- import Game.Levels.Iso.X03_Equivalence
--- import Game.Levels.Iso.X04_EquivalenceBijection
--- import Game.Levels.Iso.X05_BijectionEquivalence
--- import Game.Levels.Iso.X06_CurryEquiv
+import Game.Levels.Iso.L03_Equivalence
+import Game.Levels.Iso.L04_EquivalenceBijection
+import Game.Levels.Iso.L05_BijectionEquivalence
+import Game.Levels.Iso.L06_CurryEquiv
 
 
 World "Iso"
diff --git a/Game/Levels/Iso/L03_Equivalence.lean b/Game/Levels/Iso/L03_Equivalence.lean
new file mode 100644
index 00000000..a2038b46
--- /dev/null
+++ b/Game/Levels/Iso/L03_Equivalence.lean
@@ -0,0 +1,44 @@
+import Game.Metadata
+
+World "Iso"
+Level 3
+
+/-
+Introduction
+"
+An equivalence `α : A ≃ B` between `A` and `B` consists of a pair of functions `f : A → B` and `g : B → A` such that `f ∘ g = id` and `g ∘ f = id`.
+
+`finTwoArrowEquiv` constructs an equivalence between functions from `Fin 2` to `A` and pairs of elements of `A`, that is an equivalence
+  ```
+  (Fin 2 → A) ≃ A × A
+
+  ```
+In this level you construct an equivalence between functions from `Fin 3` to `A` and triples of elements of `A`.
+"
+-/
+Introduction "Intro Iso L03"
+
+open Function
+
+Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
+  Hint "[Hint q7vk2] An equivalence `A ≃ B` is not a proposition but *data*: a map
+  `toFun : A → B`, a backwards map `invFun : B → A`, and two proofs `left_inv`, `right_inv`
+  saying that these undo each other.
+  Note that `![a, b, c] : Fin 3 → A` denotes the function sending `0, 1, 2` to `a, b, c`."
+  Hint (hidden := true) "[Hint m3bxs] Supply all four fields at once with
+  `refine' \{ toFun := _, invFun := _, left_inv := _, right_inv := _ }`."
+  refine' { toFun f := (f 0, f 1, f 2), invFun t := ![t.1, t.2.1, t.2.2], left_inv := _, right_inv := _ }
+  · simp [LeftInverse]
+    intro f
+    ext x
+    fin_cases x
+    · simp
+    · simp
+    · simp
+  · simp [RightInverse, LeftInverse]
+
+/- Already in the place introduce vector.-/
+NewTactic refine' fin_cases
+
+NewDefinition Equiv
+-- TODO: fin_cases should be in set-theory
diff --git a/Game/Levels/Iso/X04_EquivalenceBijection.lean b/Game/Levels/Iso/L04_EquivalenceBijection.lean
similarity index 54%
rename from Game/Levels/Iso/X04_EquivalenceBijection.lean
rename to Game/Levels/Iso/L04_EquivalenceBijection.lean
index 8c8d1b3d..f0e0052e 100644
--- a/Game/Levels/Iso/X04_EquivalenceBijection.lean
+++ b/Game/Levels/Iso/L04_EquivalenceBijection.lean
@@ -1,27 +1,30 @@
 import Game.Metadata
 
-
 World "Iso"
 Level 4
 
-Title "Bijection of Equivalence"
-
 /-
 Introduction
 "
 In this level you show that there every bijection gives rise to an equivalence.
 "
 -/
-Introduction "Intro Iso X04"
+Introduction "Intro Iso L04"
 
 open Function
 
-Statement Equiv.bijective {A B : Type} (f : A ≃ B) : Bijective f.toFun := by
+Statement {A B : Type} (f : A ≃ B) : Bijective f.toFun := by
   constructor
   · Branch
       intro a₁ a₂ h
-      simpa [congr_arg f.invFun] using h
+      simp [congr_arg f.invFun]
     apply Equiv.injective
   · apply RightInverse.surjective f.right_inv
 
+/---/
+TheoremDoc Function.RightInverse.surjective as "Function.RightInverse.surjective" in "Function"
+
+/---/
+TheoremDoc Equiv.injective as "Equiv.injective" in "Function"
+
 NewTheorem Function.RightInverse.surjective Equiv.injective
diff --git a/Game/Levels/Iso/L05_BijectionEquivalence.lean b/Game/Levels/Iso/L05_BijectionEquivalence.lean
new file mode 100644
index 00000000..4279b6a1
--- /dev/null
+++ b/Game/Levels/Iso/L05_BijectionEquivalence.lean
@@ -0,0 +1,25 @@
+import Game.Metadata
+
+World "Iso"
+Level 5
+
+/-
+Introduction
+"
+In this level you show that there every bijection gives rise to an equivalence.
+"
+-/
+Introduction "Intro Iso L05"
+
+noncomputable section
+
+open Function
+
+Statement {A B : Type} (f : A → B) (h : Bijective f) : A ≃ B := by
+  rw [bijective_iff_has_inverse] at h
+  choose g hg using h
+  constructor
+  · apply f
+  · apply g
+  · apply hg.1
+  · apply hg.2
diff --git a/Game/Levels/Iso/X06_CurryEquiv.lean b/Game/Levels/Iso/L06_CurryEquiv.lean
similarity index 65%
rename from Game/Levels/Iso/X06_CurryEquiv.lean
rename to Game/Levels/Iso/L06_CurryEquiv.lean
index 9e42dffa..b474cee5 100644
--- a/Game/Levels/Iso/X06_CurryEquiv.lean
+++ b/Game/Levels/Iso/L06_CurryEquiv.lean
@@ -5,8 +5,6 @@ universe u₁ u₂ u₃
 World "Iso"
 Level 6
 
-Title "Curry"
-
 /-
 Introduction
 "
@@ -16,20 +14,14 @@ This insight was first made explicit separately by Moses Ilyich Schönfinkel in
 
 "
 -/
-Introduction "Intro Iso X06"
+Introduction "Intro Iso L06"
 
 open Function
 
-Statement curry_equiv {A : Type u₁} {B : Type u₂} {C : Type u₃} :
+Statement {A : Type u₁} {B : Type u₂} {C : Type u₃} :
     (A × B → C) ≃ (A → B → C) := by
-  constructor
-  · -- Branch
-    --  exact curry
-    use fun f a b => f (a, b)
-  · -- Branch
-    --   exact uncurry
-    use fun f (a, b) => f a b
-  · apply uncurry_curry
-  · apply curry_uncurry
-
-NewTheorem Function.curry_uncurry Function.uncurry_curry
+  refine' {toFun := curry, invFun := uncurry, left_inv := _, right_inv := _}
+  · simp [LeftInverse]
+  · simp [LeftInverse, RightInverse]
+
+NewDefinition Function.curry Function.uncurry
diff --git a/Game/Levels/Iso/X03_Equivalence.lean b/Game/Levels/Iso/X03_Equivalence.lean
deleted file mode 100644
index a676c95e..00000000
--- a/Game/Levels/Iso/X03_Equivalence.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-import Game.Metadata
-
-
-World "Iso"
-Level 3
-
-Title "Triple"
-
-/-
-Introduction
-"
-An equivalence `α : A ≃ B` between `A` and `B` consists of a pair of functions `f : A → B` and `g : B → A` such that `f ∘ g = id` and `g ∘ f = id`.
-
-`finTwoArrowEquiv` constructs an equivalence between functions from `Fin 2` to `A` and pairs of elements of `A`, that is an equivalence
-  ```
-  (Fin 2 → A) ≃ A × A
-
-  ```
-In this level you construct an equivalence between functions from `Fin 3` to `A` and triples of elements of `A`.
-"
--/
-Introduction "Intro Iso X03"
-
-open Function
-
-Statement finThreeArrowEquiv {A : Type} : (Fin 3 → A) ≃ A × A × A := by
-  constructor
-  · exact fun f => (f 0, f 1, f 2)
-  · exact fun t => fun | 0 => t.1 | 1 => t.2.1 | 2 => t.2.2
-  · intro f
-    simp
-    ext x
-    fin_cases x
-    simp
-    simp
-    simp
-  · intro t
-    simp
-
-NewTactic fin_cases
--- TODO: fin_cases should be in set-theory
diff --git a/Game/Levels/Iso/X05_BijectionEquivalence.lean b/Game/Levels/Iso/X05_BijectionEquivalence.lean
deleted file mode 100644
index 356bb0e4..00000000
--- a/Game/Levels/Iso/X05_BijectionEquivalence.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Game.Metadata
-
-
-World "Iso"
-Level 5
-
-Title "Bijection of Equivalence"
-
-/-
-Introduction
-"
-In this level you show that there every bijection gives rise to an equivalence.
-"
--/
-Introduction "Intro Iso X05"
-
-open Function
-
-Statement Equiv.ofBijective {A B : Type} (f : A → B) (h : Bijective f) : A ≃ B := by
-  have := bijective_iff_has_inverse.mp h
-  choose g hg using this
-  constructor
-  · exact f
-  · exact g
-  · exact hg.left
-  · exact hg.right
diff --git a/Game/Metadata/Tactic/simp_list.lean b/Game/Metadata/Tactic/simp_list.lean
index 2546ffdb..674c157b 100644
--- a/Game/Metadata/Tactic/simp_list.lean
+++ b/Game/Metadata/Tactic/simp_list.lean
@@ -88,6 +88,12 @@ attribute [game_simp] Set.Finite.mem_toFinset Set.mem_setOf_eq lt_add_iff_pos_le
 -- Iso, L01_Bijective:
 attribute [game_simp] add_left_inj sub_add_cancel eq_self
 
+-- Iso, L03_Equivalence:
+attribute [game_simp] Fin.isValue Nat.succ_eq_add_one Nat.reduceAdd Fin.zero_eta Matrix.cons_val_zero eq_self Fin.mk_one Matrix.cons_val_one Fin.reduceFinMk Matrix.cons_val Prod.mk.eta implies_true
+
+-- Iso, L06_CurryEquiv:
+attribute [game_simp] Function.uncurry_curry eq_self implies_true Function.curry_uncurry
+
 -- Luna, L06_Icc__Icc_insert_succ_right:
 attribute [game_simp] Finset.mem_insert Finset.mem_Icc
 

From 91a6fbb4e4a51eb719cccde62c6bc308150d6564 Mon Sep 17 00:00:00 2001
From: WenrongZou <141128015+WenrongZou@users.noreply.github.com>
Date: Tue, 18 Aug 2026 19:21:35 +0800
Subject: [PATCH 2/6] add hints

---
 Game/Levels/Iso/L03_Equivalence.lean          | 15 ++++++++++-----
 Game/Levels/Iso/L04_EquivalenceBijection.lean |  7 ++++++-
 Game/Levels/Iso/L05_BijectionEquivalence.lean | 15 +++++++++++++--
 Game/Levels/Iso/L06_CurryEquiv.lean           |  2 ++
 4 files changed, 31 insertions(+), 8 deletions(-)

diff --git a/Game/Levels/Iso/L03_Equivalence.lean b/Game/Levels/Iso/L03_Equivalence.lean
index a2038b46..04cbb75f 100644
--- a/Game/Levels/Iso/L03_Equivalence.lean
+++ b/Game/Levels/Iso/L03_Equivalence.lean
@@ -24,18 +24,23 @@ Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
   Hint "[Hint q7vk2] An equivalence `A ≃ B` is not a proposition but *data*: a map
   `toFun : A → B`, a backwards map `invFun : B → A`, and two proofs `left_inv`, `right_inv`
   saying that these undo each other.
-  Note that `![a, b, c] : Fin 3 → A` denotes the function sending `0, 1, 2` to `a, b, c`."
+  Remember that `![a, b, c] : Fin 3 → A` denotes the function sending `0, 1, 2` to `a, b, c`."
   Hint (hidden := true) "[Hint m3bxs] Supply all four fields at once with
   `refine' \{ toFun := _, invFun := _, left_inv := _, right_inv := _ }`."
   refine' { toFun f := (f 0, f 1, f 2), invFun t := ![t.1, t.2.1, t.2.2], left_inv := _, right_inv := _ }
-  · simp [LeftInverse]
+  · Hint (hidden := true) "[Hint v8rq2] Unfold `LeftInverse` and simplify."
+    simp [LeftInverse]
     intro f
-    ext x
+    Hint (hidden := true) "[Hint k3mwt] Two functions are equal as soon as they agree on every argument — that is `funext`."
+    funext x
+    Hint (hidden := true) "[Hint dz6pf] Only three values of `x` are possible; `fin_cases x` treats them one by one."
     fin_cases x
+    · Hint (hidden := true) "[Hint n5hjb] Try `simp`."
+      simp
     · simp
     · simp
-    · simp
-  · simp [RightInverse, LeftInverse]
+  · Hint (hidden := true) "[Hint t7gks] Unfold `RightInverse` and `LeftInverse`, then simplify."
+    simp [RightInverse, LeftInverse]
 
 /- Already in the place introduce vector.-/
 NewTactic refine' fin_cases
diff --git a/Game/Levels/Iso/L04_EquivalenceBijection.lean b/Game/Levels/Iso/L04_EquivalenceBijection.lean
index f0e0052e..9eec5498 100644
--- a/Game/Levels/Iso/L04_EquivalenceBijection.lean
+++ b/Game/Levels/Iso/L04_EquivalenceBijection.lean
@@ -14,12 +14,17 @@ Introduction "Intro Iso L04"
 open Function
 
 Statement {A B : Type} (f : A ≃ B) : Bijective f.toFun := by
+  Hint "[Hint p4wnd] The underlying function of an equivalence is bijective."
   constructor
   · Branch
       intro a₁ a₂ h
       simp [congr_arg f.invFun]
+    Hint (hidden := true) "[Hint c9tzr] This is exactly `Equiv.injective`."
     apply Equiv.injective
-  · apply RightInverse.surjective f.right_inv
+  · Hint "[Hint x2fqm] A map that admits a right inverse is surjective, and `f.right_inv` says
+    that `f.invFun` is one."
+    Hint (hidden := true) "[Hint j6hlv] `Function.RightInverse.surjective` turns that into surjectivity."
+    apply RightInverse.surjective f.right_inv
 
 /---/
 TheoremDoc Function.RightInverse.surjective as "Function.RightInverse.surjective" in "Function"
diff --git a/Game/Levels/Iso/L05_BijectionEquivalence.lean b/Game/Levels/Iso/L05_BijectionEquivalence.lean
index 4279b6a1..5c661b30 100644
--- a/Game/Levels/Iso/L05_BijectionEquivalence.lean
+++ b/Game/Levels/Iso/L05_BijectionEquivalence.lean
@@ -16,10 +16,21 @@ noncomputable section
 open Function
 
 Statement {A B : Type} (f : A → B) (h : Bijective f) : A ≃ B := by
+  Hint "[Hint w6ktp] A map is bijective exactly when it has a two-sided inverse, i.e. some
+  `g : B → A` undoing `f` in both directions."
+  Hint (hidden := true) "[Hint r2xdn] Remember the theorem `bijective_iff_has_inverse` and rewrite `{h}` with it."
   rw [bijective_iff_has_inverse] at h
+  Hint (hidden := true) "[Hint f8vqc] Use `choose` to extract the function from `{h}`; `obtain` cannot, since the goal `A ≃ B` is data rather than a proposition."
   choose g hg using h
+  Branch
+    constructor
+    · apply f
+    · apply g
+    · apply hg.1
+    · apply hg.2
+  obtain ⟨hg₁, hg₂⟩ := hg
   constructor
   · apply f
   · apply g
-  · apply hg.1
-  · apply hg.2
+  · apply hg₁
+  · apply hg₂
diff --git a/Game/Levels/Iso/L06_CurryEquiv.lean b/Game/Levels/Iso/L06_CurryEquiv.lean
index b474cee5..a7c1770f 100644
--- a/Game/Levels/Iso/L06_CurryEquiv.lean
+++ b/Game/Levels/Iso/L06_CurryEquiv.lean
@@ -20,6 +20,8 @@ open Function
 
 Statement {A : Type u₁} {B : Type u₂} {C : Type u₃} :
     (A × B → C) ≃ (A → B → C) := by
+  Hint "[Hint h4nzq] `Function.curry` goes from `A × B → C` to `A → B → C`, and
+  `Function.uncurry` back again."
   refine' {toFun := curry, invFun := uncurry, left_inv := _, right_inv := _}
   · simp [LeftInverse]
   · simp [LeftInverse, RightInverse]

From 75287713707b40f5be4589c398c33a4a8211aa55 Mon Sep 17 00:00:00 2001
From: TentativeConvert <marcus.zibrowius@cantab.net>
Date: Thu, 10 Sep 2026 15:32:28 +0200
Subject: [PATCH 3/6] refine instead of refine';  use L02 in L04 (and not just
 in L05)

---
 Game/Levels/Iso/L02_Inverse.lean              | 15 +------
 Game/Levels/Iso/L03_Equivalence.lean          | 44 ++++++++++++-------
 Game/Levels/Iso/L04_EquivalenceBijection.lean | 27 ++++--------
 Game/Levels/Iso/L05_BijectionEquivalence.lean |  6 +--
 Game/Levels/Iso/L06_CurryEquiv.lean           | 14 +++---
 5 files changed, 49 insertions(+), 57 deletions(-)

diff --git a/Game/Levels/Iso/L02_Inverse.lean b/Game/Levels/Iso/L02_Inverse.lean
index 989d264c..ddbf9d3d 100644
--- a/Game/Levels/Iso/L02_Inverse.lean
+++ b/Game/Levels/Iso/L02_Inverse.lean
@@ -119,17 +119,4 @@ Statement bijective_iff_has_inverse {A B : Type} (f : A → B) :
 TheoremTab "Logic"
 DisabledTheorem Function.injective_iff_hasLeftInverse Function.surjective_iff_hasRightInverse
 
-/-
-Conclusion
-"
-Die Isosophen zeigen sich sehr zufrieden.
-
-**Robo**:  Können wir jetzt nochmal … kapseln?
-
-**Isosoph**:  Klar!  Aber immer schön der Reihe nach.
-Seit wir die Kapseln in beide Richtungen benutzen, häufen sich wieder die Unfälle.
-
-Robo fährt noch dreimal hin und zurück.  Dann fliegt ihr weiter.
-"
--/
-Conclusion "Conclusion Iso L02"
+Conclusion "Conclusion Iso L02 -- planet now continues"
diff --git a/Game/Levels/Iso/L03_Equivalence.lean b/Game/Levels/Iso/L03_Equivalence.lean
index 04cbb75f..1484c496 100644
--- a/Game/Levels/Iso/L03_Equivalence.lean
+++ b/Game/Levels/Iso/L03_Equivalence.lean
@@ -21,29 +21,43 @@ Introduction "Intro Iso L03"
 open Function
 
 Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
-  Hint "[Hint q7vk2] An equivalence `A ≃ B` is not a proposition but *data*: a map
-  `toFun : A → B`, a backwards map `invFun : B → A`, and two proofs `left_inv`, `right_inv`
-  saying that these undo each other.
-  Remember that `![a, b, c] : Fin 3 → A` denotes the function sending `0, 1, 2` to `a, b, c`."
-  Hint (hidden := true) "[Hint m3bxs] Supply all four fields at once with
-  `refine' \{ toFun := _, invFun := _, left_inv := _, right_inv := _ }`."
-  refine' { toFun f := (f 0, f 1, f 2), invFun t := ![t.1, t.2.1, t.2.2], left_inv := _, right_inv := _ }
-  · Hint (hidden := true) "[Hint v8rq2] Unfold `LeftInverse` and simplify."
-    simp [LeftInverse]
-    intro f
-    Hint (hidden := true) "[Hint k3mwt] Two functions are equal as soon as they agree on every argument — that is `funext`."
+  Hint "[Hint q7vk2] An equivalence `A ≃ B` is not a proposition but *data*:
+    a map `toFun : A → B`, a backwards map `invFun : B → A`,
+    and two proofs `left_inv`, `right_inv` saying that these undo each other.
+
+    Start by constructing a candidate for the forward map `f : (Fin 3 → A ) → A × A × A`.
+    Recall that a triple in `A × A × A` is written as `(a, (b, c))`, or simply `(a, b, c)`."
+  let f := fun (f : Fin 3 → A ) ↦ ((f 0, (f 1, f 2)) : A × A × A)
+  Hint "[Hint elxld] Now the inverse map:  Remember that the function `Fin 3 → A` sending
+    `0 ↦ a`, `1 ↦ b` and `2 ↦ c` is denoted `![a, b, c] : Fin 3 → A`."
+  Hint (hidden := true) "[Hint 9s56i] Also remember that `A × A × A` is really `A × (A × A)`, so
+    the components of `t : A × A × A` are called `t.1`, `t.2.1` and `t.2.2`."
+  let g := fun (t : A × A × A ) ↦ ![ t.1, t.2.1, t.2.2]
+  Hint "[Hint g0kn2] Now a new tactic: `refine ⟨{f}, {g}, ?_, ?_⟩` will partially fill in the data and
+    leave the remaining proofs as goals.
+    That is, it will set `toFun` to `{f}` and `invFun` to `{g}`,
+    and leave proofs of `left_inv` and `right_inv` as the remaining goals."
+  refine ⟨f, g, ?_, ?_⟩
+  · Hint (hidden := true) "[Hint v8rq2] Unfold `LeftInverse`, `{f}` and `{g}` and simplify."
+    simp [LeftInverse, f, g]
+    intro f'
+    Hint (hidden := true) "[Hint k3mwt] Two functions are equal as soon as they agree on every
+      argument — that is `funext`."
     funext x
-    Hint (hidden := true) "[Hint dz6pf] Only three values of `x` are possible; `fin_cases x` treats them one by one."
+    Hint (hidden := true) "[Hint dz6pf] Only three values of `x` are possible;
+      `fin_cases x` treats them one by one."
     fin_cases x
     · Hint (hidden := true) "[Hint n5hjb] Try `simp`."
       simp
     · simp
     · simp
-  · Hint (hidden := true) "[Hint t7gks] Unfold `RightInverse` and `LeftInverse`, then simplify."
-    simp [RightInverse, LeftInverse]
+  · Hint (hidden := true) "[Hint t7gks] Unfold `RightInverse`, `LeftInverse`, `{f}` and `{g}`,
+      then simplify."
+    simp [RightInverse, LeftInverse, f, g]
+
 
 /- Already in the place introduce vector.-/
-NewTactic refine' fin_cases
+NewTactic refine fin_cases
 
 NewDefinition Equiv
 -- TODO: fin_cases should be in set-theory
diff --git a/Game/Levels/Iso/L04_EquivalenceBijection.lean b/Game/Levels/Iso/L04_EquivalenceBijection.lean
index 9eec5498..23c65eca 100644
--- a/Game/Levels/Iso/L04_EquivalenceBijection.lean
+++ b/Game/Levels/Iso/L04_EquivalenceBijection.lean
@@ -11,25 +11,14 @@ In this level you show that there every bijection gives rise to an equivalence.
 -/
 Introduction "Intro Iso L04"
 
-open Function
+open Function FullGrind
 
 Statement {A B : Type} (f : A ≃ B) : Bijective f.toFun := by
-  Hint "[Hint p4wnd] The underlying function of an equivalence is bijective."
+  Hint "[Hint p4wnd] Given an equivalence `f`, you can access it's components
+    and the relevant proofs with `f.toFun`, `f.invFun`, `f.left_inv` and `f.right_inv`."
+  Hint (hidden := true) "[Hint 6my94] Remember we proved `bijective_iff_has_inverse` a moment ago."
+  rw [bijective_iff_has_inverse]
+  use f.invFun
   constructor
-  · Branch
-      intro a₁ a₂ h
-      simp [congr_arg f.invFun]
-    Hint (hidden := true) "[Hint c9tzr] This is exactly `Equiv.injective`."
-    apply Equiv.injective
-  · Hint "[Hint x2fqm] A map that admits a right inverse is surjective, and `f.right_inv` says
-    that `f.invFun` is one."
-    Hint (hidden := true) "[Hint j6hlv] `Function.RightInverse.surjective` turns that into surjectivity."
-    apply RightInverse.surjective f.right_inv
-
-/---/
-TheoremDoc Function.RightInverse.surjective as "Function.RightInverse.surjective" in "Function"
-
-/---/
-TheoremDoc Equiv.injective as "Equiv.injective" in "Function"
-
-NewTheorem Function.RightInverse.surjective Equiv.injective
+  apply f.left_inv
+  apply f.right_inv
diff --git a/Game/Levels/Iso/L05_BijectionEquivalence.lean b/Game/Levels/Iso/L05_BijectionEquivalence.lean
index 5c661b30..31ddcb1a 100644
--- a/Game/Levels/Iso/L05_BijectionEquivalence.lean
+++ b/Game/Levels/Iso/L05_BijectionEquivalence.lean
@@ -20,7 +20,7 @@ Statement {A B : Type} (f : A → B) (h : Bijective f) : A ≃ B := by
   `g : B → A` undoing `f` in both directions."
   Hint (hidden := true) "[Hint r2xdn] Remember the theorem `bijective_iff_has_inverse` and rewrite `{h}` with it."
   rw [bijective_iff_has_inverse] at h
-  Hint (hidden := true) "[Hint f8vqc] Use `choose` to extract the function from `{h}`; `obtain` cannot, since the goal `A ≃ B` is data rather than a proposition."
+  Hint (hidden := true) "[Hint f8vqc] Use `choose` to extract the function from `{h}`"
   choose g hg using h
   Branch
     constructor
@@ -29,8 +29,6 @@ Statement {A B : Type} (f : A → B) (h : Bijective f) : A ≃ B := by
     · apply hg.1
     · apply hg.2
   obtain ⟨hg₁, hg₂⟩ := hg
-  constructor
-  · apply f
-  · apply g
+  refine ⟨f, g, ?_, ?_⟩
   · apply hg₁
   · apply hg₂
diff --git a/Game/Levels/Iso/L06_CurryEquiv.lean b/Game/Levels/Iso/L06_CurryEquiv.lean
index a7c1770f..a8734688 100644
--- a/Game/Levels/Iso/L06_CurryEquiv.lean
+++ b/Game/Levels/Iso/L06_CurryEquiv.lean
@@ -8,10 +8,14 @@ Level 6
 /-
 Introduction
 "
-In this level, you will learn about currying. Currying is the process of transforming a function that takes multiple arguments into a function that takes one argument and returns another function that takes the next argument, and so on, until all arguments have been supplied. This is useful because it allows you to partially apply a function, which means you can supply some of the arguments now and the rest later.
-
-This insight was first made explicit separately by Moses Ilyich Schönfinkel in the 19th century and later in the 20th century by Haskell Curry.
-
+In this level, you will learn about currying. Currying is the process of transforming a function
+that takes multiple arguments into a function that takes one argument and returns another function
+that takes the next argument, and so on, until all arguments have been supplied. This is useful
+because it allows you to partially apply a function, which means you can supply some of the
+arguments now and the rest later.
+
+This insight was first made explicit separately by Moses Ilyich Schönfinkel in the 19th
+century and later in the 20th century by Haskell Curry.
 "
 -/
 Introduction "Intro Iso L06"
@@ -22,7 +26,7 @@ Statement {A : Type u₁} {B : Type u₂} {C : Type u₃} :
     (A × B → C) ≃ (A → B → C) := by
   Hint "[Hint h4nzq] `Function.curry` goes from `A × B → C` to `A → B → C`, and
   `Function.uncurry` back again."
-  refine' {toFun := curry, invFun := uncurry, left_inv := _, right_inv := _}
+  refine ⟨curry, uncurry, ?_, ?_ ⟩
   · simp [LeftInverse]
   · simp [LeftInverse, RightInverse]
 

From ecee1c459f2d1626ea23792e8d30c2e338d98579 Mon Sep 17 00:00:00 2001
From: WenrongZou <141128015+WenrongZou@users.noreply.github.com>
Date: Thu, 10 Sep 2026 23:27:30 +0800
Subject: [PATCH 4/6] comment change 1

---
 Game/Doc/Tactic.lean                          | 22 ++++++++-----------
 Game/Levels/Iso.lean                          |  4 ++--
 ...06_CurryEquiv.lean => L03_CurryEquiv.lean} | 17 +++++++++-----
 ..._Equivalence.lean => L06_Equivalence.lean} | 21 ++++++------------
 4 files changed, 29 insertions(+), 35 deletions(-)
 rename Game/Levels/Iso/{L06_CurryEquiv.lean => L03_CurryEquiv.lean} (64%)
 rename Game/Levels/Iso/{L03_Equivalence.lean => L06_Equivalence.lean} (74%)

diff --git a/Game/Doc/Tactic.lean b/Game/Doc/Tactic.lean
index bcab332e..4842869e 100644
--- a/Game/Doc/Tactic.lean
+++ b/Game/Doc/Tactic.lean
@@ -430,28 +430,24 @@ TacticDoc refine'
 -/
 
 /--
-`refine' { .. }` splits a proof goal that asks for a *structure* — for example an
-equivalence `A ≃ B`, or an $R$-module — into one proof goal per field of that structure.
+`refine ⟨..⟩` splits a proof goal that asks for a *structure* — for example an
+equivalence `A ≃ B` — into one proof goal per field that you do not fill in yourself.
 
-Each field you leave as `_` becomes a new proof goal, while fields you fill in directly
+Inside the anonymous constructor `⟨..⟩` you list the fields of the structure in order.
+Each field you write as `?_` becomes a new proof goal, the fields you supply directly
 do not.
 
 ## Example
 
-The proof goal `⊢ A ≃ B` is turned by
+An equivalence `A ≃ B` consists of a map `toFun : A → B`, a backwards map `invFun : B → A`,
+and two proofs `left_inv` and `right_inv` that these undo each other.
+So for given maps `f : A → B` and `g : B → A`, the proof goal `⊢ A ≃ B` is turned by
 ```
-refine' { toFun := f, invFun := g, left_inv := _, right_inv := _ }
+refine ⟨f, g, ?_, ?_⟩
 ```
 into the two proof goals `⊢ LeftInverse g f` and `⊢ RightInverse g f`.
-
-## Friends and relatives
-
-* `constructor` also splits a structure into one goal per field, but it does not let you
-  supply any of the fields yourself.
-* (*Remark*: Lean offers various nicer ways to do this, e.g. term mode or anonymous
-  constructors, but for the purposes of this game we stick to this syntax.)
 -/
-TacticDoc refine'
+TacticDoc refine
 
 /--
 The tactic `revert h` adds the assumption `h` as an implication premise to the proof goal:
diff --git a/Game/Levels/Iso.lean b/Game/Levels/Iso.lean
index c26b346e..a9a81240 100644
--- a/Game/Levels/Iso.lean
+++ b/Game/Levels/Iso.lean
@@ -1,9 +1,9 @@
 import Game.Levels.Iso.L01_Bijective
 import Game.Levels.Iso.L02_Inverse
-import Game.Levels.Iso.L03_Equivalence
+import Game.Levels.Iso.L03_CurryEquiv
 import Game.Levels.Iso.L04_EquivalenceBijection
 import Game.Levels.Iso.L05_BijectionEquivalence
-import Game.Levels.Iso.L06_CurryEquiv
+import Game.Levels.Iso.L06_Equivalence
 
 
 World "Iso"
diff --git a/Game/Levels/Iso/L06_CurryEquiv.lean b/Game/Levels/Iso/L03_CurryEquiv.lean
similarity index 64%
rename from Game/Levels/Iso/L06_CurryEquiv.lean
rename to Game/Levels/Iso/L03_CurryEquiv.lean
index a8734688..1d61c074 100644
--- a/Game/Levels/Iso/L06_CurryEquiv.lean
+++ b/Game/Levels/Iso/L03_CurryEquiv.lean
@@ -1,9 +1,7 @@
 import Game.Metadata
 
-universe u₁ u₂ u₃
-
 World "Iso"
-Level 6
+Level 3
 
 /-
 Introduction
@@ -18,16 +16,23 @@ This insight was first made explicit separately by Moses Ilyich Schönfinkel in
 century and later in the 20th century by Haskell Curry.
 "
 -/
-Introduction "Intro Iso L06"
+Introduction "Intro Iso L03"
 
 open Function
 
-Statement {A : Type u₁} {B : Type u₂} {C : Type u₃} :
+Statement {A B C : Type*} :
     (A × B → C) ≃ (A → B → C) := by
+  Hint "[Hint w3knf] An equivalence `A ≃ B` is not a proposition but *data*:
+    a map `toFun : A → B`, a backwards map `invFun : B → A`,
+    and two proofs `left_inv`, `right_inv` saying that these undo each other."
   Hint "[Hint h4nzq] `Function.curry` goes from `A × B → C` to `A → B → C`, and
   `Function.uncurry` back again."
+  Hint (hidden := true) "[Hint p7ubs] A new tactic: `refine ⟨curry, uncurry, ?_, ?_⟩` fills in the
+    two maps and leaves the two proofs as goals."
   refine ⟨curry, uncurry, ?_, ?_ ⟩
   · simp [LeftInverse]
   · simp [LeftInverse, RightInverse]
 
-NewDefinition Function.curry Function.uncurry
+NewTactic refine
+
+NewDefinition Equiv Function.curry Function.uncurry
diff --git a/Game/Levels/Iso/L03_Equivalence.lean b/Game/Levels/Iso/L06_Equivalence.lean
similarity index 74%
rename from Game/Levels/Iso/L03_Equivalence.lean
rename to Game/Levels/Iso/L06_Equivalence.lean
index 1484c496..b5ab7720 100644
--- a/Game/Levels/Iso/L03_Equivalence.lean
+++ b/Game/Levels/Iso/L06_Equivalence.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 
 World "Iso"
-Level 3
+Level 6
 
 /-
 Introduction
@@ -16,27 +16,22 @@ An equivalence `α : A ≃ B` between `A` and `B` consists of a pair of function
 In this level you construct an equivalence between functions from `Fin 3` to `A` and triples of elements of `A`.
 "
 -/
-Introduction "Intro Iso L03"
+Introduction "Intro Iso L06"
 
 open Function
 
 Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
-  Hint "[Hint q7vk2] An equivalence `A ≃ B` is not a proposition but *data*:
-    a map `toFun : A → B`, a backwards map `invFun : B → A`,
-    and two proofs `left_inv`, `right_inv` saying that these undo each other.
-
+  Hint "[Hint q7vk2] Build the equivalence by hand, as you did for currying.
     Start by constructing a candidate for the forward map `f : (Fin 3 → A ) → A × A × A`.
     Recall that a triple in `A × A × A` is written as `(a, (b, c))`, or simply `(a, b, c)`."
-  let f := fun (f : Fin 3 → A ) ↦ ((f 0, (f 1, f 2)) : A × A × A)
+  let f := fun (f : Fin 3 → A) ↦ ((f 0, (f 1, f 2)) : A × A × A)
   Hint "[Hint elxld] Now the inverse map:  Remember that the function `Fin 3 → A` sending
     `0 ↦ a`, `1 ↦ b` and `2 ↦ c` is denoted `![a, b, c] : Fin 3 → A`."
   Hint (hidden := true) "[Hint 9s56i] Also remember that `A × A × A` is really `A × (A × A)`, so
     the components of `t : A × A × A` are called `t.1`, `t.2.1` and `t.2.2`."
   let g := fun (t : A × A × A ) ↦ ![ t.1, t.2.1, t.2.2]
-  Hint "[Hint g0kn2] Now a new tactic: `refine ⟨{f}, {g}, ?_, ?_⟩` will partially fill in the data and
-    leave the remaining proofs as goals.
-    That is, it will set `toFun` to `{f}` and `invFun` to `{g}`,
-    and leave proofs of `left_inv` and `right_inv` as the remaining goals."
+  Hint (hidden := true) "[Hint g0kn2] `refine ⟨{f}, {g}, ?_, ?_⟩` sets `toFun` to `{f}` and
+    `invFun` to `{g}`, leaving the proofs of `left_inv` and `right_inv` as goals."
   refine ⟨f, g, ?_, ?_⟩
   · Hint (hidden := true) "[Hint v8rq2] Unfold `LeftInverse`, `{f}` and `{g}` and simplify."
     simp [LeftInverse, f, g]
@@ -57,7 +52,5 @@ Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
 
 
 /- Already in the place introduce vector.-/
-NewTactic refine fin_cases
-
-NewDefinition Equiv
+NewTactic fin_cases
 -- TODO: fin_cases should be in set-theory

From 8369cd9f553e5ce889d9d7603a4ec95650ee29e9 Mon Sep 17 00:00:00 2001
From: WenrongZou <141128015+WenrongZou@users.noreply.github.com>
Date: Fri, 11 Sep 2026 12:15:18 +0800
Subject: [PATCH 5/6] update a hint

---
 Game/Doc/Tactic.lean                | 2 +-
 Game/Levels/Iso/L03_CurryEquiv.lean | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Game/Doc/Tactic.lean b/Game/Doc/Tactic.lean
index 4842869e..8929ce15 100644
--- a/Game/Doc/Tactic.lean
+++ b/Game/Doc/Tactic.lean
@@ -430,7 +430,7 @@ TacticDoc refine'
 -/
 
 /--
-`refine ⟨..⟩` splits a proof goal that asks for a *structure* — for example an
+Tactic `refine ⟨..⟩` splits a proof goal that asks for a *structure* — for example an
 equivalence `A ≃ B` — into one proof goal per field that you do not fill in yourself.
 
 Inside the anonymous constructor `⟨..⟩` you list the fields of the structure in order.
diff --git a/Game/Levels/Iso/L03_CurryEquiv.lean b/Game/Levels/Iso/L03_CurryEquiv.lean
index 1d61c074..4a9a8fb1 100644
--- a/Game/Levels/Iso/L03_CurryEquiv.lean
+++ b/Game/Levels/Iso/L03_CurryEquiv.lean
@@ -22,6 +22,9 @@ open Function
 
 Statement {A B C : Type*} :
     (A × B → C) ≃ (A → B → C) := by
+  Hint "[Hint m2rqd] You have been reading `ℕ → A → B` as a map into a function space since
+    Epo, and Cantor's diagonal argument feeds two arguments into `f : A → A → Y` the same way.
+    Such a function of two arguments is really a function on the product. "
   Hint "[Hint w3knf] An equivalence `A ≃ B` is not a proposition but *data*:
     a map `toFun : A → B`, a backwards map `invFun : B → A`,
     and two proofs `left_inv`, `right_inv` saying that these undo each other."

From 7fb58583960e40db558ade1788f94b7529547cd5 Mon Sep 17 00:00:00 2001
From: TentativeConvert <marcus.zibrowius@cantab.net>
Date: Wed, 23 Sep 2026 11:18:57 +0200
Subject: [PATCH 6/6] review

---
 Game/Doc/Definition.lean                      | 13 +++++++++++--
 Game/Levels/Iso/L03_CurryEquiv.lean           | 19 +++++++++++--------
 Game/Levels/Iso/L04_EquivalenceBijection.lean |  9 ++++++---
 Game/Levels/Iso/L06_Equivalence.lean          | 14 ++++++++------
 4 files changed, 36 insertions(+), 19 deletions(-)

diff --git a/Game/Doc/Definition.lean b/Game/Doc/Definition.lean
index 16cc8f37..b5ec5ae1 100644
--- a/Game/Doc/Definition.lean
+++ b/Game/Doc/Definition.lean
@@ -679,9 +679,18 @@ to expand this into the usual definition of the derivative in terms of the `slop
 DefinitionDoc HasDerivAt as "HasDerivAt" in "Function"
 
 /--
-Let `α, β` be two types, `α ≃ β` is the type of functions from `α → β` with a two-sided inverse.
+For types `α` and `β`, `α ≃ β` or (`Equiv α β`) is the type of functions from `α → β` with a
+two-sided inverse.  A term `f : α ≃ β` has four components:
+a map `f.toFun` (`f.toFun : α → β`), a map `f.invFun` (`f.invFun : β → α`),
+and proofs `left_inv` and `right_inv` that these are mutually inverse.
+
+The inverse equivalence is called `f.symm` (`f.symm : β ≃ α`).
+
+You don't usually have to write out f.toFun to refer to the map `α → β` – you can use coercion and
+simply write f.
+Similarly, the recommended spelling of the map `β → α` is f.symm.
 -/
-DefinitionDoc Equiv as "≃" in "Logic"
+DefinitionDoc Equiv as "≃" in "Function"
 
 /--
 For a function of two arguments `f : A → B → C`, `Function.uncurry f : A × B → C` is the
diff --git a/Game/Levels/Iso/L03_CurryEquiv.lean b/Game/Levels/Iso/L03_CurryEquiv.lean
index 4a9a8fb1..aa2045ba 100644
--- a/Game/Levels/Iso/L03_CurryEquiv.lean
+++ b/Game/Levels/Iso/L03_CurryEquiv.lean
@@ -24,14 +24,17 @@ Statement {A B C : Type*} :
     (A × B → C) ≃ (A → B → C) := by
   Hint "[Hint m2rqd] You have been reading `ℕ → A → B` as a map into a function space since
     Epo, and Cantor's diagonal argument feeds two arguments into `f : A → A → Y` the same way.
-    Such a function of two arguments is really a function on the product. "
-  Hint "[Hint w3knf] An equivalence `A ≃ B` is not a proposition but *data*:
-    a map `toFun : A → B`, a backwards map `invFun : B → A`,
-    and two proofs `left_inv`, `right_inv` saying that these undo each other."
-  Hint "[Hint h4nzq] `Function.curry` goes from `A × B → C` to `A → B → C`, and
-  `Function.uncurry` back again."
-  Hint (hidden := true) "[Hint p7ubs] A new tactic: `refine ⟨curry, uncurry, ?_, ?_⟩` fills in the
-    two maps and leaves the two proofs as goals."
+    Such a function of two arguments is really a function on the product.
+
+    An equivalence `A ≃ B` is not a proposition but *data*:
+    a map `A → B` (`toFun : A → B`), a backwards map `B → A` (`invFun : B → A`),
+    and two proofs `left_inv` and `right_inv` saying that these are mutually inverse.
+
+    To construct it, use a new tactic: `refine`. `refine ⟨f, g, ?_, ?_⟩` fills in the
+    two maps with `f` and `g` respectively, and leaves the two proofs as goals.
+
+    `Function.curry` goes from `A × B → C` to `A → B → C`, and
+    `Function.uncurry` back again."
   refine ⟨curry, uncurry, ?_, ?_ ⟩
   · simp [LeftInverse]
   · simp [LeftInverse, RightInverse]
diff --git a/Game/Levels/Iso/L04_EquivalenceBijection.lean b/Game/Levels/Iso/L04_EquivalenceBijection.lean
index 23c65eca..4d23a37e 100644
--- a/Game/Levels/Iso/L04_EquivalenceBijection.lean
+++ b/Game/Levels/Iso/L04_EquivalenceBijection.lean
@@ -14,11 +14,14 @@ Introduction "Intro Iso L04"
 open Function FullGrind
 
 Statement {A B : Type} (f : A ≃ B) : Bijective f.toFun := by
-  Hint "[Hint p4wnd] Given an equivalence `f`, you can access it's components
-    and the relevant proofs with `f.toFun`, `f.invFun`, `f.left_inv` and `f.right_inv`."
+  Hint "[Hint p4wnd] Given an equivalence `f`, you can access its components
+    and the relevant proofs with `f.toFun`, `f.invFun`, `f.left_inv` and `f.right_inv`.
+    However, it's recommended to rely on coercion and use
+    - f in place of f.toFun, and
+    - `f.symm` in place of f.invFun"
   Hint (hidden := true) "[Hint 6my94] Remember we proved `bijective_iff_has_inverse` a moment ago."
   rw [bijective_iff_has_inverse]
-  use f.invFun
+  use f.symm
   constructor
   apply f.left_inv
   apply f.right_inv
diff --git a/Game/Levels/Iso/L06_Equivalence.lean b/Game/Levels/Iso/L06_Equivalence.lean
index b5ab7720..e71d9cc9 100644
--- a/Game/Levels/Iso/L06_Equivalence.lean
+++ b/Game/Levels/Iso/L06_Equivalence.lean
@@ -21,11 +21,13 @@ Introduction "Intro Iso L06"
 open Function
 
 Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
-  Hint "[Hint q7vk2] Build the equivalence by hand, as you did for currying.
-    Start by constructing a candidate for the forward map `f : (Fin 3 → A ) → A × A × A`.
-    Recall that a triple in `A × A × A` is written as `(a, (b, c))`, or simply `(a, b, c)`."
-  let f := fun (f : Fin 3 → A) ↦ ((f 0, (f 1, f 2)) : A × A × A)
-  Hint "[Hint elxld] Now the inverse map:  Remember that the function `Fin 3 → A` sending
+  Hint "[Hint q7vk2] Here you need to build the equivalence by hand.
+    Start by constructing a candidate for the forward map `f : (Fin 3 → A ) → A × A × A`."
+  Hint (hidden := true) "[Hint plisw] Recall that a triple in `A × A × A` is written as
+    `(a, (b, c))`, or simply `(a, b, c)`."
+  let f := fun (v : Fin 3 → A) ↦ ((v 0, (v 1, v 2)) : A × A × A)
+  Hint "[Hint elxld] Now the inverse map."
+  Hint (hidden := true) "[Hint kkivj] Remember that the function `Fin 3 → A` sending
     `0 ↦ a`, `1 ↦ b` and `2 ↦ c` is denoted `![a, b, c] : Fin 3 → A`."
   Hint (hidden := true) "[Hint 9s56i] Also remember that `A × A × A` is really `A × (A × A)`, so
     the components of `t : A × A × A` are called `t.1`, `t.2.1` and `t.2.2`."
@@ -52,5 +54,5 @@ Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
 
 
 /- Already in the place introduce vector.-/
-NewTactic fin_cases
+-- NewTactic fin_cases
 -- TODO: fin_cases should be in set-theory