-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toDirectSum_tensorPower_tprod {n} (x : Fin n → M) :
    toDirectSum (tprod R M n x) = DirectSum.of _ n (PiTensorProduct.tprod R x)

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

Tactic:
rw [GradedMonoid.mk_list_dProd]

Result:
case h
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)

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.ofFn fun x_1 => (DirectSum.of (fun n => ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_2 => x x_1)).prod =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
rw [DirectSum.list_prod_ofFn_of_eq_dProd]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (DirectSum.of (fun n => ⨂[R]^n M) ((List.finRange n).dProdIndex fun x => 1))
      ((List.finRange n).dProd (fun x => 1) fun x_1 => (PiTensorProduct.tprod R) fun x_2 => x x_1) =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Proof state:
case h
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:
rw [TensorPower.list_prod_gradedMonoid_mk_single]

Result:
no goals

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
⊢ (DirectSum.of (fun n => ⨂[R]^n M) ((List.finRange n).dProdIndex fun x => 1))
      ((List.finRange n).dProd (fun x => 1) fun x_1 => (PiTensorProduct.tprod R) fun x_2 => x x_1) =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
apply DirectSum.of_eq_of_gradedMonoid_eq

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ GradedMonoid.mk ((List.finRange n).dProdIndex fun x => 1)
      ((List.finRange n).dProd (fun x => 1) fun x_1 => (PiTensorProduct.tprod R) fun x_2 => x x_1) =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) 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.ofFn (⇑toDirectSum ∘ fun i => (ι R) (x i))).prod =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
simp_rw [Function.comp_def, toDirectSum_ι]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (List.ofFn fun x_1 => (DirectSum.of (fun n => ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_2 => x x_1)).prod =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) 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
⊢ toDirectSum ((tprod R M n) x) = (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
rw [tprod_apply, map_list_prod, List.map_ofFn]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (List.ofFn (⇑toDirectSum ∘ fun i => (ι R) (x i))).prod =
    (DirectSum.of (fun i => ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)