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

Tactic:
simp_rw [Fin.append_left_eq_cons, Function.comp_def]

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) fun x_1 => Fin.cons x₀ x (Fin.cast ⋯ (Fin.cast ⋯ x_1))) =
    (PiTensorProduct.tprod R) (Fin.cons x₀ x)

Proof state:
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)

Tactic:
rw [List.finRange_zero, List.map_nil, List.prod_nil]

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ 1 = GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

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)
⊢ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x => x₀) *
      (List.map (fun x_1 => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_2 => x x_1)) (List.finRange n)).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_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)
⊢ GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    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)
⊢ ((PiTensorProduct.tprod R) fun x_1 => Fin.cons x₀ x (Fin.cast ⋯ (Fin.cast ⋯ x_1))) =
    (PiTensorProduct.tprod R) (Fin.cons x₀ x)

Tactic:
congr 1 with i

Result:
no goals

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)
⊢ 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))

Tactic:
simp_rw [Function.comp_def, Fin.cons_zero, Fin.cons_succ]

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 => x₀) *
      (List.map (fun x_1 => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_2 => x x_1)) (List.finRange n)).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 ⋯) (GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x))).snd =
    (GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))).snd

Tactic:
dsimp only [GradedMonoid.mk]

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)
⊢ (TensorPower.cast R M ⋯) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    (PiTensorProduct.tprod R) (Fin.cons x₀ x)

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ 1 = GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

Tactic:
rfl

Result:
no goals

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)
⊢ GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
refine TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_

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)
⊢ (TensorPower.cast R M ⋯) (GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x))).snd =
    (GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))).snd