[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ ↑toTensorAlgebra (GradedMonoid.GMul.mul a b) = ↑toTensorAlgebra a * ↑toTensorAlgebra b
[PROOFSTEP]
rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ← LinearMap.compl₂_apply, ←
  LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ ↑(↑(LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra) a)
      b =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra)
              toTensorAlgebra)
          a)
      b
[PROOFSTEP]
refine' LinearMap.congr_fun (LinearMap.congr_fun _ a) b
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra =
    LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra) toTensorAlgebra
[PROOFSTEP]
clear! a b
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
⊢ LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra =
    LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra) toTensorAlgebra
[PROOFSTEP]
ext
  (a b)
    -- Porting note: pulled the next two lines out of the long `simp only` below.
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv)
                  toTensorAlgebra)
                (PiTensorProduct.tprod R))
            a)
          (PiTensorProduct.tprod R))
      b =
    ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
                  toTensorAlgebra)
                (PiTensorProduct.tprod R))
            a)
          (PiTensorProduct.tprod R))
      b
[PROOFSTEP]
simp only [LinearMap.compMultilinearMap_apply]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑(↑(LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b) =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
              toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b)
[PROOFSTEP]
rw [LinearMap.compr₂_apply, ← gMul_eq_coe_linearMap]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑toTensorAlgebra (GradedMonoid.GMul.mul (↑(PiTensorProduct.tprod R) a) (↑(PiTensorProduct.tprod R) b)) =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
              toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b)
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, LinearMap.mul_apply', LinearMap.compl₂_apply, LinearMap.comp_apply,
  LinearMap.compMultilinearMap_apply, PiTensorProduct.lift.tprod, TensorPower.tprod_mul_tprod,
  TensorPower.toTensorAlgebra_tprod, TensorAlgebra.tprod_apply, ← gMul_eq_coe_linearMap]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ List.prod (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    List.prod (List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) *
      List.prod (List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i))
[PROOFSTEP]
refine' Eq.trans _ List.prod_append
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ List.prod (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    List.prod ((List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i))
[PROOFSTEP]
apply congr_arg
[GOAL]
case H.H.H.H.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    (List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i)
[PROOFSTEP]
erw [← List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_ofFn _ (TensorAlgebra.ι R), ←
  List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ↑toTensorAlgebra (↑DirectSum.GAlgebra.toFun r) = ↑(algebraMap R (TensorAlgebra R M)) r
[PROOFSTEP]
rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, LinearMap.map_smul,
  TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ AlgHom.comp ofDirectSum toDirectSum = AlgHom.id R (TensorAlgebra R M)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp ofDirectSum toDirectSum)) (ι R)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M))) (ι R)) x✝
[PROOFSTEP]
simp [DirectSum.lof_eq_of, tprod_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n m : ℕ
h : n = m
x : (⨂[R]^n) M
⊢ GradedMonoid.mk m (↑(PiTensorProduct.reindex R M (Fin.castIso h).toEquiv) x) = GradedMonoid.mk n x
[PROOFSTEP]
rw [Fin.castIso_to_equiv, mk_reindex_cast h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
refine' Fin.consInduction _ _ x
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), Fin.elim0 a)) (List.finRange 0)) =
    GradedMonoid.mk 0 (↑(PiTensorProduct.tprod R) Fin.elim0)
[PROOFSTEP]
clear x
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
        GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x) →
      List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
        GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
clear x
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), Fin.elim0 a)) (List.finRange 0)) =
    GradedMonoid.mk 0 (↑(PiTensorProduct.tprod R) Fin.elim0)
[PROOFSTEP]
rw [List.finRange_zero, List.map_nil, List.prod_nil]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
        GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x) →
      List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
        GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
intro n x₀ x ih
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
rw [List.finRange_succ_eq_map, List.map_cons, List.prod_cons, List.map_map]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x 0) *
      List.prod
        (List.map ((fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) ∘ Fin.succ) (List.finRange n)) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
simp_rw [Function.comp, Fin.cons_zero, Fin.cons_succ]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), x₀) *
      List.prod (List.map (fun x_1 => GradedMonoid.mk 1 (⨂ₜ[R] (x_2 : Fin 1), x x_1)) (List.finRange n)) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    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))
[PROOFSTEP]
refine' TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) _
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(TensorPower.cast R M (_ : 1 + n = n + 1))
      (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
[PROOFSTEP]
dsimp only [GradedMonoid.mk]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(TensorPower.cast R M (_ : 1 + n = n + 1)) (↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
rw [TensorPower.cast_tprod]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x ∘ ↑(Fin.castIso (_ : n + 1 = 1 + n))) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
simp_rw [Fin.append_left_eq_cons, Function.comp]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ (⨂ₜ[R] (x_1 : Fin (n + 1)),
      Fin.cons x₀ x (↑(Fin.castIso (_ : 1 + n = n + 1)) (↑(Fin.castIso (_ : n + 1 = 1 + n)) x_1))) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
congr 1 with i
[GOAL]
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)
[PROOFSTEP]
rw [tprod_apply, AlgHom.map_list_prod, List.map_ofFn]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.ofFn (↑toDirectSum ∘ fun i => ↑(ι R) (x i))) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
simp_rw [Function.comp, toDirectSum_ι]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.ofFn fun x_1 => ↑(DirectSum.of (fun n => (⨂[R]^n) M) 1) (⨂ₜ[R] (x_2 : Fin 1), x x_1)) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [DirectSum.list_prod_ofFn_of_eq_dProd]
[GOAL]
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.dProdIndex (List.finRange n) fun x => 1))
      (List.dProd (List.finRange n) (fun x => 1) fun x_1 => ⨂ₜ[R] (x_2 : Fin 1), x x_1) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
apply DirectSum.of_eq_of_gradedMonoid_eq
[GOAL]
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.dProdIndex (List.finRange n) fun x => 1)
      (List.dProd (List.finRange n) (fun x => 1) fun x_1 => ⨂ₜ[R] (x_2 : Fin 1), x x_1) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [GradedMonoid.mk_list_dProd]
[GOAL]
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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [TensorPower.list_prod_gradedMonoid_mk_single]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ AlgHom.comp toDirectSum ofDirectSum = AlgHom.id R (⨁ (n : ℕ), (⨂[R]^n) M)
[PROOFSTEP]
ext
[GOAL]
case h.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ : Fin i✝ → M
⊢ ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp toDirectSum ofDirectSum))
            (DirectSum.lof R ℕ (fun i => (⨂[R]^i) M) i✝))
          (PiTensorProduct.tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (n : ℕ), (⨂[R]^n) M)))
            (DirectSum.lof R ℕ (fun i => (⨂[R]^i) M) i✝))
          (PiTensorProduct.tprod R))
      x✝
[PROOFSTEP]
simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]
