-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M)) :
    l.prod.snd =
      (l.zipIdx.map fun x : tsze R M × ℕ =>
          ((l.map fst).take x.2).prod •> x.fst.snd <• ((l.map fst).drop x.2.succ).prod).sum

Proof state:
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    (List.map
        (fun x_1 =>
          (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).sum

Tactic:
rw [List.zipIdx_cons']

Result:
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    (List.map
        (fun x_1 =>
          (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)).sum

Proof state:
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 => x.fst •> x_1) ∘ fun x =>
            (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 =>
            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).sum

Tactic:
exact add_comm _ _

Result:
no goals

Proof state:
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    (List.map
        (fun x_1 =>
          (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)).sum

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ᵐᵒᵖ)]

Result:
case cons
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 => x.fst •> x_1) ∘ fun x =>
            (List.take x.2 (List.map fst xs)).prod •> (x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod))
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 =>
            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).sum

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ l.prod.snd =
    (List.map (fun x => (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx).sum

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 _ _

Result:
no goals

Proof state:
case nil
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
⊢ [].prod.snd =
    (List.map
        (fun x => (List.take x.2 (List.map fst [])).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst [])).prod)
        [].zipIdx).sum

Tactic:
simp

Result:
no goals