[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : ↑(reindex R M (Equiv.cast (_ : ι { fst := ai, snd := a }.fst = ι { fst := bi, snd := b }.fst))) a = b
⊢ { fst := ai, snd := a } = { fst := bi, snd := b }
[PROOFSTEP]
subst hi
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a b : ⨂[R] (x : ι ai), M
h : ↑(reindex R M (Equiv.cast (_ : ι { fst := ai, snd := a }.fst = ι { fst := ai, snd := b }.fst))) a = b
⊢ { fst := ai, snd := a } = { fst := ai, snd := b }
[PROOFSTEP]
simp_all
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(cast R M h) a.snd = b.snd
⊢ a = b
[PROOFSTEP]
refine' gradedMonoid_eq_of_reindex_cast h _
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(cast R M h) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
[PROOFSTEP]
rw [cast] at h2 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M
h : a.fst = b.fst
h2 : ↑(reindex R M (Fin.castIso h).toEquiv) a.snd = b.snd
⊢ ↑(reindex R M (Equiv.cast (_ : Fin a.fst = Fin b.fst))) a.snd = b.snd
[PROOFSTEP]
rw [← Fin.castIso_to_equiv, ← h2]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
h : i = j
⊢ ↑(cast R M h) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^j) M)
[PROOFSTEP]
subst h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(cast R M (_ : i = i)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
[PROOFSTEP]
rw [cast_refl]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ℕ
⊢ ↑(LinearEquiv.refl R ((⨂[R]^i) M)) = _root_.cast (_ : (⨂[R]^i) M = (⨂[R]^i) M)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
dsimp [gMul_def, mulEquiv]
[GOAL]
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)
[PROOFSTEP]
rw [tmulEquiv_apply R M a b]
[GOAL]
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)
[PROOFSTEP]
refine' (reindex_tprod _ _).trans _
[GOAL]
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)
[PROOFSTEP]
congr 1
[GOAL]
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
[PROOFSTEP]
dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]
[GOAL]
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
[PROOFSTEP]
apply funext
[GOAL]
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
[PROOFSTEP]
apply Fin.addCases
[GOAL]
case h.e_6.h.h.left
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
⊢ ∀ (i : Fin na), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.castAdd nb i)) = Fin.addCases a b (Fin.castAdd nb i)
[PROOFSTEP]
simp
[GOAL]
case h.e_6.h.h.right
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
⊢ ∀ (i : Fin nb), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.natAdd na i)) = Fin.addCases a b (Fin.natAdd na i)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : 0 + n = n)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
[PROOFSTEP]
rw [gMul_def, gOne_def]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] a)) = a
[PROOFSTEP]
induction' a using PiTensorProduct.induction_on with r a x y hx hy
[GOAL]
case C1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ ↑(cast R M (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (r • ↑(tprod R) a))) = r • ↑(tprod R) a
[PROOFSTEP]
rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod, cast_tprod]
[GOAL]
case C1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ r • ↑(tprod R) (Fin.append Fin.elim0' a ∘ ↑(Fin.castIso (_ : n = 0 + n))) = r • ↑(tprod R) a
[PROOFSTEP]
congr 2 with i
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ (Fin.append Fin.elim0' a ∘ ↑(Fin.castIso (_ : n = 0 + n))) i = a i
[PROOFSTEP]
rw [Fin.elim0'_append]
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ((a ∘ ↑(Fin.castIso (_ : 0 + n = n))) ∘ ↑(Fin.castIso (_ : n = 0 + n))) i = a i
[PROOFSTEP]
refine' congr_arg a (Fin.ext _)
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ↑(↑(Fin.castIso (_ : 0 + n = n)) (↑(Fin.castIso (_ : n = 0 + n)) i)) = ↑i
[PROOFSTEP]
simp
[GOAL]
case Cp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : ↑(cast R M (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] x)) = x
hy : ↑(cast R M (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] y)) = y
⊢ ↑(cast R M (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (x + y))) = x + y
[PROOFSTEP]
rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : n + 0 = n)) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
[PROOFSTEP]
rw [gMul_def, gOne_def]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : n + 0 = n)) (↑mulEquiv (a ⊗ₜ[R] ↑(tprod R) Fin.elim0')) = a
[PROOFSTEP]
induction' a using PiTensorProduct.induction_on with r a x y hx hy
[GOAL]
case C1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ ↑(cast R M (_ : n + 0 = n)) (↑mulEquiv ((r • ↑(tprod R) a) ⊗ₜ[R] ↑(tprod R) Fin.elim0')) = r • ↑(tprod R) a
[PROOFSTEP]
rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod R a _,
  cast_tprod]
[GOAL]
case C1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ r • ↑(tprod R) (Fin.append a Fin.elim0' ∘ ↑(Fin.castIso (_ : n = n + 0))) = r • ↑(tprod R) a
[PROOFSTEP]
congr 2 with i
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ (Fin.append a Fin.elim0' ∘ ↑(Fin.castIso (_ : n = n + 0))) i = a i
[PROOFSTEP]
rw [Fin.append_elim0']
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ((a ∘ ↑(Fin.castIso (_ : n + 0 = n))) ∘ ↑(Fin.castIso (_ : n = n + 0))) i = a i
[PROOFSTEP]
refine' congr_arg a (Fin.ext _)
[GOAL]
case C1.e_a.h.e_6.h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ↑(↑(Fin.castIso (_ : n + 0 = n)) (↑(Fin.castIso (_ : n = n + 0)) i)) = ↑i
[PROOFSTEP]
simp
[GOAL]
case Cp
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : ↑(cast R M (_ : n + 0 = n)) (↑mulEquiv (x ⊗ₜ[R] ↑(tprod R) Fin.elim0')) = x
hy : ↑(cast R M (_ : n + 0 = n)) (↑mulEquiv (y ⊗ₜ[R] ↑(tprod R) Fin.elim0')) = y
⊢ ↑(cast R M (_ : n + 0 = n)) (↑mulEquiv ((x + y) ⊗ₜ[R] ↑(tprod R) Fin.elim0')) = x + y
[PROOFSTEP]
rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
let mul : ∀ n m : ℕ, (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M := fun n m =>
  (TensorProduct.mk R _ _).compr₂
    ↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(n + m)) M)
        -- replace `a`, `b`, `c` with `tprod R a`, `tprod R b`, `tprod R c`
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
let e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (add_assoc _ _ _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
let lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  (LinearMap.llcomp R _ _ _ ((mul _ nc).compr₂ e.toLinearMap)).comp (mul na nb)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
have lhs_eq : ∀ a b c, lhs a b c = e (a ₜ* b ₜ* c) := fun _ _ _ => rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
let rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  (LinearMap.llcomp R _ _ _ (LinearMap.lflip (R := R)) <|
      (LinearMap.llcomp R _ _ _ (mul na _).flip).comp (mul nb nc)).flip
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
have rhs_eq : ∀ a b c, rhs a b c = a ₜ* (b ₜ* c) := fun _ _ _ => rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
[PROOFSTEP]
suffices : lhs = rhs
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
this : lhs = rhs
⊢ ↑(cast R M (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
case this
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
⊢ lhs = rhs
[PROOFSTEP]
exact LinearMap.congr_fun (LinearMap.congr_fun (LinearMap.congr_fun this a) b) c
[GOAL]
case this
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : (⨂[R]^na) M
b : (⨂[R]^nb) M
c : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
⊢ lhs = rhs
[PROOFSTEP]
ext a b c
[GOAL]
case this.H.H.H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : (⨂[R]^na) M
b✝ : (⨂[R]^nb) M
c✝ : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
⊢ ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap (↑(LinearMap.compMultilinearMap lhs (tprod R)) a) (tprod R)) b) (tprod R))
      c =
    ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap (↑(LinearMap.compMultilinearMap rhs (tprod R)) a) (tprod R)) b) (tprod R))
      c
[PROOFSTEP]
simp only [LinearMap.compMultilinearMap_apply, lhs_eq, rhs_eq, tprod_mul_tprod, cast_tprod]
[GOAL]
case this.H.H.H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : (⨂[R]^na) M
b✝ : (⨂[R]^nb) M
c✝ : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
⊢ ↑(tprod R) (Fin.append (Fin.append a b) c ∘ ↑(Fin.castIso (_ : na + (nb + nc) = na + nb + nc))) =
    ↑(tprod R) (Fin.append a (Fin.append b c))
[PROOFSTEP]
congr with j
[GOAL]
case this.H.H.H.H.H.H.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 nc : ℕ
a✝ : (⨂[R]^na) M
b✝ : (⨂[R]^nb) M
c✝ : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ (Fin.append (Fin.append a b) c ∘ ↑(Fin.castIso (_ : na + (nb + nc) = na + nb + nc))) j =
    Fin.append a (Fin.append b c) j
[PROOFSTEP]
rw [Fin.append_assoc]
[GOAL]
case this.H.H.H.H.H.H.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 nc : ℕ
a✝ : (⨂[R]^na) M
b✝ : (⨂[R]^nb) M
c✝ : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ((Fin.append a (Fin.append b c) ∘ ↑(Fin.castIso (_ : na + nb + nc = na + (nb + nc)))) ∘
        ↑(Fin.castIso (_ : na + (nb + nc) = na + nb + nc)))
      j =
    Fin.append a (Fin.append b c) j
[PROOFSTEP]
refine' congr_arg (Fin.append a (Fin.append b c)) (Fin.ext _)
[GOAL]
case this.H.H.H.H.H.H.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 nc : ℕ
a✝ : (⨂[R]^na) M
b✝ : (⨂[R]^nb) M
c✝ : (⨂[R]^nc) M
mul : (n m : ℕ) → (⨂[R]^n) M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M :=
  fun n m => LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^n) M) ((⨂[R]^m) M)) ↑mulEquiv
e : (⨂[R]^(na + nb + nc)) M ≃ₗ[R] (⨂[R]^(na + (nb + nc))) M := cast R M (_ : na + nb + nc = na + (nb + nc))
lhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.comp
    (↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^(na + nb)) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
      (LinearMap.compr₂ (mul (na + nb) nc) ↑e))
    (mul na nb)
lhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑lhs a) b) c = ↑e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : (⨂[R]^na) M →ₗ[R] (⨂[R]^nb) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M :=
  LinearMap.flip
    (↑(↑(LinearMap.llcomp R ((⨂[R]^nb) M) ((⨂[R]^nc) M →ₗ[R] (⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M)
              ((⨂[R]^na) M →ₗ[R] (⨂[R]^nc) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          LinearMap.lflip)
      (LinearMap.comp
        (↑(LinearMap.llcomp R ((⨂[R]^nc) M) ((⨂[R]^(nb + nc)) M) ((⨂[R]^na) M →ₗ[R] (⨂[R]^(na + (nb + nc))) M))
          (LinearMap.flip (mul na (nb + nc))))
        (mul nb nc)))
rhs_eq :
  ∀ (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M),
    ↑(↑(↑rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ↑(↑(Fin.castIso (_ : na + nb + nc = na + (nb + nc))) (↑(Fin.castIso (_ : na + (nb + nc) = na + nb + nc)) j)) = ↑j
[PROOFSTEP]
rw [Fin.coe_castIso, Fin.coe_castIso]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ↑algebraMap₀ r = r • GradedMonoid.GOne.one
[PROOFSTEP]
simp [algebraMap₀]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ r • ↑(tprod R) isEmptyElim = r • GradedMonoid.GOne.one
[PROOFSTEP]
congr
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : 0 + n = n)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) a) = r • a
[PROOFSTEP]
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul₂, LinearEquiv.map_smul, ← gMul_eq_coe_linearMap,
  one_mul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : (⨂[R]^n) M
⊢ ↑(cast R M (_ : n + 0 = n)) (GradedMonoid.GMul.mul a (↑algebraMap₀ r)) = r • a
[PROOFSTEP]
rw [gMul_eq_coe_linearMap, algebraMap₀_eq_smul_one, LinearMap.map_smul, LinearEquiv.map_smul, ← gMul_eq_coe_linearMap,
  mul_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = ↑algebraMap₀ (r * s)
[PROOFSTEP]
rw [← smul_eq_mul, LinearEquiv.map_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = r • ↑algebraMap₀ s
[PROOFSTEP]
exact algebraMap₀_mul r (@algebraMap₀ R M _ _ _ s)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : GradedMonoid.GMonoid fun i => (⨂[R]^i) M := gmonoid
⊢ (fun n => ↑algebraMap₀ ↑n) 0 = 0
[PROOFSTEP]
simp only [Nat.cast_zero, map_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
src✝ : GradedMonoid.GMonoid fun i => (⨂[R]^i) M := gmonoid
n : ℕ
⊢ (fun n => ↑algebraMap₀ ↑n) (n + 1) = (fun n => ↑algebraMap₀ ↑n) n + GradedMonoid.GOne.one
[PROOFSTEP]
simp only [Nat.cast_succ, map_add, algebraMap₀_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Semiring (⨁ (n : ℕ), (⨂[R]^n) M)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ ↑(cast R M
          (_ :
            (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst =
              (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst))
      (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).snd =
    { fst := 0 + 0,
        snd :=
          GradedMonoid.GMul.mul (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)
            (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) s) }.snd
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
⊢ (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).snd =
    ↑(LinearEquiv.symm
          (cast R M
            (_ :
              (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst =
                (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst)))
      { fst := 0 + 0,
          snd :=
            GradedMonoid.GMul.mul (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)
              (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) s) }.snd
[PROOFSTEP]
have := algebraMap₀_mul_algebraMap₀ (M := M) r s
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
this : ↑(cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) (↑algebraMap₀ s)) = ↑algebraMap₀ (r * s)
⊢ (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).snd =
    ↑(LinearEquiv.symm
          (cast R M
            (_ :
              (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst =
                (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) (r * s))).fst)))
      { fst := 0 + 0,
          snd :=
            GradedMonoid.GMul.mul (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)
              (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) s) }.snd
[PROOFSTEP]
exact this.symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
⊢ ↑(cast R M
          (_ :
            (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)).fst + x.fst =
              x.fst + (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)).fst))
      (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).snd =
    (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).snd
[PROOFSTEP]
have := (algebraMap₀_mul r x.snd).trans (mul_algebraMap₀ r x.snd).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
this :
  ↑(cast R M (_ : 0 + x.fst = x.fst)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) x.snd) =
    ↑(cast R M (_ : x.fst + 0 = x.fst)) (GradedMonoid.GMul.mul x.snd (↑algebraMap₀ r))
⊢ ↑(cast R M
          (_ :
            (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)).fst + x.fst =
              x.fst + (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r)).fst))
      (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).snd =
    (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).snd
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply, cast_symm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
this :
  ↑(cast R M (_ : 0 + x.fst = x.fst)) (GradedMonoid.GMul.mul (↑algebraMap₀ r) x.snd) =
    ↑(cast R M (_ : x.fst + 0 = x.fst)) (GradedMonoid.GMul.mul x.snd (↑algebraMap₀ r))
⊢ (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).snd =
    ↑(cast R M
          (_ :
            (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).fst =
              (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).fst))
      (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).snd
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
this :
  GradedMonoid.GMul.mul (↑algebraMap₀ r) x.snd =
    ↑(cast R M (_ : x.fst + 0 = 0 + x.fst)) (GradedMonoid.GMul.mul x.snd (↑algebraMap₀ r))
⊢ (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).snd =
    ↑(cast R M
          (_ :
            (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).fst =
              (GradedMonoid.mk 0 (↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r) * x).fst))
      (x * { fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r }).snd
[PROOFSTEP]
exact this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
⊢ ↑(cast R M (_ : x.fst = 0 + x.fst)) (GradedMonoid.mk x.fst (r • x.snd)).snd =
    ({ fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r } * x).snd
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply, cast_symm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i => (⨂[R]^i) M
⊢ (GradedMonoid.mk x.fst (r • x.snd)).snd =
    ↑(cast R M
          (_ :
            ({ fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r } * x).fst =
              (GradedMonoid.mk x.fst (r • x.snd)).fst))
      ({ fst := 0, snd := ↑(LinearMap.toAddMonoidHom ↑algebraMap₀) r } * x).snd
[PROOFSTEP]
exact (algebraMap₀_mul r x.snd).symm
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Algebra R (⨁ (n : ℕ), (⨂[R]^n) M)
[PROOFSTEP]
infer_instance
