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
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
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 (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (r • ↑(tprod R) a))) = 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 (_ : 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
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
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 (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (r • ↑(tprod R) a))) = 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 (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (r • ↑(tprod R) a))) = 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 Fin.elim0' a ∘ ↑(Fin.cast (_ : n = 0 + n))) = 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 (_ : 0 + n = n)) (↑mulEquiv (↑(tprod R) Fin.elim0' ⊗ₜ[R] (r • ↑(tprod R) a))) = r • ↑(tprod R) a
rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
  tprod_mul_tprod, 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 Fin.elim0' a ∘ ↑(Fin.cast (_ : n = 0 + n))) 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 Fin.elim0' a ∘ ↑(Fin.cast (_ : n = 0 + n))) = 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 (_ : 0 + n = n))) ∘ ↑(Fin.cast (_ : n = 0 + n))) 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 Fin.elim0' a ∘ ↑(Fin.cast (_ : n = 0 + n))) i = a i
rw [Fin.elim0'_append]
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 (_ : 0 + n = n)) (↑(Fin.cast (_ : n = 0 + n)) 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 (_ : 0 + n = n))) ∘ ↑(Fin.cast (_ : n = 0 + n))) 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 (_ : 0 + n = n)) (↑(Fin.cast (_ : n = 0 + n)) 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 (_ : 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
rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]