awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
simp_rw :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
simp_rw₁ :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (op x₂.1 + op x₃.1) •> x₁.2 =
    x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
simp_rw₂ :
  x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (x₁.2 <• x₂.1 + x₁.2 <• x₃.1) =
    x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
⊢ x₁.1 •> (x₂.2 + x₃.2) + x₁.2 <• (x₂.1 + x₃.1) = x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)

Tactic:
simp_rw [smul_add, MulOpposite.op_add, add_smul, add_add_add_comm]

Premises used: add_smul, MulOpposite.op_add, add_add_add_comm, smul_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x₁ x₂ x₃ : tsze R M
simp_rw :
  x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
simp_rw₁ :
  x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 <• x₃.1 + x₂.2 <• x₃.1) =
    x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
⊢ (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)

Tactic:
simp_rw [add_smul, smul_add, add_add_add_comm]

Premises used: add_smul, add_add_add_comm, smul_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 <• x.1 = 0
rw₁ : 0 <• x.1 = 0
rw₂ rw₃ : Eq.{v + 1} (α := M) 0 0
⊢ 0 •> x.2 + 0 <• x.1 = 0

Tactic:
rw [zero_smul, zero_add, smul_zero]

Premises used: smul_zero, zero_add, zero_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u, v} Rᵐᵒᵖ M
x : tsze R M
rw : 0 + 0 •> x.2 = 0
rw₁ : 0 •> x.2 = 0
rw₂ rw₃ : Eq.{v + 1} (α := M) 0 0
⊢ x.1 •> 0 + 0 •> x.2 = 0

Tactic:
rw [smul_zero, zero_add, zero_smul]

Premises used: smul_zero, zero_add, zero_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
x : tsze R M
n : ℕ
⊢ (x ^ n).fst = x.fst ^ n

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
x : tsze R M
n : ℕ
⊢ (x ^ n).snd = List.sum (List.map (fun (i : ℕ) ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n))

Tactic:
rfl

Premises used: List.sum, rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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.snd <• HPow.hPow (β := ℕ) x.fst 0 = HPow.hPow (β := ℕ) x.fst 0 •> x.snd

Tactic:
simp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
succ : x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
succ₁ : (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
succ₂ : x.snd <• x.fst ^ n <• x.fst = (x.fst ^ n * x.fst) •> x.snd
succ₃ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.fst •> x.snd
succ₄ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> (x.snd <• x.fst)
succ₅ : x.snd <• x.fst ^ n <• x.fst = x.fst ^ n •> x.snd <• x.fst
succ₆ succ₇ : x.fst ^ n •> x.snd <• x.fst = x.fst ^ n •> x.snd <• x.fst
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd

Tactic:
rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]

Premises used: TrivSqZeroExt.snd, pow_succ, TrivSqZeroExt.fst, MulOpposite.op_mul, SMulCommClass.smul_comm, SemigroupAction.mul_smul, MulOpposite.op
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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
⊢ x.snd <• x.fst ^ n = x.fst ^ n •> 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]

Premises used: TrivSqZeroExt.snd, pow_succ, TrivSqZeroExt.fst, MulOpposite.op_mul, SMulCommClass.smul_comm, SemigroupAction.mul_smul, MulOpposite.op, TrivSqZeroExt.zero
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
simp_rw [snd_pow_eq_sum, ← smul_comm (_ : R) (_ : Rᵐᵒᵖ), aux, smul_smul, ← pow_add]

Premises used: TrivSqZeroExt.snd_pow_eq_sum, pow_add, smul_smul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₅ rw₆ : Eq.{v + 1} (α := M) 0 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

Tactic:
rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]

Premises used: List.sum_nil, Nat.pred_zero, pow_zero, zero_smul, List.range_zero, List.map_nil
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
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
⊢ 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

Tactic:
simp_rw [Nat.pred_succ]

Premises used: Nat.pred_succ
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
⊢ ∀ (x_1 : M),
    Membership.mem (γ := List M) (List.map (fun (i : ℕ) ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)) x_1 →
      x_1 = x.fst ^ n •> x.snd

Tactic:
grind
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
rw₁ rw₂ : n.succ •> 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

Tactic:
rw [List.length_map, List.length_range]

Premises used: List.length_range, List.length_map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 - i + i) •> x.snd) (List.range n.succ)) = n.succ •> x.fst ^ n •> x.snd

Tactic:
exact (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) (by grind)).trans
      (by rw [List.length_map, List.length_range])

Premises used: TrivSqZeroExt.snd, List.sum_eq_card_nsmul, TrivSqZeroExt.fst, HPow.hPow, HSMul.hSMul, Eq.trans
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 ^ (n.pred - i + i) •> x.snd) (List.range n)) = n •> x.fst ^ n.pred •> x.snd

Tactic:
match n with
  | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
  | (Nat.succ n) =>
    simp_rw [Nat.pred_succ]
    exact (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) (by grind)).trans
      (by rw [List.length_map, List.length_range])
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
rw₁ rw₂ : n •> x.fst ^ n.pred •> x.snd = n •> x.fst ^ n.pred •> x.snd
⊢ (x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)

Tactic:
rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]

Premises used: TrivSqZeroExt.snd_pow_of_smul_comm, _private.0.TrivSqZeroExt.snd_pow_of_smul_comm.aux
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R : Type u
M : Type v
inst : CommMonoid R
inst_1 : AddMonoid M
inst_2 : DistribMulAction R M
inst_3 : DistribMulAction.{u, v} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : tsze R M
n : ℕ
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
snd_pow_of_smul_comm _ _ (op_smul_eq_smul _ _)

Premises used: TrivSqZeroExt.snd_pow_of_smul_comm, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
r : R
n : ℕ
⊢ (HPow.hPow (α := tsze R M) (inl r) n).snd = snd (inl (r ^ n))

Tactic:
simp [snd_pow_eq_sum, List.map_const']

Premises used: TrivSqZeroExt.snd_pow_eq_sum, List.map_const'
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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))
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)

Tactic:
simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]

Premises used: add_assoc, MulOpposite.op_mul, SMulCommClass.smul_comm, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
⊢ (HPow.hPow (β := ℕ) x 0).snd = snd.{u, v} (R := R) 1

Tactic:
simp [snd_pow_eq_sum]

Premises used: TrivSqZeroExt.snd_pow_eq_sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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
⊢ (x ^ (n + 1)).snd = (x ^ n * x).snd

Tactic:
simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]

Premises used: TrivSqZeroExt.snd_pow_eq_sum, TrivSqZeroExt.snd_mul, Nat.pred_succ
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
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
⊢ 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:
cases n
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
⊢ 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:
simp [List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
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
⊢ 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:
rw [List.sum_range_succ']

Premises used: List.sum_range_succ'
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
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)))
⊢ 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:
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]

Premises used: List.map_map, pow_zero, one_smul, Function.comp_def, TrivSqZeroExt.fst_pow, Nat.pred_succ, MulOpposite.op_one, Nat.sub_zero, Nat.succ_sub_succ_eq_sub, List.smul_sum
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 : ℕ
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)))
⊢ 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_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, pow_succ]

Premises used: pow_succ, smul_smul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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 * 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:
rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
l : List (tsze R M)
⊢ l.prod.fst = (List.map fst l).prod

Tactic:
map_list_prod ({ toFun := fst, map_one' := fst_one, map_mul' := fst_mul } : tsze R M →* R) _

Premises used: OneHom.mk, TrivSqZeroExt.fst_one, MonoidHom.mk, map_list_prod, TrivSqZeroExt.fst, TrivSqZeroExt.fst_mul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
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))
⊢ (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:
rw [List.zipIdx_cons']

Premises used: List.zipIdx_cons'
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
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)
⊢ (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:
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ᵐᵒᵖ)]

Premises used: Prod.map_snd, List.take_succ_cons, List.map_cons, TrivSqZeroExt.fst_list_prod, id, List.map_map, List.take_zero, one_smul, Function.comp_def, TrivSqZeroExt.snd_mul, List.drop, List.sum_cons, List.prod_nil, Prod.map_fst, SMulCommClass.smul_comm, List.prod_cons, List.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
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)
⊢ 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:
add_comm _ _

Premises used: add_comm