Intro Equiv in Iso

Game/Doc/Definition.lean

@@ -677,3 +677,33 @@ 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"
+
+/--
+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 "Function"
+
+/--
+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"

Game/Doc/Tactic.lean

@@ -157,17 +157,16 @@ x ∈ A ↔ x ∈ B
 -/
 TacticDoc ext
 
-/-
+/--
 `fin_cases i` führt eine Fallunterscheidung, wenn `i` ein endlicher Typ ist.
 
 ## Details
 `fin_cases i` ist insbesondere nützlich für `(i : Fin n)`, zum Beispiel als Index in
 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,26 @@ bei dieser Syntax.)
 TacticDoc refine'
 -/
 
+/--
+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.
+Each field you write as `?_` becomes a new proof goal, the fields you supply directly
+do not.
+
+## Example
+
+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 ⟨f, g, ?_, ?_⟩
+```
+into the two proof goals `⊢ LeftInverse g f` and `⊢ RightInverse g f`.
+-/
+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`.

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_CurryEquiv
+import Game.Levels.Iso.L04_EquivalenceBijection
+import Game.Levels.Iso.L05_BijectionEquivalence
+import Game.Levels.Iso.L06_Equivalence
 
 
 World "Iso"

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"

Game/Levels/Iso/L03_CurryEquiv.lean

@@ -0,0 +1,44 @@
+import Game.Metadata
+
+World "Iso"
+Level 3
+
+/-
+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.
+"
+-/
+Introduction "Intro Iso L03"
+
+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.
+
+    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]
+
+NewTactic refine
+
+NewDefinition Equiv Function.curry Function.uncurry

Game/Levels/Iso/L04_EquivalenceBijection.lean

@@ -0,0 +1,27 @@
+import Game.Metadata
+
+World "Iso"
+Level 4
+
+/-
+Introduction
+"
+In this level you show that there every bijection gives rise to an equivalence.
+"
+-/
+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 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.symm
+  constructor
+  apply f.left_inv
+  apply f.right_inv

Game/Levels/Iso/L05_BijectionEquivalence.lean

@@ -0,0 +1,34 @@
+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
+  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}`"
+  choose g hg using h
+  Branch
+    constructor
+    · apply f
+    · apply g
+    · apply hg.1
+    · apply hg.2
+  obtain ⟨hg₁, hg₂⟩ := hg
+  refine ⟨f, g, ?_, ?_⟩
+  · apply hg₁
+  · apply hg₂

Game/Levels/Iso/L06_Equivalence.lean

@@ -0,0 +1,58 @@
+import Game.Metadata
+
+World "Iso"
+Level 6
+
+/-
+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 L06"
+
+open Function
+
+Statement {A : Type} : (Fin 3 → A) ≃ A × A × A := by
+  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`."
+  let g := fun (t : A × A × A ) ↦ ![ t.1, t.2.1, t.2.2]
+  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]
+    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."
+    fin_cases x
+    · Hint (hidden := true) "[Hint n5hjb] Try `simp`."
+      simp
+    · simp
+    · simp
+  · 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 fin_cases
+-- TODO: fin_cases should be in set-theory