awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
      zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
      neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }
have mk : toNeg = toNeg_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk : toNeg = toNeg_1
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
      zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
      neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }
have mk₁ : toSub = toSub_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk : toNeg = toNeg_1
mk₁ : toSub = toSub_1
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
      zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
      neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }
have mk₂ : zsmul = zsmul_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
toSemiring : Semiring R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
toIntCast : IntCast R
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
toSemiring_1 : Semiring R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
toIntCast_1 : IntCast R
intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := Semiring R) Ring.toSemiring Ring.toSemiring
h₂ : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h₃ : Eq.{u + 1} (α := SubNegMonoid R) AddGroup.toSubNegMonoid AddGroup.toSubNegMonoid
mk : toNeg = toNeg_1
mk₁ : toSub = toSub_1
mk₂ : zsmul = zsmul_1
⊢ { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul,
      zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg',
      neg_add_cancel := neg_add_cancel, toIntCast := toIntCast, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : Ring R } =
    { toSemiring := toSemiring_1, toNeg := toNeg_1, toSub := toSub_1, sub_eq_add_neg := sub_eq_add_neg_1,
      zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1, zsmul_neg' := zsmul_neg'_1,
      neg_add_cancel := neg_add_cancel_1, toIntCast := toIntCast_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }
have mk₃ : toIntCast = toIntCast_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
⊢ a₁ = a₂
have h_add : ∀ (x y : R), x + y = x + y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonUnitalRing R) toNonUnitalRing toNonUnitalRing
h_add : ∀ (x y : R), x + y = x + y
⊢ a₁ = a₂
have h_mul : ∀ (x y : R), x * y = x * y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
⊢ a₁ = a₂
have h_add : ∀ (x y : R), x + y = x + y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := NonAssocRing R) toNonAssocRing toNonAssocRing
h_add : ∀ (x y : R), x + y = x + y
⊢ a₁ = a₂
have h_mul : ∀ (x y : R), x * y = x * y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
⊢ a₁ = a₂
have h_add : ∀ (x y : R), x + y = x + y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
Goal:
R : Type u
a₁ a₂ : Ring R
h : Eq.{u + 1} (α := Semiring R) toSemiring toSemiring
h_add : ∀ (x y : R), x + y = x + y
⊢ a₁ = a₂
have h_mul : ∀ (x y : R), x * y = x * y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 2), HPow.hPow (α := R) 0 i) (if n + 2 = 0 then 0 else 1)
have rw : HPow.hPow (α := R) 0 (n + 1) + ∑ i ∈ range (n + 1), HPow.hPow (α := R) 0 i = if n + 2 = 0 then 0 else 1
Tactic: rw [geom_sum_succ']
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i) (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))
have rw : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j))
  (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))
Tactic: rw [← sum_range_reflect]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j))
    (∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i))
have refine : ∀ (j : ℕ) (j_in : j ∈ range n), op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
Tactic: refine sum_congr rfl fun j j_in => ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
n i : ℕ
h : i ∈ range n
⊢ x ^ i * HPow.hPow (α := R) 1 (n - 1 - i) = x ^ i
have rw : x ^ i * 1 = x ^ i
Tactic: rw [one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
n i : ℕ
h : i ∈ range n
rw : x ^ i * 1 = x ^ i
⊢ x ^ i * HPow.hPow (α := R) 1 (n - 1 - i) = x ^ i
have rw₁ : x ^ i = x ^ i
Tactic: rw [one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero₂ : 0 + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₂ : 0 + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero₃ : HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₂ : 0 + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₃ : HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero₄ : 1 = HPow.hPow (β := ℕ) (x + y) 0
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
zero : (∑ i ∈ ∅, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₁ : 0 * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₂ : 0 + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₃ : HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
zero₄ : 1 = HPow.hPow (β := ℕ) (x + y) 0
⊢ (∑ i ∈ range 0, f 0 i) * x + HPow.hPow (β := ℕ) y 0 = HPow.hPow (β := ℕ) (x + y) 0
have zero₅ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
have rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
Tactic: rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
have rw₁ : (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n
Tactic: rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
rw₁ : (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
have rw₂ : (x + y) ^ n * HPow.hPow (β := ℕ) y 0 = (x + y) ^ n
Tactic: rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
rw₁ : (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n
rw₂ : (x + y) ^ n * HPow.hPow (β := ℕ) y 0 = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
have rw₃ : (x + y) ^ n * 1 = (x + y) ^ n
Tactic: rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
rw : (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n
rw₁ : (x + y) ^ n * y ^ (1 + n - (1 + n)) = (x + y) ^ n
rw₂ : (x + y) ^ n * HPow.hPow (β := ℕ) y 0 = (x + y) ^ n
rw₃ : (x + y) ^ n * 1 = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n
have rw₄ : (x + y) ^ n = (x + y) ^ n
Tactic: rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
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
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)
have f_last : f (n + 1) n = (x + y) ^ n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
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
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))
have this : Commute y ((x + y) ^ i)
Tactic: have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * ((x + y) ^ i * y ^ (n - 1 - i))
have rw : (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
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 : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have this₁ : i + 1 + (n - (i + 1)) = n
Tactic: have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
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
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have this₁ : n - (i + 1) + (i + 1) = n
Tactic: rw [add_comm (i + 1)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have rw : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - i) = (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - (i + 1) + 1)
Tactic: rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have rw₁ : (x + y) ^ i * y ^ (n - (i + 1) + (i + 1) - 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
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)
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)
have rw₂ : (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
Tactic: rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]