bump v4.22.0

Game/Levels/Algorithm/L03add_algo2.lean

@@ -34,7 +34,7 @@ $(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$. -/
 Statement (a b c d e f g h : ℕ) :
     (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h := by
   Hint "Solve this level in one line with `simp only [add_assoc, add_left_comm, add_comm]`"
-  simp only [add_assoc, add_left_comm, add_comm]
+  simp only [add_left_comm, add_comm]
 
 Conclusion
 "

Game/Levels/Algorithm/L07succ_ne_succ.lean

@@ -53,6 +53,7 @@ and goal
 TacticDoc contrapose
 
 NewTactic contrapose
+NewHiddenTactic contrapose!
 
 /-- `succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`. -/
 TheoremDoc MyNat.succ_ne_succ as "succ_ne_succ" in "Peano"

Game/Levels/Implication/L02exact2.lean

@@ -10,7 +10,7 @@ Introduction "If the goal is not *exactly* a hypothesis, we can sometimes
 use rewrites to fix things up."
 
 /-- Assuming $0+x=(0+y)+2$, we have $x=y+2$. -/
-Statement (x : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
+Statement (x y : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
   Hint "You can use `rw [zero_add] at {h}` to rewrite at `{h}` instead
   of at the goal."
   rw [zero_add] at h

Game/Levels/Implication/L07intro2.lean

@@ -12,7 +12,7 @@ Try this one by yourself; if you need help then click on \"Show more help!\".
 "
 
 /-- $x+1=y+1 \implies x=y$. -/
-Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
+Statement (x y : ℕ) : x + 1 = y + 1 → x = y := by
   Hint (hidden := true) "Start with `intro h` to assume the hypothesis."
   intro h
   Hint (hidden := true) "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to