awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

Premises used: true_or, neg_neg, abs_of_nonpos, abs_of_nonneg, neg_mul, or_true, mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : α
n : ℕ
⊢ |a ^ n| = |a| ^ n

Tactic:
(absHom.toMonoidHom : α →* α).map_pow _ _

Premises used: abs, MonoidWithZeroHom.toMonoidHom, absHom, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : α
n : ℕ
⊢ |a| ^ n = |a ^ n|

Tactic:
(abs_pow a n).symm

Premises used: Eq.symm, abs_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
hn : Even n
a : α
rw : 0 ≤ a ^ n
⊢ |a| ^ n = a ^ n

Tactic:
rw [← abs_pow, abs_eq_self]

Premises used: abs_eq_self, abs_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
hn.pow_nonneg _

Premises used: Even.pow_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
exact hn.pow_nonneg _

Premises used: Even.pow_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
rw : HPow.hPow (α := α) |(-1)| n = 1
rw₁ : HPow.hPow (α := α) |1| n = 1
rw₂ : HPow.hPow (α := α) 1 n = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) 1 1
⊢ |HPow.hPow (α := α) (-1) n| = 1

Tactic:
rw [← pow_abs, abs_neg, abs_one, one_pow]

Premises used: one_pow, abs_neg, pow_abs, abs_one
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a : α
⊢ |a| * |a| = a * a

Tactic:
abs_by_cases (fun x => x * x = a * a) rfl (neg_mul_neg a a)

Premises used: HMul.hMul, abs_by_cases, neg_mul_neg, Eq, rfl
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : α
⊢ |a * a| = a * a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
a : α
⊢ HPow.hPow (β := ℕ) |a| 2 = HPow.hPow (β := ℕ) a 2

Tactic:
simpa only [sq] using abs_mul_abs_self a

Premises used: sq, abs_mul_abs_self
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
x : α
⊢ |HPow.hPow (β := ℕ) x 2| = HPow.hPow (β := ℕ) x 2

Tactic:
simpa only [sq] using abs_mul_self x

Premises used: abs_mul_self, sq
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
a : α
⊢ 1 ≤ |a| + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a| ^ n = HPow.hPow (α := α) 1 n ↔ |a| = 1

Tactic:
pow_left_inj₀ (abs_nonneg a) zero_le_one h

Premises used: pow_left_inj₀, zero_le_one, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
h₁ : |a ^ n| = |a| ^ n
h₂ : 1 = HPow.hPow (α := α) 1 n
⊢ |a ^ n| = 1 ↔ |a| = 1

Tactic:
convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h

Premises used: pow_left_inj₀, zero_le_one, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

Tactic:
(pow_abs _ _).symm

Premises used: pow_abs, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ 1 = HPow.hPow (α := α) 1 n

Tactic:
(one_pow _).symm

Premises used: one_pow, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

Tactic:
exacts [(pow_abs _ _).symm, (one_pow _).symm]

Premises used: one_pow, pow_abs, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
rw : |a| = |b| ↔ |a| * |a| = |b| * |b|
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Premises used: abs_mul_abs_self
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|

Tactic:
(mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

Premises used: abs_nonneg, Iff.symm, mul_self_inj
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|

Tactic:
exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

Premises used: abs_nonneg, Iff.symm, mul_self_inj
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
rw : |a| < |b| ↔ |a| * |a| < |b| * |b|
⊢ |a| < |b| ↔ a * a < b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Premises used: abs_mul_abs_self
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|

Tactic:
mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Premises used: mul_self_lt_mul_self_iff, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|

Tactic:
exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Premises used: mul_self_lt_mul_self_iff, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
rw : |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
⊢ |a| ≤ |b| ↔ a * a ≤ b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Premises used: abs_mul_abs_self
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|

Tactic:
mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Premises used: mul_self_le_mul_self_iff, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|

Tactic:
exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Premises used: mul_self_le_mul_self_iff, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ |a| ≤ 1 ↔ a * a ≤ 1

Tactic:
simpa only [abs_one, one_mul] using abs_le_iff_mul_self_le (a := a) (b := 1)

Premises used: abs_one, one_mul, abs_le_iff_mul_self_le
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2 ↔ |a| < |b|

Tactic:
simpa only [sq_abs] using sq_lt_sq₀ (abs_nonneg a) (abs_nonneg b)

Premises used: sq_lt_sq₀, sq_abs, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h1 : -b < a
h2 : a < b
⊢ HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2

Tactic:
sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))

Premises used: Iff.mpr, le_abs_self, sq_lt_sq, And.intro, abs_lt, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2 ↔ |a| ≤ |b|

Tactic:
simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

Premises used: sq_le_sq₀, sq_abs, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h1 : -b ≤ a
h2 : a ≤ b
⊢ HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2

Tactic:
sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))

Premises used: Iff.mpr, le_abs_self, abs_le, sq_le_sq, And.intro, le_trans
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2
hb : 0 ≤ b
rwa : |a| < |b|
rwa₁ rwa₂ rwa₃ rwa₄ : HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2
⊢ |a| < b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_lt_sq]

Premises used: sq_lt_sq, abs_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : HPow.hPow (β := ℕ) a 2 < HPow.hPow (β := ℕ) b 2
hb : 0 ≤ b
⊢ -b < a ∧ a < b

Tactic:
abs_lt.1 <| abs_lt_of_sq_lt_sq h hb

Premises used: abs_lt_of_sq_lt_sq, Iff.mp, abs_lt
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2
hb : 0 ≤ b
rwa : |a| ≤ |b|
rwa₁ rwa₂ rwa₃ rwa₄ : HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2
⊢ |a| ≤ b

Tactic:
rwa [← abs_of_nonneg hb, ← sq_le_sq]

Premises used: sq_le_sq, abs_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2
hb : 0 ≤ b
⊢ a ≤ b

Tactic:
le_abs_self a |>.trans <| abs_le_of_sq_le_sq h hb

Premises used: abs_le_of_sq_le_sq, le_abs_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : HPow.hPow (β := ℕ) a 2 ≤ HPow.hPow (β := ℕ) b 2
hb : 0 ≤ b
⊢ -b ≤ a ∧ a ≤ b

Tactic:
abs_le.1 <| abs_le_of_sq_le_sq h hb

Premises used: abs_le_of_sq_le_sq, abs_le, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ |a| = |b|

Tactic:
simp only [le_antisymm_iff, sq_le_sq]

Premises used: sq_le_sq, le_antisymm_iff
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ HPow.hPow (β := ℕ) a 2 ≤ 1 ↔ |a| ≤ 1

Tactic:
simpa only [one_pow, abs_one] using sq_le_sq (a := a) (b := 1)

Premises used: one_pow, sq_le_sq, abs_one
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ HPow.hPow (β := ℕ) a 2 < 1 ↔ |a| < 1

Tactic:
simpa only [one_pow, abs_one] using sq_lt_sq (a := a) (b := 1)

Premises used: one_pow, sq_lt_sq, abs_one
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 1 ≤ HPow.hPow (β := ℕ) a 2 ↔ 1 ≤ |a|

Tactic:
simpa only [one_pow, abs_one] using sq_le_sq (a := 1) (b := a)

Premises used: one_pow, sq_le_sq, abs_one
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 1 < HPow.hPow (β := ℕ) a 2 ↔ 1 < |a|

Tactic:
simpa only [one_pow, abs_one] using sq_lt_sq (a := 1) (b := a)

Premises used: one_pow, sq_lt_sq, abs_one
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
rw : (a - b) * (a - b) = a * a + b * b - HAdd.hAdd (α := α) 1 1 * a * b
⊢ |a - b| * |a - b| = a * a + b * b - HAdd.hAdd (α := α) 1 1 * a * b

Tactic:
rw [abs_mul_abs_self]

Premises used: abs_mul_abs_self
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
⊢ (a - b) * (a - b) = a * a + b * b - HAdd.hAdd (α := α) 1 1 * a * b

Tactic:
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
    neg_add_rev, neg_neg, add_assoc]

Premises used: neg_add_rev, add_left_comm, add_assoc, sub_eq_add_neg, neg_neg, add_comm, mul_comm, mul_add, mul_one, mul_neg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : ℤˣ
inl : a = 1 → Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
inr : a = -1 → Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
⊢ Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1

Tactic:
cases Int.units_eq_one_or a

Premises used: Int.units_eq_one_or
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : ℤˣ
h : a = 1
⊢ Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : ℤˣ
h : a = -1
⊢ Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n : ℕ
inst_2 : IsOrderedRing α
⊢ |geomSum a b 0| ≤ HAdd.hAdd (α := α) (↑0 : α) 1 * HPow.hPow (β := ℕ) (max |a| |b|) 0

Tactic:
simp [geomSum]

Premises used: _private.0.geomSum
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n : ℕ
inst_2 : IsOrderedRing α
succ :
  ∀ (n : ℕ) (ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n),
    |geomSum a b (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)
⊢ |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_

Premises used: _private.0.geomSum
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ |geomSum a b (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)

Tactic:
(abs_add_le ..).trans ?_

Premises used: _private.0.geomSum, LE.le.trans, abs_add_le
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ : |a * geomSum a b n| + |b ^ (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)
⊢ |geomSum a b (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)

Tactic:
refine (abs_add_le ..).trans ?_

Premises used: LE.le.trans, abs_add_le
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ :
  |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)

Tactic:
rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]

Premises used: Nat.cast_succ, abs_mul, add_one_mul, abs_pow
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)

Tactic:
add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)

Premises used: add_le_add, pow_le_pow_left₀, le_sup_right
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ : |a| * |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1)
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)

Tactic:
refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)

Premises used: add_le_add, pow_le_pow_left₀, le_sup_right
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ : |geomSum a b n| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|
⊢ |a| * |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, mul_comm |a|]

Premises used: abs, pow_succ, mul_assoc, mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ : 0 ≤ |a|
succ₁ : 0 ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
succ₂ : |a| ≤ max |a| |b|
⊢ |geomSum a b n| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ 0 ≤ |a|

Tactic:
abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ 0 ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n

Tactic:
(abs_nonneg _).trans ih

Premises used: LE.le.trans, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ |a| ≤ max |a| |b|

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n_1 : ℕ
inst_2 : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ 0 ≤ |a|

Tactic:
exacts [abs_nonneg _, (abs_nonneg _).trans ih, le_sup_left]

Premises used: le_sup_left, LE.le.trans, abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
a b : α
n : ℕ
⊢ a ^ HAdd.hAdd (α := ℕ) 0 1 - b ^ HAdd.hAdd (α := ℕ) 0 1 = (a - b) * geomSum a b 0

Tactic:
simp [geomSum]

Premises used: _private.0.geomSum
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
a b : α
n_1 n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
?_
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
a b : α
n : ℕ
succ :
  ∀ (n : ℕ) (ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n),
    a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
⊢ a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_

Premises used: _private.0.geomSum
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
a b : α
n_1 n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
succ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n + b ^ (n + 1))
succ₁ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n) + (a - b) * b ^ (n + 1)
succ₂ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (geomSum a b n * a) + (a - b) * b ^ (n + 1)
succ₃ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b n * a + (a - b) * b ^ (n + 1)
succ₄ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a ^ (n + 1) - b ^ (n + 1)) * a + (a - b) * b ^ (n + 1)
succ₅ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1) * a - b ^ (n + 1) * a + (a - b) * b ^ (n + 1)
succ₆ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1) * a - b ^ (n + 1) * a + (a * b ^ (n + 1) - b * b ^ (n + 1))
succ₇ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1) * a + (a * b ^ (n + 1) - b * b ^ (n + 1))
succ₈ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1) * a + (a * b ^ (n + 1) - b ^ (n + 1 + 1))
succ₉ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - a * b ^ (n + 1) + (a * b ^ (n + 1) - b ^ (n + 1 + 1))
succ₁₀ succ₁₁ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1 + 1)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
    sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

Premises used: sub_add_sub_cancel, pow_succ, mul_assoc, _private.0.geomSum, sub_mul, mul_comm, mul_add, pow_succ'
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n : ℕ
inst_2 : IsOrderedRing α
zero : |HPow.hPow (β := ℕ) a 0 - HPow.hPow (β := ℕ) b 0| ≤ |a - b| * (↑0 : α) * max |a| |b| ^ HSub.hSub (α := ℕ) 0 1
succ : ∀ (n : ℕ), |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * (↑(n + 1) : α) * max |a| |b| ^ (n + 1 - 1)
⊢ |a ^ n - b ^ n| ≤ |a - b| * (↑n : α) * max |a| |b| ^ (n - 1)

Tactic:
obtain _ | n := n
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
⊢ |HPow.hPow (β := ℕ) a 0 - HPow.hPow (β := ℕ) b 0| ≤ |a - b| * (↑0 : α) * max |a| |b| ^ HSub.hSub (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
succ : |a - b| * |geomSum a b n| ≤ |a - b| * (HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n)
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * (↑(n + 1) : α) * max |a| |b| ^ (n + 1 - 1)

Tactic:
rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]

Premises used: Nat.cast_succ, mul_assoc, abs_mul, Nat.add_sub_cancel, _private.0.pow_sub_pow_eq_sub_mul_geomSum
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
succ : 0 ≤ |a - b|
succ₁ : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * (HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ 0 ≤ |a - b|

Tactic:
abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ 0 ≤ |a - b|

Tactic:
exact abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n

Tactic:
abs_geomSum_le ..

Premises used: _private.0.abs_geomSum_le
-- Module: Mathlib.Algebra.Order.Ring.Abs
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n

Tactic:
exact abs_geomSum_le ..

Premises used: _private.0.abs_geomSum_le