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
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
rw [gMul_def, gOne_def]
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

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
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
induction' a using PiTensorProduct.induction_on with r a x y hx hy
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
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
dsimp only at a
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.cast (_ : n = n + 0))) = r • ↑(tprod R) a
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
rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
  tprod_mul_tprod R a _, cast_tprod]
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.cast (_ : n = n + 0))) i = a i
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.cast (_ : n = n + 0))) = r • ↑(tprod R) a
congr 2 with i
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.cast (_ : n + 0 = n))) ∘ ↑(Fin.cast (_ : n = n + 0))) i = a i
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.cast (_ : n = n + 0))) i = a i
rw [Fin.append_elim0']
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.cast (_ : n + 0 = n)) (↑(Fin.cast (_ : n = n + 0)) i)) = ↑i
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.cast (_ : n + 0 = n))) ∘ ↑(Fin.cast (_ : n = n + 0))) i = a i
refine' congr_arg a (Fin.ext _)
no goals
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.cast (_ : n + 0 = n)) (↑(Fin.cast (_ : n = n + 0)) i)) = ↑i
simp
no goals
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
rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]