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 M finSumFinEquiv) (↑(tmulEquiv R M) (↑(tprod R) a ⊗ₜ[R] ↑(tprod R) b)) = ↑(tprod R) (Fin.append a b)
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)
dsimp [gMul_def, mulEquiv]
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 M finSumFinEquiv) (⨂ₜ[R] (i : Fin na ⊕ Fin nb), Sum.elim a b i) = ↑(tprod R) (Fin.append a b)
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 M finSumFinEquiv) (↑(tmulEquiv R M) (↑(tprod R) a ⊗ₜ[R] ↑(tprod R) b)) = ↑(tprod R) (Fin.append a b)
rw [tmulEquiv_apply R M a b]
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
⊢ (⨂ₜ[R] (i : Fin (na + nb)), Sum.elim a b (↑finSumFinEquiv.symm i)) = ↑(tprod R) (Fin.append a b)
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 M finSumFinEquiv) (⨂ₜ[R] (i : Fin na ⊕ Fin nb), Sum.elim a b i) = ↑(tprod R) (Fin.append a b)
refine' (reindex_tprod _ _).trans _
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
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
⊢ (⨂ₜ[R] (i : Fin (na + nb)), Sum.elim a b (↑finSumFinEquiv.symm i)) = ↑(tprod R) (Fin.append a b)
congr 1
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
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
dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]
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
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
apply funext
no goals
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
apply Fin.addCases <;> simp