Add test: Function level 10

server/testgame/TestGame/Levels/Function.lean

@@ -1,12 +1,12 @@
 import TestGame.Levels.Function.L01_Function
 import TestGame.Levels.Function.L02_Let
-import TestGame.Levels.Function.L03_Piecewise
+import TestGame.Levels.Function.L03_Composition
-import TestGame.Levels.Function.L04_Injective
+import TestGame.Levels.Function.L06_Piecewise
-import TestGame.Levels.Function.L05_Injective
+import TestGame.Levels.Function.L07_Injective
-import TestGame.Levels.Function.L06_Injective
+import TestGame.Levels.Function.L08_Injective
-import TestGame.Levels.Function.L07_Surjective
+import TestGame.Levels.Function.L09_Surjective
-import TestGame.Levels.Function.L08_Bijective
+import TestGame.Levels.Function.L10_Bijective
-import TestGame.Levels.Function.L09_Inverse
+import TestGame.Levels.Function.L11_Inverse
 
 Game "TestGame"
 World "Function"

server/testgame/TestGame/Levels/Function/L11_Inverse.lean

@@ -0,0 +1,86 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 10
+
+Title "Inverse"
+
+Introduction
+"
+Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
+eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
+und der Gelehrte möchte wissen, wie das den genau ginge.
+
+Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
+aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
+"
+
+open Function
+
+Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
+    Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+  Hint "constructor"
+  constructor
+  Hint "intro h" -- does not show
+  intro h
+  Hint "rcases h with ⟨h₁, h₂⟩" -- shows too late: 1, 2 after
+  rcases h with ⟨h₁, h₂⟩
+  Hint "let g := fun x => (h₂ x).choose" -- shows correct + 1 after
+  let g := fun x => (h₂ x).choose
+  Hint "use g"
+  use g
+  Hint "constructor" -- does not show
+  constructor
+  Hint "intro x" -- does not show
+  intro x
+  Hint "simp" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+  simp
+  Hint "apply h₁"
+  apply h₁
+  Hint "apply Exists.choose_spec (h₂ (f x))"
+  apply Exists.choose_spec (h₂ (f x))
+  Hint "intro y" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+  intro y
+  Hint "simp"
+  simp
+  Hint "apply Exists.choose_spec (h₂ y)"
+  apply Exists.choose_spec (h₂ y)
+  Hint "intro ⟨g, h₁, h₂⟩"
+  intro ⟨g, h₁, h₂⟩
+  Hint "constructor"
+  constructor
+  Hint "intro a b hab"
+  intro a b hab
+  Hint "have h : g (f a) = g (f b)"
+  have h : g (f a) = g (f b)
+  Hint "apply congrArg"
+  apply congrArg
+  Hint "assumption"
+  assumption
+  Hint "rw [h₁, h₁] at h"
+  rw [h₁, h₁] at h
+  Hint "assumption"
+  assumption
+  Hint "intro x"
+  intro x
+  Hint "use g x"
+  use g x
+  Hint "rw [h₂]"
+  rw [h₂]
+
+-- NewDefinition LeftInverse RightInverse
+-- NewLemma Exists.choose Exists.choose_spec congrArg congrFun
+-- DisabledLemma Function.bijective_iff_has_inverse
+
+Hint (A B: Type) (f : A → B) (h : Bijective f) :
+  (∃ g, LeftInverse g f ∧ RightInverse g f) → Bijective f =>
+  "Test"
+
+Conclusion
+"Endlich entkommt ihr dem Tempel.
+
+**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
+
+**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"