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

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

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 Fin.elim0 a ∘ Fin.cast ⋯) i = a i

Tactic:
rw [Fin.elim0_append]

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

Tactic:
induction a using PiTensorProduct.induction_on with
| smul_tprod r a =>
  rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
    tprod_mul_tprod, cast_tprod]
  congr 2 with i
  rw [Fin.elim0_append]
  refine congr_arg a (Fin.ext ?_)
  simp
| add x y hx hy =>
  rw [TensorProduct.tmul_add, 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:
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 GradedMonoid.GOne.one a) = 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 ((tprod R) Fin.elim0 ⊗ₜ[R] a)) = 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
⊢ r • (tprod R) (Fin.append Fin.elim0 a ∘ 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 Fin.elim0 a ∘ Fin.cast ⋯) i = a i

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

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

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
⊢ (cast R M ⋯) (mulEquiv ((tprod R) Fin.elim0 ⊗ₜ[R] (r • (tprod R) a))) = r • (tprod R) a

Tactic:
rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
  tprod_mul_tprod, 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 Fin.elim0 a ∘ Fin.cast ⋯) = r • (tprod R) a