-- Mathlib/LinearAlgebra/TensorPower/Basic.lean
theorem mul_one {n} (a : ⨂[R]^n M) : cast R M (add_zero _) (a ₜ* ₜ1) = a

Proof state:
case add
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 ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) = x
hy : (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = y
⊢ (cast R M ⋯) (mulEquiv ((x + y) ⊗ₜ[R] (tprod R) Fin.elim0)) = x + y

Tactic:
rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]

Result:
no goals

Proof state:
case smul_tprod.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 ⋯) i = a i

Tactic:
rw [Fin.append_elim0]

Result:
case smul_tprod.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 ⋯) ∘ Fin.cast ⋯) i = a i

Proof state:
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 ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a

Tactic:
rw [gMul_def, gOne_def]

Result:
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 ⋯) (mulEquiv (a ⊗ₜ[R] (tprod R) Fin.elim0)) = a

Proof state:
case smul_tprod
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 ⋯) (mulEquiv ((r • (tprod R) a) ⊗ₜ[R] (tprod R) Fin.elim0)) = r • (tprod R) a

Tactic:
rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
  tprod_mul_tprod R a _, cast_tprod]

Result:
case smul_tprod
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 ⋯) = r • (tprod R) a

Proof state:
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 ⋯) (mulEquiv (a ⊗ₜ[R] (tprod R) Fin.elim0)) = a

Tactic:
induction a using PiTensorProduct.induction_on with
| smul_tprod r a =>
  rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
    tprod_mul_tprod R a _, cast_tprod]
  congr 2 with i
  rw [Fin.append_elim0]
  refine congr_arg a (Fin.ext ?_)
  simp
| add x y hx hy =>
  rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]

Result:
no goals

Proof state:
case smul_tprod.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 ⋯ (Fin.cast ⋯ i)) = ↑i

Tactic:
simp

Result:
no goals

Proof state:
case smul_tprod
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 ⋯) = r • (tprod R) a

Tactic:
congr 2 with i

Result:
case smul_tprod.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 ⋯) i = a i

Proof state:
case smul_tprod.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 ⋯) ∘ Fin.cast ⋯) i = a i

Tactic:
refine congr_arg a (Fin.ext ?_)

Result:
case smul_tprod.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 ⋯ (Fin.cast ⋯ i)) = ↑i