-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem _root_.TensorPower.list_prod_gradedMonoid_mk_single (n : ℕ) (x : Fin n → M) :
    ((List.finRange n).map fun a =>
          (GradedMonoid.mk _ (PiTensorProduct.tprod R fun _ : Fin 1 => x a) :
            GradedMonoid fun n => ⨂[R]^n M)).prod =
      GradedMonoid.mk n (PiTensorProduct.tprod R x)

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
        GradedMonoid.mk n ((PiTensorProduct.tprod R) x) →
      (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x a))
            (List.finRange (n + 1))).prod =
        GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
intro n x₀ x ih

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x a))
        (List.finRange (n + 1))).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x a))
        (List.finRange (n + 1))).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
rw [List.finRange_succ_eq_map, List.map_cons, List.prod_cons, List.map_map]

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x 0) *
      (List.map ((fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x a)) ∘ Fin.succ)
          (List.finRange n)).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)

Tactic:
refine Fin.consInduction ?_ ?_ x <;> clear x

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x => a.elim0)) (List.finRange 0)).prod =
    GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
        GradedMonoid.mk n ((PiTensorProduct.tprod R) x) →
      (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x a))
            (List.finRange (n + 1))).prod =
        GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (TensorPower.cast R M ⋯) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    (PiTensorProduct.tprod R) (Fin.cons x₀ x)

Tactic:
rw [TensorPower.cast_tprod]

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x ∘ Fin.cast ⋯) = (PiTensorProduct.tprod R) (Fin.cons x₀ x)