docs: nest doc-gen4 in a docbuild/ sub-project (mathlib pattern)

.github/workflows/ci.yml

@@ -54,7 +54,7 @@ jobs:
         run: lake build Foundation
 
       - name: Build docs
-        run: lake build Foundation:docs
+        run: cd docbuild && lake build Foundation:docs
 
       - name: Pack project cache
         run: lake pack
@@ -78,7 +78,7 @@ jobs:
         with:
           name: lean-artifacts
           path: |
-            .lake/build/doc
+            docbuild/.lake/build/doc
             import_graph.png
             import_graph.pdf
             import_graph.html
@@ -138,7 +138,7 @@ jobs:
           name: lean-artifacts
       - name: Copy from artifacts to pages
         run: |
-          cp -r "$GITHUB_WORKSPACE/.lake/build/doc" pages/docs
+          cp -r "$GITHUB_WORKSPACE/docbuild/.lake/build/doc" pages/docs
           cp "$GITHUB_WORKSPACE/import_graph.png" \
              "$GITHUB_WORKSPACE/import_graph.pdf" \
              "$GITHUB_WORKSPACE/import_graph.html" \

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/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

@@ -142,7 +142,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'⟩
@@ -159,7 +159,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'⟩
@@ -308,7 +308,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/IOpen/Basic.lean

@@ -124,14 +124,14 @@ lemma div_mul_add (a b : V) {r} (hr : r < b) : (a * b + r) / b = a :=
 lemma div_mul_add' (a b : V) {r} (hr : r < b) : (b * a + r) / b = a := by simpa [mul_comm] using div_mul_add a b hr
 
 @[simp] lemma zero_div (a : V) : 0 / a = 0 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · exact div_eq_of (by simp) (by simpa)
 
 lemma div_mul (a b c : V) : a / (b * c) = a / b / c := by
-  rcases zero_le b with (rfl | hb)
+  rcases Arithmetic.zero_le b with (rfl | hb)
   · simp
-  rcases zero_le c with (rfl | hc)
+  rcases Arithmetic.zero_le c with (rfl | hc)
   · simp
   exact div_eq_of
     (by calc
@@ -142,14 +142,14 @@ lemma div_mul (a b c : V) : a / (b * c) = a / b / c := by
           _ ≤ b * c * (a / b / c + 1) := by simpa [mul_assoc] using mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc))
 
 @[simp] lemma mul_div_le (a b : V) : b * (a / b) ≤ a := by
-  have : 0 ≤ b := by exact zero_le b
+  have : 0 ≤ b := by exact Arithmetic.zero_le b
   rcases this with (rfl | pos)
   · simp
   · rcases eq_mul_div_add_of_pos a pos with ⟨v, _, e⟩
     simpa [← e] using show b * (a / b) ≤ b * (a / b) + v from le_self_add
 
 @[simp] lemma div_le (a b : V) : a / b ≤ a := by
-  have : 0 ≤ b := zero_le b
+  have : 0 ≤ b := Arithmetic.zero_le b
   rcases this with (rfl | pos)
   · simp
   · have : 1 * (a / b) ≤ b * (a / b) := mul_le_mul_of_nonneg_right (le_iff_lt_succ.mpr (by simp [pos])) (by simp)
@@ -192,7 +192,7 @@ lemma div_mul_add_self' (a c : V) {b} (pos : 0 < b) : (b * a + c) / b = a + c /
   simpa using div_mul_add 0 b h
 
 @[simp] lemma div_sq (a : V) : a^2 / a = a := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · simp [sq, pos]
 
@@ -208,14 +208,14 @@ lemma div_mul_add_self' (a c : V) {b} (pos : 0 < b) : (b * a + c) / b = a + c /
   simpa using div_add_mul_self a 1 pos
 
 lemma mul_div_self_of_dvd {a b : V} : a * (b / a) = b ↔ a ∣ b := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp [eq_comm]
   · constructor
     · intro e; rw [←e]; simp
     · rintro ⟨r, rfl⟩; simp [pos]
 
 lemma div_lt_of_pos_of_one_lt {a b : V} (ha : 0 < a) (hb : 1 < b) : a / b < a := by
-  rcases zero_le (a / b) with (e | lt)
+  rcases Arithmetic.zero_le (a / b) with (e | lt)
   · simp [←e, ha]
   · exact lt_of_lt_of_le (lt_mul_of_one_lt_left lt hb) (mul_div_le a b)
 
@@ -224,7 +224,7 @@ lemma le_two_mul_div_two_add_one (a : V) : a ≤ 2 * (a / 2) + 1 := by
   exact le_iff_lt_succ.mpr (by simpa [add_assoc, one_add_one_eq_two, mul_add] using this)
 
 lemma div_monotone {a b : V} (h : a ≤ b) (c : V) : a / c ≤ b / c := by
-  rcases zero_le c with (rfl | pos)
+  rcases Arithmetic.zero_le c with (rfl | pos)
   · simp
   by_contra A
   have : b / c + 1 ≤ a / c := succ_le_iff_lt.mpr (by simpa using A)
@@ -280,7 +280,7 @@ lemma div_add_mod (a b : V) : b * (a / b) + (a % b) = a :=
 @[simp] lemma zero_mod (a : V) : 0 % a = 0 := by simp [mod_def]
 
 @[simp] lemma mod_self (a : V) : a % a = 0 := by
-  rcases zero_le a with (rfl | h)
+  rcases Arithmetic.zero_le a with (rfl | h)
   · simp
   · simp [mod_def, h]
 
@@ -300,7 +300,7 @@ lemma mod_mul_add_of_lt (a b : V) {r} (hr : r < b) : (a * b + r) % b = r := by
   simp [mul_comm b a, pos]
 
 @[simp] lemma mod_mul_self_left (a b : V) : (a * b) % b = 0 := by
-  rcases zero_le b with (rfl | h)
+  rcases Arithmetic.zero_le b with (rfl | h)
   · simp
   · simpa using mod_mul_add_of_lt a b h
 
@@ -349,7 +349,7 @@ lemma mod_mul {a b m : V} (pos : 0 < m) : (a * b) % m = ((a % m) * (b % m)) % m
   _           = ((a % m) * (b % m)) % m                               := by simp [add_mul, mul_add, pos, mul_left_comm _ m, add_assoc, mul_assoc]
 
 @[simp] lemma mod_div (a b : V) : a % b / b = 0 := by
-  rcases zero_le b with (rfl | pos)
+  rcases Arithmetic.zero_le b with (rfl | pos)
   · simp
   · exact div_eq_zero_of_lt b (by simp [pos])
 
@@ -780,7 +780,7 @@ lemma polynomial_induction [V ⊧ₘ* 𝗣𝗔⁻] (Γ m) [V ⊧ₘ* 𝗜𝗡
   · exact hP
   case inst => exact inferInstance
   case ind x IH =>
-    rcases zero_le x with (rfl | pos)
+    rcases Arithmetic.zero_le x with (rfl | pos)
     · exact zero
     · have : x / 2 < x := div_lt_of_pos_of_one_lt pos one_lt_two
       rcases even_or_odd' x with (hx | hx)

Foundation/FirstOrder/Arithmetic/Induction.lean

@@ -39,7 +39,7 @@ theorem bounded_all_sigma1_order_induction {f : V → V → V} (hf : 𝚺₁-Fun
     rcases sigma₁_replacement₂ hf (under (x + 1)) (under (y + 1)) |>.exists with ⟨m, hm⟩
     exact ⟨m, fun x' hx' y' hy' ↦
       le_of_lt <| lt_of_mem <| hm (f x' y') |>.mpr
-        ⟨x', by simpa [lt_succ_iff_le] using hx', y', by simpa [lt_succ_iff_le] using hy', rfl⟩⟩
+        ⟨x', by simpa [lt_succ_iff_le] using! hx', y', by simpa [lt_succ_iff_le] using! hy', rfl⟩⟩
   intro x y
   have : ∀ k ≤ x, ∃ W, Seq W ∧ k + 1 = lh W ∧
       ⟪0, y⟫ ∈ W ∧

Foundation/FirstOrder/Arithmetic/Omega1/Basic.lean

@@ -93,7 +93,7 @@ lemma smash_comm (a b : V) : a ⨳ b = b ⨳ a := (exponential_smash a b).uniq (
   exact lt_exponential_length this
 
 @[simp] lemma lt_smash_one_righs (a : V) : a ⨳ 1 ≤ 2 * a + 1 := by
-  rcases zero_le a with (rfl | pos)
+  rcases Arithmetic.zero_le a with (rfl | pos)
   · simp
   · exact (le_iff_lt_length_of_exp (exponential_smash a 1)).mpr (by
       suffices ‖a‖ < ‖a * 2 + 1‖ by simpa [mul_comm 2 a]
@@ -120,7 +120,7 @@ lemma smash_two_mul (a : V) {b} (pos : 0 < b) : a ⨳ (2 * b) = (a ⨳ b) * (a 
   exact h₁.uniq h₂
 
 lemma smash_two_mul_le_sq_smash (a b : V) : a ⨳ (2 * b) ≤ (a ⨳ b) ^ 2 := by
-  rcases zero_le b with (rfl | pos)
+  rcases Arithmetic.zero_le b with (rfl | pos)
   · simp
   · simpa [smash_two_mul a pos, sq]
     using smash_monotone (by rfl) (pos_iff_one_le.mp pos)