awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ HSub.hSub (α := α) 1 2⁻¹
have h : HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹
Tactic: convert! (one_div a).le.trans (inv_anti₀ zero_lt_two a2) using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹
have h : 1 = HAdd.hAdd (α := α) 2⁻¹ 2⁻¹
Tactic: rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
h : 1 = HAdd.hAdd (α := α) 2⁻¹ 2⁻¹
⊢ HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹
have h₁ : 1 = HMul.hMul (α := α) 2 2⁻¹
Tactic: rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
h : 1 = HAdd.hAdd (α := α) 2⁻¹ 2⁻¹
h₁ : 1 = HMul.hMul (α := α) 2 2⁻¹
⊢ HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹
have h₂ : Eq.{u_2 + 1} (α := α) 1 1
Tactic: rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
have rw : (a * d - c * b) / (c * d) < 0 ↔ a / c < b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) < 0 ↔ a / c < b / d
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
have rw₁ : a / c - b / d < 0 ↔ a / c < b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) < 0 ↔ a / c < b / d
rw₁ : a / c - b / d < 0 ↔ a / c < b / d
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
have rw₂ : a / c < b / d ↔ a / c < b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
have rw : (a * d - c * b) / (c * d) ≤ 0 ↔ a / c ≤ b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) ≤ 0 ↔ a / c ≤ b / d
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
have rw₁ : a / c - b / d ≤ 0 ↔ a / c ≤ b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) ≤ 0 ↔ a / c ≤ b / d
rw₁ : a / c - b / d ≤ 0 ↔ a / c ≤ b / d
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
have rw₂ : a / c ≤ b / d ↔ a / c ≤ b / d
Tactic: rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
have inl : ∀ (hb : b < 0), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
have inr : 1 < a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
inr : 1 < a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
have inr₁ : ∀ (hb : 0 < b), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
have inl : ∀ (hb : b < 0), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
have inr : 1 ≤ a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
inr : 1 ≤ a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
have inr₁ : ∀ (hb : 0 < b), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
have inl : ∀ (hb : b < 0), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
have inr : a / 0 < 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
inr : a / 0 < 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
have inr₁ : ∀ (hb : 0 < b), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
have inl : ∀ (hb : b < 0), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
have inr : a / 0 ≤ 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
inr : a / 0 ≤ 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
have inr₁ : ∀ (hb : 0 < b), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
Tactic: rcases lt_trichotomy b 0 with (hb | rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : ∀ ε > 0, b - ε ≤ a
⊢ b ≤ a
have contrapose! : ∀ (h : a < b), ∃ ε > 0, a < b - ε
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b
have hb : 0 < b
Tactic: have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b
have obtain : ∀ (a' : α) (ha' : c / b < a') (a_a' : a' < a), ∃ a' ∈ Set.Ico 0 a, c < a' * b
Tactic: obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'
have hb : 0 < b
Tactic: have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'
have simp_rw : ∀ (h : c < b * a), ∃ b' ∈ Set.Ico 0 b, c < b' * a
Tactic: simp_rw [mul_comm a] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ a' > a, a' * b < c
have inl : ∀ (hb : b ≤ 0), ∃ a' > a, a' * b < c
Tactic: rcases le_or_gt b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
inl : ∀ (hb : b ≤ 0), ∃ a' > a, a' * b < c
⊢ ∃ a' > a, a' * b < c
have inr : ∀ (hb : 0 < b), ∃ a' > a, a' * b < c
Tactic: rcases le_or_gt b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c
have inl : ∀ (a' : α) (ha' : a < a'), ∃ a' > a, a' * b < c
Tactic: obtain ⟨a', ha'⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c
have inr : ∀ (a' : α) (ha' : a < a') (hc' : a' < c / b), ∃ a' > a, a' * b < c
Tactic: obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ b' > b, a * b' < c
have simp_rw : ∀ (hc : b * a < c), ∃ b' > b, b' * a < c
Tactic: simp_rw [mul_comm a] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b
have refine : ∀ (d : α) (hd : a * b < d), c ≤ d
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d
have obtain : ∀ (a' : α) (ha' : a' > a) (hd : a' * b < d), c ≤ d
Tactic: obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d
have obtain : ∀ (b' : α) (hb' : b' > b) (hd : a' * b' < d), c ≤ d
Tactic: obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
⊢ a * b ≤ c
have refine : ∀ (d : α) (d_ab : d < a * b), d ≤ c
Tactic: refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
⊢ d ≤ c
have inl : ∀ (hd : d < 0), d ≤ c
Tactic: rcases lt_or_ge d 0 with hd | hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
inl : ∀ (hd : d < 0), d ≤ c
⊢ d ≤ c
have inr : ∀ (hd : 0 ≤ d), d ≤ c
Tactic: rcases lt_or_ge d 0 with hd | hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c
have inr : ∀ (a' : α) (ha' : a' ∈ Set.Ico 0 a) (d_ab : d < a' * b), d ≤ c
Tactic: obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab_1 : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab : d < a' * b
⊢ d ≤ c
have inr : ∀ (b' : α) (hb' : b' ∈ Set.Ico 0 b) (d_ab : d < a' * b'), d ≤ c
Tactic: obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_4
inst : CommRing α
inst_1 : NoZeroDivisors α
inst_2 : PartialOrder α
inst_3 : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ a * a = b * b ↔ a = b
have this : ∀ (h : 0 ≤ -b), b = 0
Tactic: have := fun h ↦ le_antisymm (neg_nonneg.mp h) b0
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ |1 / a| = 1 / |a|
have rw : |1| / |a| = 1 / |a|
Tactic: rw [abs_div, abs_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : |1| / |a| = 1 / |a|
⊢ |1 / a| = 1 / |a|
have rw₁ : 1 / |a| = 1 / |a|
Tactic: rw [abs_div, abs_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
have inr : ∀ (this : ∀ (B : α) (B_pos : 0 < B), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε) (B_pos : B ≤ 0),
  ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Tactic: wlog! B_pos : 0 < B generalizing B
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
inr :
  ∀ (this : ∀ (B : α) (B_pos : 0 < B), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε)
    (B_pos : B ≤ 0), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
have wlog! : ∀ (B : α) (B_pos : 0 < B), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Tactic: wlog! B_pos : 0 < B generalizing B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α) (B_pos : 0 < B), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : B ≤ 0
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
have inr : ∀ (δ : α) (δ_pos : δ > 0) (cont : ∀ (q r : α), |r| ≤ 1 → |q - r| ≤ δ → |q ^ n - r ^ n| < ε),
  ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
Tactic: have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
have pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
Tactic: have pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1) := zero_lt_one.trans_le <| le_add_of_nonneg_right <|
    mul_nonneg n.cast_nonneg <| (pow_pos (B_pos.trans <| lt_add_of_pos_right _ zero_lt_one) _).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
have refine : ∀ (q r : α) (hr : |r| ≤ B) (hqr : |q - r| ≤ min 1 (ε / (1 + (↑n : α) * (B + 1) ^ (n - 1)))),
  |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
Tactic: refine ⟨min 1 (ε / (1 + n * (B + 1) ^ (n - 1))), lt_min zero_lt_one (div_pos hε pos),
    fun q r hr hqr ↦ (abs_pow_sub_pow_le ..).trans_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ min 1 (ε / (1 + (↑n : α) * (B + 1) ^ (n - 1)))
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
have hqr₁ : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
Tactic: rw [le_inf_iff, le_div_iff₀ pos, mul_one_add, ← mul_assoc] at hqr
Cleared hypotheses: hqr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
have inl : ∀ (h : 0 = |q - r|), |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
Tactic: obtain h | h := (abs_nonneg (q - r)).eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
inl : ∀ (h : 0 = |q - r|), |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
have inr : ∀ (h : 0 < |q - r|), |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
Tactic: obtain h | h := (abs_nonneg (q - r)).eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
have inr : |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)
Tactic: refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)
have inr : 0 ≤ |q - r| * (↑n : α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
inr : 0 ≤ |q - r| * (↑n : α)
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)
have inr₁ : 0 ≤ max |q| |r|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
inr : 0 ≤ |q - r| * (↑n : α)
inr₁ : 0 ≤ max |q| |r|
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)
have inr₂ : max |q| |r| ≤ B + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + (↑n : α) * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * (↑n : α) * (B + 1) ^ (n - 1) ≤ ε
h : 0 < |q - r|
⊢ max |q| |r| ≤ B + 1
have inr : |q| ≤ B + 1
Tactic: refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
have h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
Tactic: have h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2 := two_mul_le_add_sq (ε * a) b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)
have rw : 2 * a * b = 2 * a * b * 1
Tactic: rw [mul_inv_cancel₀ hε.ne', mul_one]