awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this_1 : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ n - (i + 1) + (i + 1) = n

Tactic:
rw [add_comm (i + 1)] at this

Premises used: add_comm, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this_1 : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
rw : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - (i + 1) + 1)
rw₁ : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
rw₂ : (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
rw₃ : (x + y) ^ i * y ^ (n - (1 + i) + 1 + i - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
rw₄ rw₅ : (x + y) ^ i * y ^ (n - (1 + i) + 1) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]

Premises used: add_assoc, add_comm, add_tsub_cancel_right, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ ∀ i ∈ range n, f (n + 1) i = y * f n i

Tactic:
have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
succ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n
succ₁ : (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₂ : (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₃ : f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₄ : (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
succ₅ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = x * (x + y) ^ n + y * (x + y) ^ n
succ₆ : (x + y) ^ n * x + ((∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₇ : (x + y) ^ n * x + ((∑ x ∈ range n, y * f n x) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₈ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y ^ (n + 1)) = (x + y) ^ n * x + y * (x + y) ^ n
succ₉ : (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₀ : (x + y) ^ n * x + (y * ((∑ i ∈ range n, f n i) * x) + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₁ : (x + y) ^ n * x + y * ((∑ i ∈ range n, f n i) * x + y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
succ₁₂ succ₁₃ : (x + y) ^ n * x + y * (x + y) ^ n = (x + y) ^ n * x + y * (x + y) ^ n
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]

Premises used: add_mul, Finset.mul_sum, Commute.pow_right, add_assoc, mul_assoc, Finset.sum_range_succ_comm, Commute.add_right, Commute.refl, HAdd.hAdd, mul_add, Commute.eq, Finset.sum_congr, pow_succ', rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun (m i : ℕ) ↦ (x + y) ^ i * y ^ (m - 1 - i)
zero : (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
succ :
  ∀ (n : ℕ) (ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n),
    (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n

Tactic:
induction n with
  | zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
  | succ n ih =>
    have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
    rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]

Premises used: add_mul, Finset.mul_sum, Commute.pow_right, add_assoc, MulZeroClass.zero_mul, mul_assoc, Finset.sum_range_succ_comm, zero_add, pow_zero, Commute.add_right, Commute.refl, HAdd.hAdd, mul_add, Finset.sum_empty, Commute.eq, pow_succ', Finset.range_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * x ^ (n - 1 - i)) (∑ i ∈ range n, x ^ (i + (n - 1 - i)))

Tactic:
simp_rw [← pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
rw : n • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
rw₁ rw₂ : (↑n : R) * x ^ (n - 1) = (↑n : R) * x ^ (n - 1)
⊢ #(range n) • x ^ (n - 1) = (↑n : R) * x ^ (n - 1)

Tactic:
rw [Finset.card_range, nsmul_eq_mul]

Premises used: Finset.card_range, nsmul_eq_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i * HPow.hPow (α := R) 1 (n - 1 - i)) * x + HPow.hPow (α := R) 1 n = (x + 1) ^ n

Tactic:
have := (Commute.one_right x).geom_sum₂_mul_add n
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * HPow.hPow (α := R) 1 (n - 1 - i)) * x + HPow.hPow (α := R) 1 n = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
rw [one_pow, geom_sum₂_with_one] at this

Premises used: one_pow, geom_sum₂_with_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
exact this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
h : Commute x y
zero :
  Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i * y ^ (HSub.hSub (α := ℕ) 0 1 - i))
    (∑ i ∈ range 0, y ^ i * x ^ (HSub.hSub (α := ℕ) 0 1 - i))
succ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1), x ^ i * y ^ (n + 1 - 1 - i))
      (∑ i ∈ range (n + 1), y ^ i * x ^ (n + 1 - 1 - i))
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, y ^ i * x ^ (n - 1 - i))

Tactic:
cases n
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i * y ^ (HSub.hSub (α := ℕ) 0 1 - i))
    (∑ i ∈ range 0, y ^ i * x ^ (HSub.hSub (α := ℕ) 0 1 - i))

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
succ :
  Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ range (n + 1), x ^ x_1 * y ^ (n - x_1))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1), x ^ i * y ^ (n + 1 - 1 - i))
    (∑ i ∈ range (n + 1), y ^ i * x ^ (n + 1 - 1 - i))

Tactic:
simp only [Nat.add_sub_cancel]

Premises used: Nat.add_sub_cancel
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
succ :
  Eq.{u_1 + 1} (α := R) (∑ r ∈ range (n + 1), x ^ (n - r) * y ^ (n - (n - r)))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
⊢ Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ range (n + 1), x ^ x_1 * y ^ (n - x_1))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))

Tactic:
rw [← Finset.sum_flip]

Premises used: Finset.sum_flip
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ r ∈ range (n + 1), x ^ (n - r) * y ^ (n - (n - r)))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
succ : ∀ (i : ℕ) (hi : i ∈ range (n + 1)), x ^ (n - i) * y ^ (n - (n - i)) = y ^ i * x ^ (n - i)
⊢ Eq.{u_1 + 1} (α := R) (∑ r ∈ range (n + 1), x ^ (n - r) * y ^ (n - (n - r)))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ range (n + 1)
⊢ x ^ (n - i) * y ^ (n - (n - i)) = y ^ i * x ^ (n - i)

Tactic:
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _

Premises used: Nat.sub_sub_self, Commute.pow_pow, Finset.mem_range, Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
x : R
n : ℕ
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (∑ i ∈ range n, x ^ i) : S)
    (∑ i ∈ range n, HPow.hPow (α := S) ((f : (a : R) → S) x : S) i : S)

Tactic:
simp [map_sum f]

Premises used: map_sum
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
x y : R
n : ℕ
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) : S)
    (∑ i ∈ range n,
        HPow.hPow (α := S) ((f : (a : R) → S) x : S) i * HPow.hPow (α := S) ((f : (a : R) → S) y : S) (n - 1 - i) :
      S)

Tactic:
simp [map_sum f]

Premises used: map_sum
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
(Commute.all x y).geom_sum₂_mul_add n

Premises used: Commute.geom_sum₂_mul_add, Commute.all
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, y ^ i * x ^ (n - 1 - i))

Tactic:
(Commute.all x y).geom_sum₂_comm n

Premises used: Commute.all, Commute.geom_sum₂_comm
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
h : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
apply eq_tsub_of_add_eq

Premises used: eq_tsub_of_add_eq
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n

Tactic:
simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

Premises used: HSub.hSub, tsub_add_cancel_of_le, geom_sum₂_mul_add
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
rw : (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Tactic:
rw [← Finset.sum_range_reflect]

Premises used: Finset.sum_range_reflect
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Tactic:
geom_sum₂_mul_of_ge hxy n

Premises used: geom_sum₂_mul_of_ge
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
h : ∀ x_1 ∈ range n, x ^ (n - 1 - x_1) * y ^ (n - 1 - (n - 1 - x_1)) = y ^ x_1 * x ^ (n - 1 - x_1)
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n

Tactic:
convert! geom_sum₂_mul_of_ge hxy n using 3

Premises used: geom_sum₂_mul_of_ge
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h : x_1 ∈ range n
⊢ x_1 < n

Tactic:
simp_all only [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h_1 : x_1 < n
h : y ^ (n - 1 - (n - 1 - x_1)) * x ^ (n - 1 - x_1) = y ^ x_1 * x ^ (n - 1 - x_1)
⊢ x ^ (n - 1 - x_1) * y ^ (n - 1 - (n - 1 - x_1)) = y ^ x_1 * x ^ (n - 1 - x_1)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h_1 : x_1 < n
h : n - 1 - (n - 1 - x_1) = x_1
⊢ y ^ (n - 1 - (n - 1 - x_1)) * x ^ (n - 1 - x_1) = y ^ x_1 * x ^ (n - 1 - x_1)

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h : x_1 < n
⊢ n - 1 - (n - 1 - x_1) = x_1

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x : R
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
simpa using geom_sum₂_mul_of_ge hx n

Premises used: geom_sum₂_mul_of_ge
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x : R
hx : x ≤ 1
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
simpa using geom_sum₂_mul_of_le hx n

Premises used: geom_sum₂_mul_of_le
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, HPow.hPow (α := R) (-1) i) (if Even (α := ℕ) 0 then 0 else 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
succ : (HPow.hPow (α := R) (-1) k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (k + 1), HPow.hPow (α := R) (-1) i) (if Even (k + 1) then 0 else 1)

Tactic:
simp only [geom_sum_succ', Nat.even_add_one, hk]

Premises used: Nat.even_add_one, geom_sum_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
pos : ∀ (h : Even k), HPow.hPow (α := R) (-1) k + 0 = 1
neg : ∀ (h : ¬Even k), HPow.hPow (α := R) (-1) k + 1 = 0
⊢ (HPow.hPow (α := R) (-1) k + if Even k then 0 else 1) = if ¬Even k then 0 else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : Even k
pos : HAdd.hAdd (α := R) 1 0 = 1
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HPow.hPow (α := R) (-1) k + 0 = 1

Tactic:
rw [h.neg_one_pow, add_zero]

Premises used: Even.neg_one_pow, add_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : ¬Even k
neg : HAdd.hAdd (α := R) (-1) 1 = 0
neg₁ neg₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (-1) k + 1 = 0

Tactic:
rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

Premises used: Nat.not_even_iff_odd, neg_add_cancel, Iff.mp, Odd.neg_one_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, HPow.hPow (α := R) (-1) i) (if Even (α := ℕ) 0 then 0 else 1)
succ :
  ∀ (k : ℕ) (hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ range (k + 1), HPow.hPow (α := R) (-1) i) (if Even (k + 1) then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, HPow.hPow (α := R) (-1) i) (if Even n then 0 else 1)

Tactic:
induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

Premises used: Nat.even_add_one, geom_sum_succ', neg_add_cancel, add_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n

Tactic:
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n

Tactic:
rw [sub_add_cancel] at this

Premises used: sub_add_cancel
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
rw :
  (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) =
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n - y ^ n
rw₁ rw₂ : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y)
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
rw [← this, add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
a : MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
⊢ (y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n

Tactic:
apply op_injective

Premises used: MulOpposite.op_injective
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
a :
  MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n
⊢ MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)

Tactic:
simp only [op_mul, op_sub, op_pow]

Premises used: MulOpposite.op_pow, MulOpposite.op_mul, MulOpposite.op_sub
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n

Tactic:
simp [(Commute.op h.symm).geom_sum₂_mul n]

Premises used: Commute.geom_sum₂_mul, Commute.symm, Commute.op
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
rw : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)
rw₁ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
rw₂ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
rw₃ rw₄ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n

Tactic:
rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]

Premises used: neg_sub, HPow.hPow, Commute.mul_neg_geom_sum₂, neg_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
Dvd.intro _ <| h.mul_geom_sum₂ _

Premises used: Dvd.intro, Commute.mul_geom_sum₂
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
rw : HPow.hPow (α := R) 1 n - x ^ n
| 1 - x ^ n

Tactic:
rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
conv_rhs : 1 - x ∣ HPow.hPow (α := R) 1 n - x ^ n
⊢ 1 - x ∣ 1 - x ^ n

Tactic:
conv_rhs => rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ HPow.hPow (α := R) 1 n - x ^ n

Tactic:
(Commute.one_left x).sub_dvd_pow_sub_pow n

Premises used: Commute.sub_dvd_pow_sub_pow, Commute.one_left
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ HPow.hPow (α := R) 1 n - x ^ n

Tactic:
exact (Commute.one_left x).sub_dvd_pow_sub_pow n

Premises used: Commute.sub_dvd_pow_sub_pow, Commute.one_left
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
rw : x ^ n - HPow.hPow (α := R) 1 n
| x ^ n - 1

Tactic:
rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
conv_rhs : x - 1 ∣ x ^ n - HPow.hPow (α := R) 1 n
⊢ x - 1 ∣ x ^ n - 1

Tactic:
conv_rhs => rw [← one_pow n]

Premises used: one_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - HPow.hPow (α := R) 1 n

Tactic:
(Commute.one_right x).sub_dvd_pow_sub_pow n

Premises used: Commute.sub_dvd_pow_sub_pow, Commute.one_right
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - HPow.hPow (α := R) 1 n

Tactic:
exact (Commute.one_right x).sub_dvd_pow_sub_pow n

Premises used: Commute.sub_dvd_pow_sub_pow, Commute.one_right