Port to leanprover/lean4:v4.26.0

Game/CustomTactic/Linarith.lean

@@ -1,4 +1,5 @@
 import Mathlib.Tactic.Linarith
+import Mathlib.Util.ElabWithoutMVars
 
 open Mathlib.Tactic in
 
@@ -10,7 +11,7 @@ syntax (name := Game.linarith) "linarith" "!"? linarithArgsRest : tactic
 open Lean Mathlib Syntax Elab Tactic in
 elab_rules (kind := Game.linarith) : tactic
   | `(tactic| linarith $[!%$bang]? $cfg:optConfig $[[$args,*]]?) => withMainContext do
-    let args ← ((args.map (TSepArray.getElems)).getD {}).mapM (elabLinarithArg `linarith)
+    let args ← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTermWithoutNewMVars `linarith)
     let cfg := (← elabLinarithConfig cfg).updateReducibility bang.isSome
     commitIfNoEx do liftMetaFinishingTactic <| Linarith.linarith true args.toList cfg
   | `(tactic| linarith $[!%$bang]? $cfg:optConfig only%$o $[[$args,*]]?) =>

Game/Levels/L10Levels/L06_Prod.lean

@@ -62,7 +62,7 @@ specialize hN2 n hn2
 specialize hc n
 rewrite [hc]
 have f1 : |a n * b n - L * M| = |(a n - L) * b n + (L * (b n -  M))| := by ring_nf
-have f2 : |(a n - L) * b n + (L * (b n -  M))| ≤ |(a n - L) * b n| + |(L * (b n -  M))| := by apply abs_add
+have f2 : |(a n - L) * b n + (L * (b n -  M))| ≤ |(a n - L) * b n| + |(L * (b n -  M))| := by apply abs_add_le
 have f3 : |(a n - L) * b n| = |(a n - L)| * |b n| := by apply abs_mul
 have bnBnd : |b n| ≤ K := by apply hK.2 n
 have f5 : |(a n - L)| * |b n| ≤ ε / (2 * K) * K := by bound

Game/Levels/L11Levels/L01_IsCauchyOfLim.lean

@@ -74,7 +74,7 @@ intro n hn m hm
 have hn' : |a n - L| < ε / 2 := by apply hN n hn
 have hm' : |a m - L| < ε / 2 := by apply hN m (by bound)
 rewrite [(by ring_nf : |a m - a n| = |(a m - L) + (L - a n)|)]
-have f1 : |(a m - L) + (L - a n)| ≤ |a m - L| + |L - a n| := by apply abs_add
+have f1 : |(a m - L) + (L - a n)| ≤ |a m - L| + |L - a n| := by apply abs_add_le
 have f2 : |L - a n| = |a n - L| := by apply abs_sub_comm
 linarith [f1, f2, hn', hm']
 

Game/Levels/L11Levels/L02_IsCauchyOfSum.lean

@@ -55,7 +55,7 @@ specialize hN1 n (by bound) m (by bound)
 specialize hN2 n (by bound) m (by bound)
 change |(a m + b m) - (a n + b n)| < ε
 rewrite [(by ring_nf : |(a m + b m) - (a n + b n)| = |(a m - a n) + (b m - b n)|)]
-have f1 : |a m - a n + (b m - b n)| ≤ |a m - a n| + |(b m - b n)| := by apply abs_add
+have f1 : |a m - a n + (b m - b n)| ≤ |a m - a n| + |(b m - b n)| := by apply abs_add_le
 linarith [f1, hN1, hN2]
 
 Conclusion "

Game/Levels/L11Levels/L03_IsBddOfCauchy.lean

@@ -65,7 +65,7 @@ specialize f1 m hm
 linarith [f1, aNnonneg]
 specialize hN (by bound)
 have f2 : |a m| = |(a m - a N) + a N| := by ring_nf
-have f3 : |(a m - a N) + a N| ≤ |a m - a N| + |a N| := by apply abs_add
+have f3 : |(a m - a N) + a N| ≤ |a m - a N| + |a N| := by apply abs_add_le
 linarith [f2, f3, hN, sumNonneg]
 
 Conclusion "

Game/Levels/L15Levels/L01_check.lean

@@ -176,8 +176,8 @@ have hy : IsCauchy y := by
   have qmBnd := hN m (N m) (by bound)
   have f1 : |(q m (N m) : ℝ) - q n (N n)| = |(q m (N m) - x m) + ((x n - q n (N n)) + (x m - x n))| := by ring_nf
   have f2 : |(q m (N m) - x m) + ((x n - q n (N n)) + (x m - x n))| ≤
-    |(q m (N m) - x m)| + |(x n - q n (N n)) + (x m - x n)| := by apply abs_add
-  have f3 : |(x n - q n (N n)) + (x m - x n)| ≤ |(x n - q n (N n))| + |(x m - x n)| := by apply abs_add
+    |(q m (N m) - x m)| + |(x n - q n (N n)) + (x m - x n)| := by apply abs_add_le
+  have f3 : |(x n - q n (N n)) + (x m - x n)| ≤ |(x n - q n (N n))| + |(x m - x n)| := by apply abs_add_le
   have f3' : |(x n - q n (N n))| = |q n (N n) - x n| := by apply abs_sub_comm
   field_simp at hN2
   have hn' : (N1 : ℝ) + N2 ≤ n := by exact_mod_cast hn
@@ -204,7 +204,7 @@ change |x n - L| < ε
 change ∀ n ≥ N3, |y n - L| < ε / 2 at hN3
 
 rewrite [show |x n - L| = |(x n - y n) + (y n - L)| by ring_nf]
-have f1 : |(x n - y n) + (y n - L)| ≤ |(x n - y n)| + |(y n - L)| := by apply abs_add
+have f1 : |(x n - y n) + (y n - L)| ≤ |(x n - y n)| + |(y n - L)| := by apply abs_add_le
 specialize hN n (N n) (by bound)
 change |y n - x n| < 1 / (n + 1) at hN
 rewrite [show |y n - x n| = |x n - y n| by apply abs_sub_comm] at hN

Game/Levels/L15Levels/L01_completenessAlt.lean

@@ -122,7 +122,7 @@ intro n hn m hm
 change |q m (N' m) - q n (N' n)| < ε
 have f1 : |q m (N' m) - q n (N' n)| = |(q m (N' m) -  q n (N' m)) + (q n (N' m) - q n (N' n))| := by ring_nf
 have f2 : |(q m (N' m) -  q n (N' m)) + (q n (N' m) - q n (N' n))| ≤
-  |(q m (N' m) -  q n (N' m))| + |(q n (N' m) - q n (N' n))| := by apply abs_add
+  |(q m (N' m) -  q n (N' m))| + |(q n (N' m) - q n (N' n))| := by apply abs_add_le
 have := (N'bnd' m n hm)
 have := hN1
 --have := hN m (N' m) (N'bnd m) (N' n) (by apply N'mono hm)
@@ -161,8 +161,8 @@ have hy : IsCauchy y := by
   change |(q m (N m)) - xm| < 1 / (m + 1) at qmBnd
   have f1 : |(q m (N m) : ℝ) - q n (N n)| = |(q m (N m) - xm) + ((xn - q n (N n)) + (xm - xn))| := by ring_nf
   have f2 : |(q m (N m) - xm) + ((xn - q n (N n)) + (xm - xn))| ≤
-    |(q m (N m) - xm)| + |(xn - q n (N n)) + (xm - xn)| := by apply abs_add
-  have f3 : |(xn - q n (N n)) + (xm - xn)| ≤ |(xn - q n (N n))| + |(xm - xn)| := by apply abs_add
+    |(q m (N m) - xm)| + |(xn - q n (N n)) + (xm - xn)| := by apply abs_add_le
+  have f3 : |(xn - q n (N n)) + (xm - xn)| ≤ |(xn - q n (N n))| + |(xm - xn)| := by apply abs_add_le
   have f3' : |(xn - q n (N n))| = |q n (N n) - xn| := by apply abs_sub_comm
   have f4 : (1 : ℝ) / (n + 1) < ε / 3 := by sorry
   have f5 : (1 : ℝ) / (m + 1) < ε / 3 := by sorry
@@ -183,7 +183,7 @@ change |xn - L| < ε
 change ∀ n ≥ N3, |y n - L| < ε / 2 at hN3
 
 rewrite [show |xn - L| = |(xn - y n) + (y n - L)| by ring_nf]
-have f1 : |(xn - y n) + (y n - L)| ≤ |(xn - y n)| + |(y n - L)| := by apply abs_add
+have f1 : |(xn - y n) + (y n - L)| ≤ |(xn - y n)| + |(y n - L)| := by apply abs_add_le
 specialize hN n (N n) (by bound)
 change |y n - xn| < 1 / (n + 1) at hN
 rewrite [show |y n - xn| = |xn - y n| by apply abs_sub_comm] at hN

Game/Levels/L18Pset/L02.lean

@@ -23,7 +23,7 @@ by_cases hm' : n ≤ m
 specialize hm hm'
 rewrite [sum_Ico_succ hm']
 rewrite [sum_Ico_succ hm']
-have f : |∑ k ∈ Ico n m, a k + a m|  ≤ |∑ k ∈ Ico n m, a k| + |a m| := by apply abs_add
+have f : |∑ k ∈ Ico n m, a k + a m|  ≤ |∑ k ∈ Ico n m, a k| + |a m| := by apply abs_add_le
 linarith [f, hm]
 have hn : n = m+1 := by bound
 rewrite [hn]

Game/Levels/L18Pset/L04.lean

@@ -30,9 +30,8 @@ specialize hN2 n (by bound)
 specialize hN3 n (by bound)
 ring_nf at hN3
 have f1 : |L - M| = |(L - a n) + ((a n - b n) + (b n - M))| := by ring_nf
-have f2 : |(L - a n) + ((a n - b n) + (b n - M))| ≤ |(L - a n)| + |((a n - b n) + (b n - M))| := by apply abs_add
-have f3 : |((a n - b n) + (b n - M))| ≤ |(a n - b n)| + |(b n - M)| := by apply
-abs_add
+have f2 : |(L - a n) + ((a n - b n) + (b n - M))| ≤ |(L - a n)| + |((a n - b n) + (b n - M))| := by apply abs_add_le
+have f3 : |((a n - b n) + (b n - M))| ≤ |(a n - b n)| + |(b n - M)| := by apply abs_add_le
 have f4 : |(L - a n)| = |a n - L| := by apply abs_sub_comm
 linarith[ f1, f2, f3,f4, hN1, hN2, hN3]
 

Game/Levels/L19Levels/L03.lean

@@ -94,7 +94,7 @@ specialize hN1 (N1 + N2) (by bound)
 rewrite [show Series (a ∘ σ) n - L =
   (Series (a ∘ σ) n - Series a (N1 + N2)) + (Series a (N1 + N2) - L) by ring_nf]
 have f1 : |Series (a ∘ σ) n - Series a (N1 + N2) + (Series a (N1 + N2) - L)|
-        ≤ |Series (a ∘ σ) n - Series a (N1 + N2)| + |(Series a (N1 + N2) - L)| := by apply abs_add
+        ≤ |Series (a ∘ σ) n - Series a (N1 + N2)| + |(Series a (N1 + N2) - L)| := by apply abs_add_le
 have f2 : |Series (a ∘ σ) n - Series a (N1 + N2)| =
     |∑ k ∈ image σ (range n) \ range (N1 + N2), a k| := by
   have f : Series (a ∘ σ) n = ∑ k ∈ image σ (range n), a k := Series_image a σ hσ.1 n

Game/Levels/L20Levels/L03.lean

@@ -66,7 +66,7 @@ specialize hf x hx1
 specialize hg x hx2
 change |f x + g x - (f c + g c)| < ε
 rewrite [show f x + g x - (f c + g c) = (f x - f c) + (g x - g c) by ring_nf]
-have f1 : |(f x - f c) + (g x - g c)| ≤ |(f x - f c)| + |(g x - g c)| := by apply abs_add
+have f1 : |(f x - f c) + (g x - g c)| ≤ |(f x - f c)| + |(g x - g c)| := by apply abs_add_le
 linarith [f1, hf, hg]
 
 Conclusion "

Game/Levels/L21Levels/L08.lean

@@ -93,7 +93,7 @@ have ht2 : |t - x| < ε / (|2 * x| + 1) := by linarith [ht, δ2]
 have ht : |t + x| ≤ |2 * x| + 1 := by
   have ht' : |t + x| ≤ |t - x| + |2 * x| := by
     rewrite [show t + x = t - x + 2 * x by ring_nf]
-    have f1 : |t - x + 2 * x| ≤ |t - x| + |2 * x| := by apply abs_add
+    have f1 : |t - x + 2 * x| ≤ |t - x| + |2 * x| := by apply abs_add_le
     apply f1
   linarith [ht', ht1]
 have ht' : |t - x| * |t + x| ≤ |t - x| * (|2 * x| + 1) := by bound

Game/Levels/L22Levels/L02.lean

@@ -115,9 +115,9 @@ intro y hy
 have h1 : |F y - F x| ≤ |f N y - F y| + |f N y - f N x| + |f N x - F x| := by
     rewrite [show F y - F x = (F y - f N y) + ((f N y - f N x) + (f N x - F x)) by ring_nf]
     have f1 : |(F y - f N y) + ((f N y - f N x) + (f N x - F x))| ≤
-        |(F y - f N y)| + |((f N y - f N x) + (f N x - F x))| := by apply abs_add
+        |(F y - f N y)| + |((f N y - f N x) + (f N x - F x))| := by apply abs_add_le
     have f2 : |((f N y - f N x) + (f N x - F x))| ≤ |f N y - f N x| + |f N x - F x| :=
-        by apply abs_add
+        by apply abs_add_le
     have f3 : |F y - f N y| = |f N y - F y| := by apply abs_sub_comm
     linarith [f1, f2, f3]
 have h2 : |f N y - F y| < ε / 3 := by apply hN N (by bound) y

Game/Levels/L23Levels/L02.lean

@@ -64,7 +64,7 @@ have f1 : |RiemannSum f a b m - RiemannSum f a b n| ≤
   rewrite [show RiemannSum f a b m - RiemannSum f a b n =
       (RiemannSum f a b m - RiemannSum f a b (m * n)) +
       (RiemannSum f a b (n * m) - RiemannSum f a b n) by ring_nf]
-  apply abs_add
+  apply abs_add_le
 have hfn := RiemannSumRefinement f hab (show n ≠ 0 by bound) (show m ≠ 0 by bound) (show 0 < ε / (2 * (b - a)) by bound)
     (show 0 < δ by bound) hδ₂ hn_small
 have hfm := RiemannSumRefinement f hab (show m ≠ 0 by bound) (show n ≠ 0 by bound) (show 0 < ε / (2 * (b - a)) by bound)

Game/Levels/L23Levels/L03.lean

@@ -141,13 +141,13 @@ have hxy' : |y - x| < (δs i i.2) / 2 := by
   sorry
 have hyxi : |y - xs i| < (δs i i.2) := by
   rewrite [show y - xs i = (y - x) + (x - xs i) by ring_nf]
-  have h1 : |(y - x) + (x - xs i)| ≤ |y - x| + |x - xs i| := by apply abs_add
+  have h1 : |(y - x) + (x - xs i)| ≤ |y - x| + |x - xs i| := by apply abs_add_le
   have h2 : |x - xs i| = |xs i - x| := by apply abs_sub_comm
   linarith [hxy', hxxi, h1, h2]
 have fyfxi := hδs (xs i) i.2 y hy hyxi
 have fxix := hδs (xs i) i.2 x hx hxxi'
 rewrite [show f y - f x = (f y - f (xs i)) + (f (xs i) - f x) by ring_nf]
-have h1 : |(f y - f (xs i)) + (f (xs i) - f x)| ≤ |f y - f (xs i)| + |f (xs i) - f x| := by apply abs_add
+have h1 : |(f y - f (xs i)) + (f (xs i) - f x)| ≤ |f y - f (xs i)| + |f (xs i) - f x| := by apply abs_add_le
 rewrite [show |f (xs i) - f x| = |f x - f (xs i)| by apply abs_sub_comm] at h1
 linarith [fyfxi, fxix, h1]
 

Game/Levels/L24Levels/L02.lean

@@ -126,7 +126,7 @@ have hz'' : |z - xi| < ri := by
 have hz''' : |y - z| ≤ ri := by linarith [hz', hr]
 have hiy : |y - xi| ≤ |y - z| + |z - xi| := by
   rewrite [show y - xi = (y - z) + (z - xi) by ring_nf]
-  apply abs_add
+  apply abs_add_le
 linarith [hdist, hz'', hz''', hiy, ripos]
 
 intro z hz

Game/Levels/L4Levels/L01_NonConverge.lean

@@ -102,9 +102,9 @@ And that get us the desired contradiction.
 - **Negation**: If `P` is some `Prop`, then `¬ P` is definitionally equivalent to `P → False`. So you can write `change P → False`, either at the Goal, or `at` a hypothesis.
 
 
-- **The triangle inequality**: To add the fact that `|x + y| ≤ |x| + |y|` to our list of hypotheses, invoke the `abs_add` theorem:
+- **The triangle inequality**: To add the fact that `|x + y| ≤ |x| + |y|` to our list of hypotheses, invoke the `abs_add_le` theorem:
 
-`have factName : |x + y| ≤ |x| + |y| := by apply abs_add`
+`have factName : |x + y| ≤ |x| + |y| := by apply abs_add_le`
 
 - **Negation inside an absolute value**: You may also find useful the theorem `abs_neg`, which can be called via:
 
@@ -119,16 +119,16 @@ followed by a minus sign, `abs_neg` won't work!
 "
 
 /--
-Usage: `have factName : |x + y| ≤ |x| + |y| := by apply abs_add`
+Usage: `have factName : |x + y| ≤ |x| + |y| := by apply abs_add_le`
 -/
-TheoremDoc abs_add as "abs_add" in "|x|"
+TheoremDoc abs_add_le as "abs_add_le" in "|x|"
 
 /--
 Usage: `have factName : |-x| = |x| := by apply abs_neg`
 -/
 TheoremDoc abs_neg as "abs_neg" in "|x|"
 
-NewTheorem abs_add abs_neg
+NewTheorem abs_add_le abs_neg
 
 /-- `(a : ℕ → ℝ) := ∃ L, SeqLim a L`
 
@@ -166,10 +166,10 @@ Statement (a : ℕ → ℝ) (ha : ∀ n, a n = (-1) ^ n) :
   rewrite [f5] at f1
   have f6 : (-1 : ℝ) ^ (2 * N + 1) = -1 := by bound
   rewrite [f6] at f2
-  have f7 : (2 : ℝ) = |2| := by norm_num
+  have f7 : (2 : ℝ) = |2| := (abs_of_pos two_pos).symm
   have f8 : |(2 : ℝ)| = |1 - (-1)| := by ring_nf
-  have f9 : |1 - (-1)| = |(1 - L) + (L - (-1))| := by ring_nf
-  have f10 : |(1 - L) + (L - (-1))| ≤ |(1 - L)| + |(L - (-1))| := by apply abs_add
+  have f9 : |1 - (-1)| = |(1 - L) + (L - (-1))| := by congr 1; ring
+  have f10 : |(1 - L) + (L - (-1))| ≤ |(1 - L)| + |(L - (-1))| := by apply abs_add_le
   have f11 : |(L - (-1))| = |-((-1) - L)| := by ring_nf
   have f12 : |-((-1) - L)| = |((-1) - L)| := by apply abs_neg
   have f13 : (2 : ℝ) < 1/2 + 1/2 := by linarith [f8, f9, f10, f11, f12, f7, f1, f2]

Game/Levels/L4Pset/L4Pset1.lean

@@ -49,17 +49,17 @@ Statement (a : ℕ → ℝ) (ha2n : ∀ n, a (2 * n) = 3 - 1 / n) (ha2np1 : ∀
   have f6' : N ≤ 2 * (N + 5) + 1 := by bound
   have f7' : |a (2 * (N + 5) + 1) - L| < 1 / 2 := by apply hN (2 * (N + 5) + 1) f6'
 
-  have f8 : (2 : ℝ) = |2| := by norm_num
-  have f9 : |(2 : ℝ)| = |(3 - L) + (L - 1)| := by ring_nf
-  have f10 : |(3 - L) + (L - 1)| ≤ |(3 - L)| + |(L - 1)| := by apply abs_add
-  have f11 : |(3 - L)| = |(3 - a (2 * (N + 5))) + (a (2 * (N + 5)) - L)| := by ring_nf
+  have f8 : (2 : ℝ) = |2| := (abs_of_pos two_pos).symm
+  have f9 : |(2 : ℝ)| = |(3 - L) + (L - 1)| := by congr 1; ring
+  have f10 : |(3 - L) + (L - 1)| ≤ |(3 - L)| + |(L - 1)| := by apply abs_add_le
+  have f11 : |(3 - L)| = |(3 - a (2 * (N + 5))) + (a (2 * (N + 5)) - L)| := by congr 1; ring
   have f12 : |(3 - a (2 * (N + 5))) + (a (2 * (N + 5)) - L)| ≤
-    |(3 - a (2 * (N + 5)))| + |(a (2 * (N + 5)) - L)| := by apply abs_add
+    |(3 - a (2 * (N + 5)))| + |(a (2 * (N + 5)) - L)| := by apply abs_add_le
 
-  have f13 : |(L - 1)| = |-(1 - L)| := by ring_nf
+  have f13 : |(L - 1)| = |-(1 - L)| := by congr 1; ring
   have f14 : |-(1 - L)| = |(1 - L)| := by apply abs_neg
-  have f15 : |(1 - L)| = |(1 - a (2 * (N + 5) + 1)) + (a (2 * (N + 5) + 1) - L)| := by ring_nf
-  have f16 : |(1 - a (2 * (N + 5) + 1)) + (a (2 * (N + 5) + 1) - L)| ≤ |(1 - a (2 * (N + 5) + 1))| + |(a (2 * (N + 5) + 1) - L)| := by apply abs_add
+  have f15 : |(1 - L)| = |(1 - a (2 * (N + 5) + 1)) + (a (2 * (N + 5) + 1) - L)| := by congr 1; ring
+  have f16 : |(1 - a (2 * (N + 5) + 1)) + (a (2 * (N + 5) + 1) - L)| ≤ |(1 - a (2 * (N + 5) + 1))| + |(a (2 * (N + 5) + 1) - L)| := by apply abs_add_le
 
   have f17 : (2 : ℝ) ≤ 1 / 4 + 1 / 2 + 1 / 4 + 1 / 2 := by linarith [f8, f9, f10, f11, f12, f13, f14, f15, f16, f7, f7', f2, f2', f4]
   norm_num at f17

Game/Levels/L6Levels/L00_SumOfSeqs.lean

@@ -74,7 +74,7 @@ Statement SumLim (a b c : ℕ → ℝ) (L M : ℝ)
   specialize hNa ineq_a
   specialize hNb ineq_b
   have ineq : |a n - L + (b n - M)| ≤
-    |a n - L| + |(b n - M)| := by apply abs_add
+    |a n - L| + |(b n - M)| := by apply abs_add_le
   bound --linarith [hNa, hNb, ineq]
 
 

Game/Levels/L6Pset/L6Pset4.lean

@@ -25,7 +25,7 @@ choose n hn using ha
 specialize hN n hn.1
 have ha : |a n| > 10 := by apply hn.2
 have f2 : |a n| = |(a n - L) + L| := by ring_nf
-have f3 : |(a n - L) + L| ≤ |(a n - L)| + |L| := by apply abs_add
+have f3 : |(a n - L) + L| ≤ |(a n - L)| + |L| := by apply abs_add_le
 linarith [f1, ha, f2, f3, hN]
 
 Conclusion "Done."

Game/Levels/L7Levels/L00_Uniqueness.lean

@@ -80,7 +80,7 @@ specialize hN1 (N1 + N2) f3
 specialize hN2 (N1 + N2) f4
 have f5 : |L - M| = |(L - a (N1+N2)) + (a (N1 + N2) - M)| := by ring_nf
 have f6 : |(L - a (N1+N2)) + (a (N1 + N2) - M)| ≤
-    |(L - a (N1+N2))| + |(a (N1 + N2) - M)| := by apply abs_add
+    |(L - a (N1+N2))| + |(a (N1 + N2) - M)| := by apply abs_add_le
 have f7 : |(L - a (N1+N2))| = |-(a (N1+N2) - L)| := by ring_nf
 have f8 : |-(a (N1+N2) - L)| = |(a (N1+N2) - L)| := by apply abs_neg
 linarith [f5, f6, f7, f8, hN1, hN2]

Game/Levels/L7Levels/L01_Eventually.lean

@@ -61,7 +61,7 @@ use N
 intro n hn
 specialize hN n hn
 have l1 : |L| = |a n + (L - a n)| := by ring_nf
-have l2 : |a n + (L - a n)| ≤ |a n| + |L - a n| := by apply abs_add
+have l2 : |a n + (L - a n)| ≤ |a n| + |L - a n| := by apply abs_add_le
 have l3 : |L - a n| = |-(a n - L)| := by ring_nf
 have l4 : |-(a n - L)| = |(a n - L)| := by apply abs_neg
 linarith [l1, l2, l3, l4, hN]

Game/Levels/L7Pset/L7Pset1.lean

@@ -25,7 +25,7 @@ use N
 intro n hn
 specialize hN n hn
 have f1 : |a n| = |a n - L + L| := by ring_nf
-have f2 : |a n - L + L| ≤ |a n - L| + |L| := by apply abs_add
+have f2 : |a n - L + L| ≤ |a n - L| + |L| := by apply abs_add_le
 linarith [f1, f2, hN]
 
 Conclusion "Done."

Game/Levels/L7Pset/L7Pset3.lean

@@ -27,7 +27,7 @@ have absy : |-y| = |y| := by apply abs_neg
 have absy' : |-y| = -y := by apply abs_of_nonneg hy
 have xsubneg : |x - -y| = |x + y| := by ring_nf
 rewrite [← absy, absy', xsubneg]
-have f1 : |x + y| ≤ |x| + |y| := by apply abs_add
+have f1 : |x + y| ≤ |x| + |y| := by apply abs_add_le
 rewrite [absx, ← absy, absy'] at f1
 have f2 : x + -y = x - y := by ring_nf
 rewrite [f2] at f1
@@ -48,7 +48,7 @@ have xy : 0 ≤ -(x - y) := by bound
 have absxy : |-(x - y)| = -(x - y) := by apply abs_of_nonneg xy
 have absxy' : |-(x - y)| = |x - y| := by apply abs_neg
 rewrite [f1, f2, ← absxy', absxy]
-have f3 : |x + y| ≤ |x| + |y| := by apply abs_add
+have f3 : |x + y| ≤ |x| + |y| := by apply abs_add_le
 rewrite [absy, ← absxneg, absxeq] at f3
 have f4 : -(x - y) = -x + y := by ring_nf
 rewrite [f4]

Game/Metadata.lean

@@ -8,7 +8,7 @@ import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Analysis.SpecialFunctions.Log.Base
---import Mathlib.Tactic.Cases -- CasesPrime???
+import Mathlib.Tactic.Cases
 
 /-! Use this file to add things that should be available in all levels.