awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Field.Basic
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
refine : ∀ (d : α) (d_ab : d < a * b), d ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Algebra.Order.Field.Basic
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
inr : ∀ (hd : 0 ≤ d), d ≤ c
⊢ d ≤ c

Tactic:
rcases lt_or_ge d 0 with hd | hd

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
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 : d < 0
⊢ d ≤ c

Tactic:
hd.le.trans hc

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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 : d < 0
⊢ d ≤ c

Tactic:
exact hd.le.trans hc

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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
inr : ∀ (a' : α) (ha' : a' ∈ Set.Ico 0 a) (d_ab : d < a' * b), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab

Premises used: _private.0.exists_lt_mul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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
inr : ∀ (b' : α) (hb' : b' ∈ Set.Ico 0 b) (d_ab : d < a' * b'), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab

Premises used: _private.0.exists_lt_mul_right_of_nonneg, And.left
-- Module: Mathlib.Algebra.Order.Field.Basic
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_2 : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c

Tactic:
d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)

Premises used: LT.lt.le, And.right, And.left, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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_2 : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c

Tactic:
exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)

Premises used: LT.lt.le, And.right, And.left, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : CommRing α
inst_1 : NoZeroDivisors α
inst_2 : PartialOrder α
inst_3 : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ ∀ (h : 0 ≤ -b), b = 0

Tactic:
have := fun h ↦ le_antisymm (neg_nonneg.mp h) b0
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : CommRing α
inst_1 : NoZeroDivisors α
inst_2 : PartialOrder α
inst_3 : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
this : ∀ (h : 0 ≤ -b), b = 0
⊢ a * a = b * b ↔ a = b

Tactic:
grind [sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg]

Premises used: add_eq_zero_iff_eq_neg, mul_eq_zero, sq_sub_sq
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
hc : c ≤ 0
a b : α
⊢ min (a / c) (b / c) = max a b / c

Tactic:
Eq.symm <| Antitone.map_max fun _ _ => div_le_div_of_nonpos_of_le hc

Premises used: div_le_div_of_nonpos_of_le, Antitone.map_max, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
hc : c ≤ 0
a b : α
⊢ max (a / c) (b / c) = min a b / c

Tactic:
Eq.symm <| Antitone.map_min fun _ _ => div_le_div_of_nonpos_of_le hc

Premises used: div_le_div_of_nonpos_of_le, Antitone.map_min, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ |a⁻¹| = |a|⁻¹

Tactic:
map_inv₀ (absHom : α →*₀ α) a

Premises used: abs, map_inv₀, absHom
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a / b| = |a| / |b|

Tactic:
map_div₀ (absHom : α →*₀ α) a b

Premises used: abs, map_div₀, absHom
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : |1| / |a| = 1 / |a|
rw₁ rw₂ : 1 / |a| = 1 / |a|
⊢ |1 / a| = 1 / |a|

Tactic:
rw [abs_div, abs_one]

Premises used: abs_div, abs_one
-- Module: Mathlib.Algebra.Order.Field.Basic
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| < ε
wlog! : ∀ (B : α) (B_pos : 0 < B), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
wlog! B_pos : 0 < B generalizing B
-- Module: Mathlib.Algebra.Order.Field.Basic
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
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| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
have ⟨δ, δ_pos, cont⟩ := this 1 zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
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
δ : α
δ_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:
⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans (B_pos.trans zero_le_one))⟩

Premises used: zero_le_one, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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
δ : α
δ_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:
exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans (B_pos.trans zero_le_one))⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
⊢ 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
-- Module: Mathlib.Algebra.Order.Field.Basic
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| < ε

Tactic:
⟨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 ?_⟩

Premises used: HMul.hMul, HSub.hSub, lt_min, HDiv.hDiv, Nat.cast, zero_lt_one, HPow.hPow, abs_pow_sub_pow_le, HAdd.hAdd, And.intro, Exists.intro, div_pos, OfNat.ofNat, LE.le.trans_lt, Min.min
-- Module: Mathlib.Algebra.Order.Field.Basic
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)
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) < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

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 ?_⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
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| ≤ 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

Premises used: mul_assoc, le_inf_iff, le_div_iff₀, mul_one_add
-- Module: Mathlib.Algebra.Order.Field.Basic
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) < ε
inr : ∀ (h : 0 < |q - r|), |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε

Tactic:
obtain h | h := (abs_nonneg (q - r)).eq_or_lt

Premises used: LE.le.eq_or_lt, HSub.hSub, abs_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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) < ε

Tactic:
simpa only [← h, zero_mul] using hε

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
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) < ε

Tactic:
(lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2

Premises used: lt_of_le_of_lt, And.right, LT.lt.trans_le, lt_add_of_pos_left
-- Module: Mathlib.Algebra.Order.Field.Basic
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 : |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) < ε

Tactic:
refine (lt_of_le_of_lt ?_ <| lt_add_of_pos_left _ h).trans_le hqr.2

Premises used: lt_of_le_of_lt, And.right, LT.lt.trans_le, lt_add_of_pos_left
-- Module: Mathlib.Algebra.Order.Field.Basic
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|
inr₂ : max |q| |r| ≤ B + 1
⊢ |q - r| * (↑n : α) * max |q| |r| ^ (n - 1) ≤ |q - r| * (↑n : α) * (B + 1) ^ (n - 1)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Field.Basic
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|
⊢ 0 ≤ |q - r| * (↑n : α)

Tactic:
mul_nonneg (abs_nonneg _) n.cast_nonneg

Premises used: mul_nonneg, Nat.cast_nonneg, abs_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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|
⊢ 0 ≤ |q - r| * (↑n : α)

Tactic:
exact mul_nonneg (abs_nonneg _) n.cast_nonneg

Premises used: mul_nonneg, Nat.cast_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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|
⊢ 0 ≤ max |q| |r|

Tactic:
(abs_nonneg _).trans le_sup_left

Premises used: le_sup_left, LE.le.trans, abs_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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|
⊢ 0 ≤ max |q| |r|

Tactic:
exact (abs_nonneg _).trans le_sup_left

Premises used: le_sup_left, LE.le.trans, abs_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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

Tactic:
max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)

Premises used: zero_le_one, le_add_of_nonneg_right, max_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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 : |q| ≤ B + 1
⊢ max |q| |r| ≤ B + 1

Tactic:
refine max_le ?_ (hr.trans <| le_add_of_nonneg_right zero_le_one)

Premises used: zero_le_one, le_add_of_nonneg_right, max_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
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| ≤ B + 1

Tactic:
add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)

Premises used: add_le_add, Eq.rec, add_sub_cancel, And.left, LE.le.trans, abs_add_le
-- Module: Mathlib.Algebra.Order.Field.Basic
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| ≤ B + 1

Tactic:
exact add_sub_cancel r q ▸ (abs_add_le ..).trans (add_le_add hr hqr.1)
-- Module: Mathlib.Algebra.Order.Field.Basic
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

Tactic:
have h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2 := two_mul_le_add_sq (ε * a) b
-- Module: Mathlib.Algebra.Order.Field.Basic
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
rw : 2 * a * b = 2 * a * b * 1
rw₁ rw₂ : 2 * a * b = 2 * a * b
⊢ 2 * a * b = 2 * a * b * (ε * ε⁻¹)

Tactic:
rw [mul_inv_cancel₀ hε.ne', mul_one]

Premises used: mul_inv_cancel₀, LT.lt.ne', mul_one
-- Module: Mathlib.Algebra.Order.Field.Basic
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
simp_rw : 2 * (a * (b * (ε * ε⁻¹))) = 2 * (ε * (a * (b * ε⁻¹)))
simp_rw₁ : 2 * (a * (b * (ε⁻¹ * ε))) = 2 * (a * (b * ε⁻¹) * ε)
⊢ 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹

Tactic:
simp_rw [mul_assoc, mul_comm ε, mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
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
ha : 0 ≤ ε⁻¹
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Field.Basic
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
⊢ 0 ≤ ε⁻¹

Tactic:
inv_nonneg.mpr hε.le

Premises used: Iff.mpr, LT.lt.le, inv_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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
⊢ 0 ≤ ε⁻¹

Tactic:
exact inv_nonneg.mpr hε.le

Premises used: Iff.mpr, LT.lt.le, inv_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
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
rw :
  ε⁻¹ * (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₁ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₂ :
  ε⁻¹ * (HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2) + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₃ :
  ε⁻¹ * HPow.hPow (β := ℕ) ε 2 * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₄ :
  ε⁻¹ * (ε * ε) * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₅ :
  ε⁻¹ * ε * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₆ :
  1 * ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
rw₇ rw₈ :
  ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2 = ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2

Tactic:
rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]

Premises used: pow_two, mul_assoc, LT.lt.ne', Inv.inv, mul_comm, mul_add, mul_pow, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
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
calc : 2 * a * b = 2 * a * b * (ε * ε⁻¹)
calc₁ : 2 * a * b * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹
calc₂ : 2 * (ε * a) * b * ε⁻¹ ≤ (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹
calc₃ :
  (HPow.hPow (β := ℕ) (ε * a) 2 + HPow.hPow (β := ℕ) b 2) * ε⁻¹ =
    ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2
⊢ 2 * a * b ≤ ε * HPow.hPow (β := ℕ) a 2 + ε⁻¹ * HPow.hPow (β := ℕ) b 2

Tactic:
calc 2 * a * b
  _ = 2 * a * b * (ε * ε⁻¹) := by rw [mul_inv_cancel₀ hε.ne', mul_one]
  _ = (2 * (ε * a) * b) * ε⁻¹ := by simp_rw [mul_assoc, mul_comm ε, mul_assoc]
  _ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹ := by gcongr; exact inv_nonneg.mpr hε.le
  _ = ε * a ^ 2 + ε⁻¹ * b ^ 2 := by
    rw [mul_comm _ ε⁻¹, mul_pow, mul_add, ← mul_assoc, pow_two, ← mul_assoc, inv_mul_cancel₀ hε.ne',
      one_mul]

Premises used: HMul.hMul, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : GroupWithZero α
inst_1 : PartialOrder α
a b : α
inst_2 : PosMulReflectLT α
ha : 0 < a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
div_nonneg ha.le hb

Premises used: LT.lt.le, div_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : GroupWithZero α
inst_1 : PartialOrder α
a b : α
inst_2 : PosMulReflectLT α
ha : 0 ≤ a
hb : 0 < b
⊢ 0 ≤ a / b

Tactic:
div_nonneg ha hb.le

Premises used: LT.lt.le, div_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : GroupWithZero α
inst_1 : PartialOrder α
a b : α
ha : 0 < a
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
div_ne_zero ha.ne' hb

Premises used: div_ne_zero, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : GroupWithZero α
inst_1 : PartialOrder α
a b : α
ha : a ≠ 0
hb : 0 < b
⊢ a / b ≠ 0

Tactic:
div_ne_zero ha hb.ne'

Premises used: div_ne_zero, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_5
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 0 < HPow.hPow (β := ℤ) a 0

Tactic:
zero_lt_one.trans_eq (zpow_zero a).symm

Premises used: zpow_zero, LT.lt.trans_eq, zero_lt_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Canonical
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : IsStrictOrderedRing α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
simp_rw : (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv, tsub_mul]

Premises used: div_eq_mul_inv, tsub_mul
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x y : K
h : y < x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_ge h.le n)

Premises used: eq_div_of_mul_eq, LT.lt.le, LT.lt.ne', geom_sum₂_mul_of_ge, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x y : K
h : x < y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (y ^ n - x ^ n) / (y - x)

Tactic:
eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum₂_mul_of_le h.le n)

Premises used: eq_div_of_mul_eq, LT.lt.le, geom_sum₂_mul_of_le, LT.lt.ne', tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Field.GeomSum
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : CanonicallyOrderedAdd K
inst_4 : Sub K
inst_5 : OrderedSub K
x : K
h : 1 < x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1)

Tactic:
eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_one_le h.le n)

Premises used: eq_div_of_mul_eq, LT.lt.le, LT.lt.ne', geom_sum_mul_of_one_le, tsub_pos_of_lt