awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
zero : x.snd <• HPow.hPow (β := ℕ) x.fst 0 = HPow.hPow (β := ℕ) x.fst 0 •> x.snd
⊢ x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
have succ : ∀ (n : ℕ) (ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd), x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd
Tactic: induction n with
    | zero => simp
    | succ n ih =>
      rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd
have simp_rw : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.pred - i + i) •> x.snd) (List.range n)) = n •> x.fst ^ n.pred •> x.snd
Tactic: simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
  0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
    0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw₁ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) = 0 •> 1 •> x.snd
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
    0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
rw₁ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) = 0 •> 1 •> x.snd
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw₂ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) []) = 0 •> 1 •> x.snd
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
    0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
rw₁ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) = 0 •> 1 •> x.snd
rw₂ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) []) = 0 •> 1 •> x.snd
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw₃ : Eq.{v + 1} (α := M) (List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) [])) 0
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
    0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
rw₁ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) = 0 •> 1 •> x.snd
rw₂ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) []) = 0 •> 1 •> x.snd
rw₃ : Eq.{v + 1} (α := M) (List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) [])) 0
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw₄ : Eq.{v + 1} (α := M) (List.sum []) 0
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) =
    0 •> HPow.hPow (β := ℕ) x.fst 0 •> x.snd
rw₁ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) (List.range 0)) = 0 •> 1 •> x.snd
rw₂ : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) []) = 0 •> 1 •> x.snd
rw₃ : Eq.{v + 1} (α := M) (List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i + i) •> x.snd) [])) 0
rw₄ : Eq.{v + 1} (α := M) (List.sum []) 0
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i + i) •> x.snd) (List.range 0)) =
    0 •> x.fst ^ Nat.pred 0 •> x.snd
have rw₅ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.succ.pred - i + i) •> x.snd) (List.range n.succ)) =
    n.succ •> x.fst ^ n.succ.pred •> x.snd
have simp_rw : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)) = n.succ •> x.fst ^ n •> x.snd
Tactic: simp_rw [Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ List.length.{v} (α := M) (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)) •>
      x.fst ^ n •> x.snd =
    n.succ •> x.fst ^ n •> x.snd
have rw : (List.range n.succ).length •> x.fst ^ n •> x.snd = n.succ •> x.fst ^ n •> x.snd
Tactic: rw [List.length_map, List.length_range]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n_1 : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
rw : (List.range n.succ).length •> x.fst ^ n •> x.snd = n.succ •> x.fst ^ n •> x.snd
⊢ List.length.{v} (α := M) (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)) •>
      x.fst ^ n •> x.snd =
    n.succ •> x.fst ^ n •> x.snd
have rw₁ : n.succ •> x.fst ^ n •> x.snd = n.succ •> x.fst ^ n •> x.snd
Tactic: rw [List.length_map, List.length_range]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)
have rw : n •> x.fst ^ n.pred •> x.snd = n •> (x.snd <• x.fst ^ n.pred)
Tactic: rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
rw : n •> x.fst ^ n.pred •> x.snd = n •> (x.snd <• x.fst ^ n.pred)
⊢ (x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)
have rw₁ : n •> x.fst ^ n.pred •> x.snd = n •> x.fst ^ n.pred •> x.snd
Tactic: rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x y z : tsze R M
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
have simp_rw : (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
  x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
Tactic: simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x y z : tsze R M
simp_rw :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
    x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
have simp_rw₁ : (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
  (x.1 * y.1) •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
Tactic: simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x y z : tsze R M
simp_rw :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
    x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
simp_rw₁ :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
have simp_rw₂ : (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
  (x.1 * y.1) •> z.2 + (x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1))
Tactic: simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x y z : tsze R M
simp_rw :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
    x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
simp_rw₁ :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
simp_rw₂ :
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + (x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1))
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
have simp_rw₃ : (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
  (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• (y.1 * z.1))
Tactic: simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : tsze R M
⊢ (x ^ (n + 1)).snd = (x ^ n * x).snd
have simp_rw : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) =
  (x ^ n).fst •> x.snd +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)) <• x.fst
Tactic: simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : tsze R M
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) =
    (x ^ n).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)) <• x.fst
have zero : List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i) •> x.snd <• x.fst ^ i) (List.range (HAdd.hAdd (α := ℕ) 0 1))) =
  (HPow.hPow (β := ℕ) x 0).fst •> x.snd +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i) •> x.snd <• x.fst ^ i) (List.range 0)) <• x.fst
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : tsze R M
zero :
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (0 - i) •> x.snd <• x.fst ^ i) (List.range (HAdd.hAdd (α := ℕ) 0 1))) =
    (HPow.hPow (β := ℕ) x 0).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (Nat.pred 0 - i) •> x.snd <• x.fst ^ i) (List.range 0)) <• x.fst
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) =
    (x ^ n).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)) <• x.fst
have succ : ∀ (n : ℕ),
  List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n + 1 - i) •> x.snd <• x.fst ^ i) (List.range (n + 1 + 1))) =
    (x ^ (n + 1)).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ ((n + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) <• x.fst
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
⊢ List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n + 1 - i) •> x.snd <• x.fst ^ i) (List.range (n + 1 + 1))) =
    (x ^ (n + 1)).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ ((n + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) <• x.fst
have succ : x.fst ^ (n + 1 - 0) •> x.snd <• HPow.hPow (β := ℕ) x.fst 0 +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n + 1 - i.succ) •> x.snd <• x.fst ^ i.succ) (List.range (n + 1))) =
  (x ^ (n + 1)).fst •> x.snd +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ ((n + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) <• x.fst
Tactic: rw [List.sum_range_succ']
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
⊢ x.fst ^ (n + 1 - 0) •> x.snd <• HPow.hPow (β := ℕ) x.fst 0 +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n + 1 - i.succ) •> x.snd <• x.fst ^ i.succ) (List.range (n + 1))) =
    (x ^ (n + 1)).fst •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ ((n + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))) <• x.fst
have succ : x.fst ^ (n + 1) •> x.snd +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i.succ) (List.range (n + 1))) =
  x.fst ^ (n + 1) •> x.snd +
    List.sum (List.map (fun (x_1 : ℕ) ↦ x.fst ^ (n - x_1) •> x.snd <• x.fst ^ x_1 <• x.fst) (List.range (n + 1)))
Tactic: simp only [pow_zero, op_one, Nat.sub_zero, one_smul, Nat.succ_sub_succ_eq_sub, fst_pow,
          Nat.pred_succ, List.smul_sum, List.map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
⊢ x.fst ^ (n + 1) •> x.snd +
      List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> x.snd <• x.fst ^ i.succ) (List.range (n + 1))) =
    x.fst ^ (n + 1) •> x.snd +
      List.sum (List.map (fun (x_1 : ℕ) ↦ x.fst ^ (n - x_1) •> x.snd <• x.fst ^ x_1 <• x.fst) (List.range (n + 1)))
have succ : (x.fst ^ n * x.fst) •> x.snd +
    List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i) •> (x.snd <• (x.fst ^ i * x.fst))) (List.range (n + 1))) =
  (x.fst ^ n * x.fst) •> x.snd +
    List.sum
      (List.map (fun (x_1 : ℕ) ↦ x.fst ^ (n - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n + 1)))
Tactic: simp_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx)
⊢ (x :: xs).prod.snd =
    List.sum
      (List.map
        (fun (x_1 : tsze R M × ℕ) ↦
          (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
            (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
        (x :: xs).zipIdx)
have cons : (x :: xs).prod.snd =
  List.sum
    (List.map
      (fun (x_1 : tsze R M × ℕ) ↦
        (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
          (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
      ((x, 0) :: List.map (Prod.map id fun (x : ℕ) ↦ x + 1) xs.zipIdx))
Tactic: rw [List.zipIdx_cons']
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx)
⊢ (x :: xs).prod.snd =
    List.sum
      (List.map
        (fun (x_1 : tsze R M × ℕ) ↦
          (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
            (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
        ((x, 0) :: List.map (Prod.map id fun (x : ℕ) ↦ x + 1) xs.zipIdx))
have cons : List.sum
      (List.map
        ((fun (x_1 : M) ↦ x.fst •> x_1) ∘ fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
        xs.zipIdx) +
    x.snd <• (List.map fst xs).prod =
  x.snd <• (List.map fst xs).prod +
    List.sum
      (List.map
        (fun (x_1 : tsze R M × ℕ) ↦
          x.fst •>
            (List.take x_1.2 (List.map fst xs)).prod •> (x_1.1.snd <• (List.drop (x_1.2 + 1) (List.map fst xs)).prod))
        xs.zipIdx)
Tactic: simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ l.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx)
have nil : Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (List.prod []))
  (List.sum
    (List.map
      (fun (x : tsze R M × ℕ) ↦
        List.prod (List.take x.2 (List.map (α := tsze R M) fst [])) •> x.1.snd <•
          List.prod (List.drop x.2.succ (List.map (α := tsze R M) fst [])))
      (List.zipIdx [])))
Tactic: induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.zipIdx_cons']
    simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
    exact add_comm _ _
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
nil :
  Eq.{v + 1} (α := M) (snd.{u, v} (R := R) (List.prod []))
    (List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          List.prod (List.take x.2 (List.map (α := tsze R M) fst [])) •> x.1.snd <•
            List.prod (List.drop x.2.succ (List.map (α := tsze R M) fst [])))
        (List.zipIdx [])))
⊢ l.prod.snd =
    List.sum
      (List.map
        (fun (x : tsze R M × ℕ) ↦
          (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx)
have cons : ∀ (x : tsze R M) (xs : List (tsze R M))
  (ih :
    xs.prod.snd =
      List.sum
        (List.map
          (fun (x : tsze R M × ℕ) ↦
            (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
          xs.zipIdx)),
  (x :: xs).prod.snd =
    List.sum
      (List.map
        (fun (x_1 : tsze R M × ℕ) ↦
          (List.take x_1.2 (List.map fst (x :: xs))).prod •> x_1.1.snd <•
            (List.drop x_1.2.succ (List.map fst (x :: xs))).prod)
        (x :: xs).zipIdx)
Tactic: induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.zipIdx_cons']
    simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
    exact add_comm _ _
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommMonoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x₁ x₂ : tsze R M
⊢ x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
have rw : x₁.1 •> x₂.2 + x₂.1 •> x₁.2 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1
Tactic: rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]