-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toTensorAlgebra_gMul {i j} (a : (⨂[R]^i) M) (b : (⨂[R]^j) M) :
    TensorPower.toTensorAlgebra (@GradedMonoid.GMul.mul _ (fun n => ⨂[R]^n M) _ _ _ _ a b) =
      TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b

Proof state:
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 : Fin i → M
b : Fin j → M
⊢ toTensorAlgebra (GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b)) =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b)

Tactic:
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]

Result:
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 : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod =
    (List.ofFn fun i => (TensorAlgebra.ι R) (a i)).prod * (List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod

Proof state:
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
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b

Tactic:
refine LinearMap.congr_fun (LinearMap.congr_fun ?_ a) b

Result:
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
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

Tactic:
ext (a b)

Result:
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 : Fin i → M
b : Fin j → M
⊢ ((((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b =
    (((((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b

Proof state:
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 : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod =
    (List.ofFn fun i => (TensorAlgebra.ι R) (a i)).prod * (List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod

Tactic:
refine Eq.trans ?_ List.prod_append

Result:
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 : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod =
    ((List.ofFn fun i => (TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod

Proof state:
case H.H.H.H.e_a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
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)

Tactic:
erw [← List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_ofFn _ (TensorAlgebra.ι R), ←
  List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]

Result:
no goals

Proof state:
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
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

Tactic:
clear! a b

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

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

Tactic:
rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ←
  LinearMap.compl₂_apply, ← LinearMap.comp_apply]

Result:
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
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b

Proof state:
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 : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => (TensorAlgebra.ι R) (Fin.append a b i_1)).prod =
    ((List.ofFn fun i => (TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => (TensorAlgebra.ι R) (b i)).prod

Tactic:
congr

Result:
case H.H.H.H.e_a
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
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)

Proof state:
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 : Fin i → M
b : Fin j → M
⊢ ((((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b =
    (((((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b

Tactic:
simp only [LinearMap.compMultilinearMap_apply]

Result:
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 : Fin i → M
b : Fin j → M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b) =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b)