chore: Forward-port to Lean/mathlib v4.31.0 (#830)

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: gotrevor

Foundation.lean

@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import Foundation.FirstOrder.Arithmetic.Basic
 public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy

Foundation/FirstOrder/Arithmetic/Basic/Hierarchy.lean

@@ -315,7 +315,7 @@ set_option linter.flexible false in
 
 lemma exsClosure : {n : ℕ} → {φ : Semiformula L ξ n} → Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) (exsClosure φ)
   | 0, _, hp => hp
-  | n + 1, φ, hp => by simpa using exsClosure (hp.exs)
+  | n + 1, φ, hp => exsClosure (φ := ∃⁰ φ) hp.exs
 
 instance : LogicalConnective.AndOrClosed (Hierarchy Γ s : Semiformula L ξ k → Prop) where
   verum := verum _ _ _

Foundation/FirstOrder/Arithmetic/Definability/Absoluteness.lean

@@ -30,7 +30,7 @@ lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin
 lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1)}
     (hf : 𝚺₀.DefinedFunction f φ) (hf' : 𝚺₀.DefinedFunction f' φ) (v : Fin k → ℕ) :
     (f v : V) = f' (Nat.cast ∘ v) := by
-  simpa using Defined.shigmaZero_absolute V hf hf' (f v :> v)
+  simpa [Function.comp_def] using Defined.shigmaZero_absolute V hf hf' (f v :> v)
 
 lemma sigmaOne_upward_absolute {k} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
     φ.val.Evalb v → φ.val.Evalb (M := V) (Nat.cast ∘ v) := by
@@ -56,7 +56,7 @@ lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k
 lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1)}
     (hf : 𝚺₁.DefinedFunction f φ) (hf' : 𝚺₁.DefinedFunction f' φ) (v : Fin k → ℕ) :
     (f v : V) = f' (Nat.cast ∘ v) := by
-  simpa using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v)
+  simpa [Function.comp_def] using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v)
 
 variable {V}
 

Foundation/FirstOrder/Arithmetic/Definability/BoundedDefinable.lean

@@ -55,8 +55,8 @@ lemma comp [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {k} {f : (Fin l → V) → V} {g :
     choose tg htg using fun i ↦ (hg i).bounded
     exact ⟨Rew.subst tg tf, by
       intro v
-      simpa [Semiterm.val_substs]
-        using le_trans (htf (g · v)) (Structure.Monotone.term_monotone tf (fun i ↦ htg i v) (by simp))⟩
+      simpa [Semiterm.val_substs, Function.comp_def]
+        using! le_trans (htf (g · v)) (Structure.Monotone.term_monotone tf (fun i ↦ htg i v) (by simp))⟩
 
 end Bounded
 

Foundation/FirstOrder/Arithmetic/Definability/Hierarchy.lean

@@ -169,7 +169,7 @@ lemma ProvablyProperOn.ofProperOn [𝗘𝗤 ℒₒᵣ ⪯ T] {φ : 𝚫-[m].Semi
     (h : ∀ (M : Type w) [ORingStructure M] [M↓[ℒₒᵣ] ⊧* T], φ.ProperOn M) : φ.ProvablyProperOn T := by
   apply FirstOrder.Arithmetic.complete.{w} T _ ?_
   intro M _ _
-  simpa [models_iff] using (h M).iff
+  simpa [models_iff] using! (h M).iff
 
 variable {T}
 

Foundation/FirstOrder/Arithmetic/Exponential/Bit.lean

@@ -186,10 +186,10 @@ end model
 section model
 
 lemma mem_iff_mul_exp_add_exp_add {i a : V} : i ∈ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + Exp.exp i + r := by
-  simpa [mem_iff_bit, exp_succ] using lenbit_iff_add_mul (exp_pow2 i) (a := a)
+  simpa [mem_iff_bit, exp_succ] using! lenbit_iff_add_mul (exp_pow2 i) (a := a)
 
 lemma not_mem_iff_mul_exp_add {i a : V} : i ∉ a ↔ ∃ k, ∃ r < Exp.exp i, a = k * Exp.exp (i + 1) + r := by
-  simpa [mem_iff_bit, exp_succ] using not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
+  simpa [mem_iff_bit, exp_succ] using! not_lenbit_iff_add_mul (exp_pow2 i) (a := a)
 
 section empty
 
@@ -239,13 +239,13 @@ instance : LawfulSingleton V V where
     i ∈ insert j a ↔ i = j ∨ i ∈ a := by
   by_cases h : j ∈ a <;> simp [h, insert_eq, bitInsert]
   · by_cases e : i = j <;> simp [h, e]
-  · simpa [exp_inj.eq_iff] using
+  · simpa [exp_inj.eq_iff] using!
       lenbit_add_pow2_iff_of_not_lenbit (exp_pow2 i) (exp_pow2 j) h
 
 @[simp] lemma mem_bitRemove_iff {i j a : V} :
     i ∈ bitRemove j a ↔ i ≠ j ∧ i ∈ a := by
   by_cases h : j ∈ a
-  · simpa [h, bitRemove, exp_inj.eq_iff] using
+  · simpa [h, bitRemove, exp_inj.eq_iff] using!
       lenbit_sub_pow2_iff_of_lenbit (exp_pow2 i) (exp_pow2 j) h
   · simp only [bitRemove, h, ↓reduceIte, ne_eq, iff_and_self]
     rintro _ rfl; contradiction
@@ -442,7 +442,7 @@ lemma nonempty_of_pos {a : V} (h : 0 < a) : ∃ i, i ∈ a := by
   simp [this] at h
 
 lemma eq_empty_or_nonempty (a : V) : a = ∅ ∨ ∃ i, i ∈ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [emptyset_def]
   · right; exact nonempty_of_pos pos
 
@@ -457,7 +457,7 @@ lemma isempty_iff {s : V} : s = ∅ ↔ ∀ x, x ∉ s := by
 @[simp] lemma empty_subset (s : V) : ∅ ⊆ s := by intro x; simp
 
 lemma lt_of_lt_log {a b : V} (pos : 0 < b) (h : ∀ i ∈ a, i < log b) : a < b := by
-  rcases zero_le a with (rfl | apos)
+  rcases Arithmetic.zero_le a with (rfl | apos)
   · exact pos
   by_contra A
   exact not_lt_of_ge (log_monotone <| show b ≤ a by simpa using A) (h (log a) (log_mem_of_pos apos))

Foundation/FirstOrder/Arithmetic/Exponential/Log.lean

@@ -25,7 +25,7 @@ lemma log_exists_unique_pos {y : V} (hy : 0 < y) : ∃! x, x < y ∧ ∃ y' ≤
       exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)),
         2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩
     case odd y IH =>
-      rcases (zero_le y : 0 ≤ y) with (rfl | pos)
+      rcases (Arithmetic.zero_le y : 0 ≤ y) with (rfl | pos)
       · simp
       · rcases (IH pos : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
         exact ⟨x + 1, by simpa using lt_of_lt_of_le hxy (by simp),
@@ -62,7 +62,7 @@ lemma log_lt_self_of_pos {y : V} (pos : 0 < y) : log y < y :=
   ((Classical.choose!_spec (log_exists_unique y)).2 pos).1
 
 @[simp] lemma log_le_self (a : V) : log a ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · exact le_of_lt <| log_lt_self_of_pos pos
 
@@ -121,9 +121,9 @@ lemma log_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : log (a * p) = log a +
   simpa using log_mul_pow2_add_of_lt pos pp pp.pos
 
 lemma log_monotone {a b : V} (h : a ≤ b) : log a ≤ log b := by
-  rcases zero_le a with (rfl | posa)
+  rcases Arithmetic.zero_le a with (rfl | posa)
   · simp
-  rcases zero_le b with (rfl | posb)
+  rcases Arithmetic.zero_le b with (rfl | posb)
   · have := lt_of_lt_of_le posa h; simp_all
   rcases log_pos posa with ⟨a', ha', Ha, _⟩
   rcases log_pos posb with ⟨b', _, Hb, hb⟩
@@ -147,12 +147,12 @@ lemma length_eq_binaryLength (a : V) : ‖a‖ = if 0 < a then log a + 1 else 0
 lemma length_of_pos {a : V} (pos : 0 < a) : ‖a‖ = log a + 1 := by simp [length_eq_binaryLength, pos]
 
 @[simp] lemma length_le (a : V) : ‖a‖ ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [pos, length_of_pos, ←lt_iff_succ_le, log_lt_self_of_pos]
 
 lemma length_graph {i a : V} : i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0) := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [length_of_pos, pos, pos_iff_ne_zero.mp pos]
 
@@ -174,7 +174,7 @@ lemma length_two_mul_of_pos {a : V} (pos : 0 < a) : ‖2 * a‖ = ‖a‖ + 1 :=
   simp [pos, length_of_pos, log_two_mul_of_pos]
 
 lemma length_two_mul_add_one (a : V) : ‖2 * a + 1‖ = ‖a‖ + 1 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [pos, length_of_pos, log_two_mul_add_one_of_pos]
 
@@ -185,7 +185,7 @@ lemma length_mul_pow2 {a p : V} (pos : 0 < a) (pp : Pow2 p) : ‖a * p‖ = ‖a
   simp [length_of_pos, pos, pp.pos, log_mul_pow2 pos pp, add_right_comm (log a) (log p) 1]
 
 lemma length_monotone {a b : V} (h : a ≤ b) : ‖a‖ ≤ ‖b‖ := by
-  rcases zero_le a with (rfl | posa)
+  rcases Arithmetic.zero_le a with (rfl | posa)
   · simp
   · simpa [length_of_pos posa, length_of_pos (lt_of_lt_of_le posa h)]
     using log_monotone h
@@ -208,13 +208,13 @@ lemma exponential_log_le_self {a b : V} (pos : 0 < a) (h : Exponential (log a) b
   assumption
 
 lemma lt_exponential_log_self {a b : V} (h : Exponential (log a) b) : a < 2 * b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   rcases log_pos pos with ⟨_, _, H, _⟩; rcases H.uniq h
   assumption
 
 lemma lt_exp_len_self {a b : V} (h : Exponential ‖a‖ b) : a < b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h
   rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩
@@ -225,7 +225,7 @@ lemma le_iff_le_log_of_exp {x y a : V} (H : Exponential x y) (pos : 0 < a) : y 
    fun h ↦ by rcases log_pos pos with ⟨a', ha', Haa', _⟩; exact le_trans (Exponential.monotone_le H Haa' h) ha'⟩
 
 lemma le_iff_lt_length_of_exp {x y a : V} (H : Exponential x y) : y ≤ a ↔ x < ‖a‖ := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simpa using pos_iff_ne_zero.mp H.range_pos
   simp [le_iff_le_log_of_exp H pos, length_of_pos pos, ←le_iff_lt_succ]
 
@@ -242,7 +242,7 @@ lemma Exponential.le_log {x y : V} (H : Exponential x y) : x ≤ log y := (le_if
 lemma Exponential.lt_length {x y : V} (H : Exponential x y) : x < ‖y‖ := (le_iff_lt_length_of_exp H).mp (by rfl)
 
 lemma lt_exponential_length {a b : V} (h : Exponential ‖a‖ b) : a < b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp at h; simp [h]
   have : Exponential (log a + 1) b := by simpa [length_of_pos pos] using h
   rcases Exponential.exponential_succ.mp this with ⟨b, rfl, H⟩
@@ -261,7 +261,7 @@ lemma sq_len_le_three_mul (a : V) : ‖a‖ ^ 2 ≤ 3 * a := by
       _           ≤ 3 * a + 2 * a + a     := by simp [←pos_iff_one_le, pos]
       _           = 3 * (2 * a)           := by simp_all only [←two_add_one_eq_three, two_mul, add_mul, add_assoc, one_mul]
   case odd a IH =>
-    rcases zero_le a with (rfl | pos)
+    rcases Arithmetic.zero_le a with (rfl | pos)
     · simp [←two_add_one_eq_three]
     calc
       ‖2 * a + 1‖ ^ 2 = (‖a‖ + 1) ^ 2         := by rw [length_two_mul_add_one a]
@@ -380,7 +380,7 @@ lemma bexp_two_mul {a a' x : V} (hx : 2 * x < ‖a‖) (hx' : x < ‖a'‖) :
   bexp_eq_of_exp hx (exp_bexp_of_lt hx').bit_zero
 
 lemma bexp_two_mul_succ {a i : V} : bexp (2 * a) (i + 1) = 2 * bexp a i := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   rcases show i ≥ ‖a‖ ∨ i < ‖a‖ from le_or_gt ‖a‖ i with (h | h)
   · simp [bexp_eq_zero_of_le, h, show ‖2 * a‖ ≤ i + 1 from by simp [length_two_mul_of_pos pos, h]]
@@ -421,7 +421,7 @@ instance : Bounded₂ (fbit : V → V → V) := ⟨‘1’, λ _ ↦ by simp⟩
   simp [fbit, bexp_two_mul_add_one_succ, Arithmetic.div_mul]
 
 @[simp] lemma fbit_two_mul_zero_eq_zero (a : V) : fbit (2 * a) 0 = 0 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · have : bexp (2 * a) 0 = 1 := bexp_eq_of_exp (by simp [pos]) (by simp)
     simp [fbit, this]

Foundation/FirstOrder/Arithmetic/Exponential/Pow2.lean

@@ -141,7 +141,7 @@ lemma not_lenbit_iff_rem {i a : V} : ¬LenBit i a ↔ (a / i) % 2 = 0 := by
 @[simp] lemma LenBit.self {a : V} (pos : 0 < a) : LenBit a a := by simp [LenBit.iff_rem, pos]
 
 lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a := by
-  have : 0 ≤ i := zero_le i
+  have : 0 ≤ i := Arithmetic.zero_le i
   rcases (eq_or_lt_of_le this) with (rfl | pos)
   · simp
   rcases h with ⟨k', hk'⟩
@@ -158,7 +158,7 @@ lemma LenBit.mod {i a k : V} (h : 2 * i ∣ k) : LenBit i (a % k) ↔ LenBit i a
 @[simp] lemma LenBit.mod_two_mul_self {a i : V} : LenBit i (a % (2 * i)) ↔ LenBit i a := LenBit.mod (by simp)
 
 lemma LenBit.add {i a b : V} (h : 2 * i ∣ b) : LenBit i (a + b) ↔ LenBit i a := by
-  have : 0 ≤ i := zero_le i
+  have : 0 ≤ i := Arithmetic.zero_le i
   rcases (eq_or_lt_of_le this) with (rfl | pos)
   · simp
   rcases h with ⟨b', hb'⟩
@@ -307,7 +307,7 @@ lemma four_le {i : V} (hi : Pow2 i) (lt : 2 < i) : 4 ≤ i := by
 
 lemma mul_add_lt_of_mul_lt_of_pos {a b p q : V} (hp : Pow2 p) (hq : Pow2 q)
     (h : a * p < q) (hb : b < p) (hbq : b < q) : a * p + b < q := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [hbq]
   have : p ∣ q :=
     dvd_of_le hp hq (le_of_lt <| lt_of_le_of_lt (le_mul_of_pos_left pos) h)

Foundation/FirstOrder/Arithmetic/HFS/Basic.lean

@@ -64,7 +64,7 @@ lemma sUnion_lt_of_pos {a : V} (ha : 0 < a) : ⋃ʰᶠ a < a :=
     exact lt_of_lt_of_le (lt_of_mem hi) (le_log_of_mem hx)
 
 @[simp] lemma sUnion_le (a : V) : ⋃ʰᶠ a ≤ a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [←emptyset_def]
   · exact le_of_lt (sUnion_lt_of_pos pos)
 

Foundation/FirstOrder/Arithmetic/HFS/PRF.lean

@@ -140,7 +140,7 @@ lemma CSeq.exists (l : V) : ∃ s, c.CSeq v s ∧ l + 1 = lh s := by
   · apply HierarchySymbol.Definable.exs
     apply HierarchySymbol.Definable.and
     · exact ⟨p.cseqDef.rew (Rew.embSubsts <| #0 :> fun i ↦ &(v i)), by
-         intro w; simpa [Matrix.comp_vecCons''] using c.cseq_defined_iff (w 0 :> v)⟩
+         intro w; simpa [Matrix.comp_vecCons''] using! c.cseq_defined_iff (w 0 :> v)⟩
     · definability
   case zero =>
     exact ⟨!⟦c.zero v⟧, CSeq.initial, by simp⟩