refactor: define < on WithBot/WithTop as an inductive predicate (#30848)

Follow up to #19668, where I did the same for `LE` but forgot to do it for `LT`.

Author: YaelDillies

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -284,15 +284,18 @@ variable [LT α] {x y : WithZero α} {a b : α}
 /-- The order on `WithZero α`, defined by `⊥ < ↑a` and `a < b → ↑a < ↑b`. -/
 instance (priority := 10) instLT : LT (WithZero α) := WithBot.instLT
 
-lemma lt_def : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b := WithBot.lt_def
+lemma lt_def : x < y ↔ x = 0 ∧ (∃ b : α, y = b) ∨ ∃ a b : α, a < b ∧ x = ↑a ∧ y = ↑b :=
+  WithBot.lt_def
+
+lemma lt_iff_exists : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b := WithBot.lt_iff_exists
 
 @[simp, norm_cast] lemma coe_lt_coe : (a : WithZero α) < b ↔ a < b := by simp [lt_def]
 @[simp] lemma zero_lt_coe (a : α) : 0 < (a : WithZero α) := by simp [lt_def]
 @[simp] protected lemma not_lt_zero (a : WithZero α) : ¬a < 0 := by simp [lt_def]
 
 lemma lt_iff_exists_coe : x < y ↔ ∃ b : α, y = b ∧ x < b := WithBot.lt_iff_exists_coe
 
-lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := by simp [lt_def]
+lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := WithBot.lt_coe_iff
 
 /-- A version of `pos_iff_ne_zero` for `WithZero` that only requires `LT α`,
 not `PartialOrder α`. -/

Mathlib/Analysis/Analytic/OfScalars.lean

@@ -268,7 +268,7 @@ theorem ofScalars_radius_eq_zero_of_tendsto [NormOneClass E]
   rw [← coe_zero, coe_le_coe]
   have := FormalMultilinearSeries.summable_norm_mul_pow _ hr
   contrapose! this
-  apply not_summable_of_ratio_norm_eventually_ge ENNReal.one_lt_two
+  refine not_summable_of_ratio_norm_eventually_ge (r := 2) (by simp) ?_ ?_
   · contrapose! hc
     apply not_tendsto_atTop_of_tendsto_nhds (a:=0)
     rw [not_frequently] at hc

Mathlib/Analysis/Oscillation.lean

@@ -125,7 +125,7 @@ theorem uniform_oscillationWithin (comp : IsCompact K) (hK : ∀ x ∈ K, oscill
       intro r' hr'
       grw [← hn₂, ← image_subset_iff.2 hr, hr']
     by_cases r_top : r = ⊤
-    · use 1, one_pos, 2, ENNReal.one_lt_two, this 2 (by simp only [r_top, le_top])
+    · exact ⟨1, one_pos, 2, by simp, this 2 (by simp only [r_top, le_top])⟩
     · obtain ⟨r', hr'⟩ := exists_between (toReal_pos (ne_of_gt r0) r_top)
       use r', hr'.1, r.toReal, hr'.2, this r.toReal ofReal_toReal_le
   have S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁ :=

Mathlib/Order/WithBot.lean

@@ -247,16 +247,17 @@ section LE
 
 variable [LE α] {x y : WithBot α}
 
-/-- The order on `WithBot α`, defined by `⊥ ≤ ⊥`, `⊥ ≤ ↑a` and `a ≤ b → ↑a ≤ ↑b`.
-
-Equivalently, `x ≤ y` can be defined as `∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b`,
-see `le_if_forall`. The definition as an inductive predicate is preferred since it
-cannot be accidentally unfolded too far. -/
+/-- Auxiliary definition for the order on `WithBot`. -/
 @[mk_iff le_def_aux]
 protected inductive LE : WithBot α → WithBot α → Prop
   | protected bot_le (x : WithBot α) : WithBot.LE ⊥ x
   | protected coe_le_coe {a b : α} : a ≤ b → WithBot.LE a b
 
+/-- The order on `WithBot α`, defined by `⊥ ≤ y` and `a ≤ b → ↑a ≤ ↑b`.
+
+Equivalently, `x ≤ y` can be defined as `∀ a : α, x = ↑a → ∃ b : α, y = ↑b ∧ a ≤ b`,
+see `le_iff_forall`. The definition as an inductive predicate is preferred since it
+cannot be accidentally unfolded too far. -/
 instance (priority := 10) instLE : LE (WithBot α) where le := WithBot.LE
 
 lemma le_def : x ≤ y ↔ x = ⊥ ∨ ∃ a b : α, a ≤ b ∧ x = a ∧ y = b := le_def_aux ..
@@ -303,28 +304,32 @@ section LT
 
 variable [LT α] {x y : WithBot α}
 
+/-- Auxiliary definition for the order on `WithBot`. -/
+@[mk_iff lt_def_aux]
+protected inductive LT : WithBot α → WithBot α → Prop
+  | protected bot_lt (b : α) : WithBot.LT ⊥ b
+  | protected coe_lt_coe {a b : α} : a < b → WithBot.LT a b
+
 /-- The order on `WithBot α`, defined by `⊥ < ↑a` and `a < b → ↑a < ↑b`.
 
-Equivalently, `x ≤ y` can be defined as `∀ b : α, y = ↑v → ∃ a : α, x = ↑a ∧ a ≤ b`,
-see `le_if_forall`. The definition as an inductive predicate is preferred since it
+Equivalently, `x < y` can be defined as `∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b`,
+see `lt_iff_exists`. The definition as an inductive predicate is preferred since it
 cannot be accidentally unfolded too far. -/
-instance (priority := 10) instLT : LT (WithBot α) where
-  lt
-  | ⊥, ⊥ => False
-  | (a : α), ⊥ => False
-  | ⊥, (b : α) => True
-  | (a : α), (b : α) => a < b
+instance (priority := 10) instLT : LT (WithBot α) where lt := WithBot.LT
+
+lemma lt_def : x < y ↔ (x = ⊥ ∧ ∃ b : α, y = b) ∨ ∃ a b : α, a < b ∧ x = a ∧ y = b :=
+  (lt_def_aux ..).trans <| by simp
 
-lemma lt_def : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b := by
-  cases x <;> cases y <;> simp [LT.lt]
+lemma lt_iff_exists : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b := by
+  cases x <;> cases y <;> simp [lt_def]
 
 @[simp, norm_cast] lemma coe_lt_coe : (a : WithBot α) < b ↔ a < b := by simp [lt_def]
 @[simp] lemma bot_lt_coe (a : α) : ⊥ < (a : WithBot α) := by simp [lt_def]
 @[simp] protected lemma not_lt_bot (a : WithBot α) : ¬a < ⊥ := by simp [lt_def]
 
 lemma lt_iff_exists_coe : x < y ↔ ∃ b : α, y = b ∧ x < b := by cases y <;> simp
 
-lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := by simp [lt_def]
+lemma lt_coe_iff : x < b ↔ ∀ a : α, x = a → a < b := by simp [lt_iff_exists]
 
 /-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
 `PartialOrder α`. -/
@@ -827,7 +832,11 @@ section LE
 
 variable [LE α] {x y : WithTop α}
 
-/-- The order on `WithTop α`, defined by `⊤ ≤ ⊤`, `↑a ≤ ⊤` and `a ≤ b → ↑a ≤ ↑b`. -/
+/-- The order on `WithTop α`, defined by `x ≤ ⊤` and `a ≤ b → ↑a ≤ ↑b`.
+
+Equivalently, `x ≤ y` can be defined as `∀ b : α, y = ↑b → ∃ a : α, x = ↑a ∧ a ≤ b`,
+see `le_iff_forall`. The definition as an inductive predicate is preferred since it
+cannot be accidentally unfolded too far. -/
 instance (priority := 10) instLE : LE (WithTop α) where le a b := WithBot.LE (α := αᵒᵈ) b a
 
 lemma le_def : x ≤ y ↔ y = ⊤ ∨ ∃ a b : α, a ≤ b ∧ x = a ∧ y = b :=
@@ -896,25 +905,27 @@ section LT
 
 variable [LT α] {x y : WithTop α}
 
-/-- The order on `WithTop α`, defined by `↑a < ⊤` and `a < b → ↑a < ↑b`. -/
-instance (priority := 10) instLT : LT (WithTop α) where
-  -- We match on `b, a` rather than `a, b` to keep the defeq with `WithBot.instLT (α := αᵒᵈ)`
-  lt a b := match b, a with
-  | ⊤, ⊤ => False
-  | (b : α), ⊤ => False
-  | ⊤, (a : α) => True
-  | (b : α), (a : α) => a < b
+/-- The order on `WithTop α`, defined by `↑a < ⊤` and `a < b → ↑a < ↑b`.
+
+Equivalently, `x < y` can be defined as `∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b`,
+see `le_if_forall`. The definition as an inductive predicate is preferred since it
+cannot be accidentally unfolded too far. -/
+instance (priority := 10) instLT : LT (WithTop α) where lt a b := WithBot.LT (α := αᵒᵈ) b a
+
+lemma lt_def : x < y ↔ (∃ a : α, x = ↑a) ∧ y = ⊤ ∨ ∃ a b : α, a < b ∧ x = ↑a ∧ y = ↑b :=
+  WithBot.lt_def.trans <| or_congr and_comm <| exists_swap.trans <|
+    exists₂_congr fun _ _ ↦ and_congr_right' and_comm
 
-lemma lt_def : x < y ↔ ∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b := by
-  cases x <;> cases y <;> simp [LT.lt]
+lemma lt_iff_exists : x < y ↔ ∃ a : α, x = ↑a ∧ ∀ b : α, y = ↑b → a < b := by
+  cases x <;> cases y <;> simp [lt_def]
 
 @[simp, norm_cast] lemma coe_lt_coe : (a : WithTop α) < b ↔ a < b := by simp [lt_def]
 @[simp] lemma coe_lt_top (a : α) : (a : WithTop α) < ⊤ := by simp [lt_def]
 @[simp] protected lemma not_top_lt (a : WithTop α) : ¬⊤ < a := by simp [lt_def]
 
 lemma lt_iff_exists_coe : x < y ↔ ∃ a : α, x = a ∧ a < y := by cases x <;> simp
 
-lemma coe_lt_iff : a < y ↔ ∀ b : α, y = b → a < b := by simp [lt_def]
+lemma coe_lt_iff : a < y ↔ ∀ b : α, y = b → a < b := by simp [lt_iff_exists]
 
 /-- A version of `lt_top_iff_ne_top` for `WithTop` that only requires `LT α`, not
 `PartialOrder α`. -/

Mathlib/RingTheory/PowerBasis.lean

@@ -108,13 +108,12 @@ theorem mem_span_pow {x y : S} {d : ℕ} (hd : d ≠ 0) :
       ∃ f : R[X], f.natDegree < d ∧ y = aeval x f := by
   rw [mem_span_pow']
   constructor <;>
-    · rintro ⟨f, h, hy⟩
-      refine ⟨f, ?_, hy⟩
-      by_cases hf : f = 0
-      · simp only [hf, natDegree_zero, degree_zero] at h ⊢
-        first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
-      simp_all only [degree_eq_natDegree hf]
-      · exact WithBot.coe_lt_coe.1 h
+  · rintro ⟨f, h, hy⟩
+    refine ⟨f, ?_, hy⟩
+    by_cases hf : f = 0
+    · simp only [hf, natDegree_zero, degree_zero] at h ⊢
+      first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
+    simpa [degree_eq_natDegree hf] using h
 
 theorem dim_ne_zero [Nontrivial S] (pb : PowerBasis R S) : pb.dim ≠ 0 := fun h =>
   not_nonempty_iff.mpr (h.symm ▸ Fin.isEmpty : IsEmpty (Fin pb.dim)) pb.basis.index_nonempty