-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem tprod_mul_tprod {na nb} (a : Fin na → M) (b : Fin nb → M) :
    tprod R a ₜ* tprod R b = tprod R (Fin.append a b)

Proof state:
case h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (x : Fin (na + nb)), Sum.elim a b (Fin.addCases Sum.inl Sum.inr x) = Fin.addCases a b x

Tactic:
apply Fin.addCases <;> simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ GradedMonoid.GMul.mul ((tprod R) a) ((tprod R) b) = (tprod R) (Fin.append a b)

Tactic:
dsimp [gMul_def, mulEquiv]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (reindex R (fun x => M) finSumFinEquiv) ((tmulEquiv R M) ((tprod R) a ⊗ₜ[R] (tprod R) b)) = (tprod R) (Fin.append a b)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ((tprod R) fun i => Sum.elim a b (finSumFinEquiv.symm i)) = (tprod R) (Fin.append a b)

Tactic:
congr 1

Result:
case h.e_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (fun i => Sum.elim a b (finSumFinEquiv.symm i)) = Fin.append a b

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (reindex R (fun x => M) finSumFinEquiv) ((tprod R) fun i => Sum.elim a b i) = (tprod R) (Fin.append a b)

Tactic:
refine (reindex_tprod _ _).trans ?_

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ((tprod R) fun i => Sum.elim a b (finSumFinEquiv.symm i)) = (tprod R) (Fin.append a b)

Proof state:
case h.e_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (fun i => Sum.elim a b (Fin.addCases Sum.inl Sum.inr i)) = Fin.addCases a b

Tactic:
apply funext

Result:
case h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (x : Fin (na + nb)), Sum.elim a b (Fin.addCases Sum.inl Sum.inr x) = Fin.addCases a b x

Proof state:
case h.e_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (fun i => Sum.elim a b (finSumFinEquiv.symm i)) = Fin.append a b

Tactic:
dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]

Result:
case h.e_6.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (fun i => Sum.elim a b (Fin.addCases Sum.inl Sum.inr i)) = Fin.addCases a b

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (reindex R (fun x => M) finSumFinEquiv) ((tmulEquiv R M) ((tprod R) a ⊗ₜ[R] (tprod R) b)) = (tprod R) (Fin.append a b)

Tactic:
rw [tmulEquiv_apply R M a b]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (reindex R (fun x => M) finSumFinEquiv) ((tprod R) fun i => Sum.elim a b i) = (tprod R) (Fin.append a b)