awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Ring α
a : α
⊢ Odd |a| ↔ Odd a
have inl : ∀ (h : |a| = a), Odd |a| ↔ Odd a
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Ring α
a : α
inl : ∀ (h : |a| = a), Odd |a| ↔ Odd a
⊢ Odd |a| ↔ Odd a
have inr : ∀ (h : |a| = -a), Odd |a| ↔ Odd a
Tactic: rcases abs_choice a with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
⊢ |a * b| = |a| * |b|
have rw : a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inl : ∀ (ha : a ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total a 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
inl : ∀ (ha : a ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inr : ∀ (ha : 0 ≤ a), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total a 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inl : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
inl : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inl₁ : ∀ (hb : 0 ≤ b), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : 0 ≤ a
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inr : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a b : α
ha : 0 ≤ a
inr : ∀ (hb : b ≤ 0), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
have inr₁ : ∀ (hb : 0 ≤ b), a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Tactic: rcases le_total b 0 with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ |a| ^ n = a ^ n
have rw : 0 ≤ a ^ n
Tactic: rw [← abs_pow, abs_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
⊢ |HPow.hPow (α := α) (-1) n| = 1
have rw : HPow.hPow (α := α) |(-1)| n = 1
Tactic: rw [← pow_abs, abs_neg, abs_one, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
n : ℕ
rw : HPow.hPow (α := α) |(-1)| n = 1
⊢ |HPow.hPow (α := α) (-1) n| = 1
have rw₁ : HPow.hPow (α := α) |1| n = 1
Tactic: rw [← pow_abs, abs_neg, abs_one, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
⊢ |HPow.hPow (α := α) (-1) n| = 1
have rw₂ : HPow.hPow (α := α) 1 n = 1
Tactic: rw [← pow_abs, abs_neg, abs_one, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
⊢ |HPow.hPow (α := α) (-1) n| = 1
have rw₃ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [← pow_abs, abs_neg, abs_one, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = 1 ↔ |a| = 1
have h₁ : |a ^ n| = |a| ^ n
Tactic: convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
h₁ : |a ^ n| = |a| ^ n
⊢ |a ^ n| = 1 ↔ |a| = 1
have h₂ : 1 = HPow.hPow (α := α) 1 n
Tactic: convert! pow_left_inj₀ (abs_nonneg a) zero_le_one h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b
have rw : |a| = |b| ↔ |a| * |a| = |b| * |b|
Tactic: rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ a * a < b * b
have rw : |a| < |b| ↔ |a| * |a| < |b| * |b|
Tactic: rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b
have rw : |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
Tactic: rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
have rwa : |a| < |b|
Tactic: rwa [← abs_of_nonneg hb, ← sq_lt_sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
have rwa : |a| ≤ |b|
Tactic: rwa [← abs_of_nonneg hb, ← sq_le_sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
have rw : (a - b) * (a - b) = a * a + b * b - HAdd.hAdd (α := α) 1 1 * a * b
Tactic: rw [abs_mul_abs_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : ℤˣ
⊢ Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
have inl : a = 1 → Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
Tactic: cases Int.units_eq_one_or a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsOrderedRing α
a : ℤˣ
inl : a = 1 → Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
⊢ Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
have inr : a = -1 → Eq.{u_1 + 1} (α := α) |(↑(↑a : ℤ) : α)| 1
Tactic: cases Int.units_eq_one_or a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n : ℕ
inst_2 : IsOrderedRing α
⊢ |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
have 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)
Tactic: induction n with | zero => simp [geomSum] | succ n ih => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
have succ : |a * geomSum a b n| + |b ^ (n + 1)| ≤ HAdd.hAdd (α := α) (↑(n + 1) : α) 1 * max |a| |b| ^ (n + 1)
Tactic: refine (abs_add_le ..).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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) : α) 1 * max |a| |b| ^ (n + 1)
have succ : |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)
Tactic: rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
have succ : |a| * |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1)
Tactic: refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ (n + 1)
have succ : |geomSum a b n| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|
Tactic: rw [pow_succ, ← mul_assoc, mul_comm |a|]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|
have succ : 0 ≤ |a|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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|
⊢ |geomSum a b n| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|
have succ₁ : 0 ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
⊢ |geomSum a b n| * |a| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n * max |a| |b|
have succ₂ : |a| ≤ max |a| |b|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
a b : α
n : ℕ
⊢ a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
have 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)
Tactic: induction n with | zero => simp [geomSum] | succ n ih => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
have succ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n + 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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))
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₁ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (a * geomSum a b n) + (a - b) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₂ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * (geomSum a b n * a) + (a - b) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₃ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b n * a + (a - b) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₄ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a ^ (n + 1) - b ^ (n + 1)) * a + (a - b) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₅ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1) * a - b ^ (n + 1) * a + (a - b) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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)
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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))
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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))
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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))
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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))
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)
have succ₁₀ : a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = a ^ (n + 1 + 1) - b ^ (n + 1 + 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
n : ℕ
inst_2 : IsOrderedRing α
⊢ |a ^ n - b ^ n| ≤ |a - b| * (↑n : α) * max |a| |b| ^ (n - 1)
have zero : |HPow.hPow (β := ℕ) a 0 - HPow.hPow (β := ℕ) b 0| ≤ |a - b| * (↑0 : α) * max |a| |b| ^ HSub.hSub (α := ℕ) 0 1
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
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
⊢ |a ^ n - b ^ n| ≤ |a - b| * (↑n : α) * max |a| |b| ^ (n - 1)
have succ : ∀ (n : ℕ), |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * (↑(n + 1) : α) * max |a| |b| ^ (n + 1 - 1)
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * (↑(n + 1) : α) * max |a| |b| ^ (n + 1 - 1)
have succ : |a - b| * |geomSum a b n| ≤ |a - b| * (HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n)
Tactic: rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * (HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n)
have succ : 0 ≤ |a - b|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Abs (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
a b : α
inst_2 : IsOrderedRing α
n : ℕ
succ : 0 ≤ |a - b|
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * (HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n)
have succ₁ : |geomSum a b n| ≤ HAdd.hAdd (α := α) (↑n : α) 1 * max |a| |b| ^ n
Tactic: gcongr