awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
rw :
  Eq (α := (a : ⨂[R]^i M) → ⨂[R]^i M)
    ((⇑(LinearEquiv.refl R (⨂[R]^i M)) : (a : ⨂[R]^i M) → ⨂[R]^i M) : (a : ⨂[R]^i M) → ⨂[R]^i M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)
⊢ Eq (α := (a : ⨂[R]^i M) → ⨂[R]^i M) ((⇑(cast R M ⋯) : (a : ⨂[R]^i M) → ⨂[R]^i M) : (a : ⨂[R]^i M) → ⨂[R]^i M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)

Tactic:
rw [cast_refl]

Premises used: TensorPower.cast_refl
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
i : ℕ
⊢ Eq (α := (a : ⨂[R]^i M) → ⨂[R]^i M)
    ((⇑(LinearEquiv.refl R (⨂[R]^i M)) : (a : ⨂[R]^i M) → ⨂[R]^i M) : (a : ⨂[R]^i M) → ⨂[R]^i M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
rw :
  Eq (α := ⨂[R]^(na + nb) M)
    ((reindex R (fun (x : Fin na ⊕ Fin nb) ↦ M) finSumFinEquiv : (a : ⨂[R] (x : Fin na ⊕ Fin nb), M) → ⨂[R]^(na + nb) M)
      ((tprod R (s := fun (i : Fin na ⊕ Fin nb) ↦ M) : (a : (i : Fin na ⊕ Fin nb) → M) → ⨂[R] (i : Fin na ⊕ Fin nb), M)
        fun (i : Fin na ⊕ Fin nb) ↦ Sum.elim a b i))
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
      (Fin.append a b))
⊢ Eq (α := ⨂[R]^(na + nb) M)
    ((reindex R (fun (x : Fin na ⊕ Fin nb) ↦ M) finSumFinEquiv : (a : ⨂[R] (x : Fin na ⊕ Fin nb), M) → ⨂[R]^(na + nb) M)
        ((tmulEquiv R M : (a : ⨂[R]^na M ⊗[R] ⨂[R]^nb M) → ⨂[R] (x : Fin na ⊕ Fin nb), M)
          ((tprod R (s := fun (x : Fin na) ↦ M) : (a : (i : Fin na) → M) → ⨂[R] (i : Fin na), M) a ⊗ₜ[R]
            (tprod R (s := fun (x : Fin nb) ↦ M) : (a : (i : Fin nb) → M) → ⨂[R] (i : Fin nb), M) b)) :
      ⨂[R]^(na + nb) M)
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
        (Fin.append a b) :
      ⨂[R] (i : Fin (na + nb)), M)

Tactic:
rw [tmulEquiv_apply R M a b]

Premises used: PiTensorProduct.tmulEquiv_apply
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ Eq (α := ⨂[R]^(na + nb) M)
    ((reindex R (fun (x : Fin na ⊕ Fin nb) ↦ M) finSumFinEquiv : (a : ⨂[R] (x : Fin na ⊕ Fin nb), M) → ⨂[R]^(na + nb) M)
      ((tprod R (s := fun (i : Fin na ⊕ Fin nb) ↦ M) : (a : (i : Fin na ⊕ Fin nb) → M) → ⨂[R] (i : Fin na ⊕ Fin nb), M)
        fun (i : Fin na ⊕ Fin nb) ↦ Sum.elim a b i))
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
      (Fin.append a b))

Tactic:
(reindex_tprod _ _).trans ?_

Premises used: PiTensorProduct.reindex_tprod, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
refine :
  Eq (α := ⨂[R] (i : Fin (na + nb)), M)
    ((tprod R (s := fun (i : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
        fun (i : Fin (na + nb)) ↦ Sum.elim a b ((Equiv.symm finSumFinEquiv : (a : Fin (na + nb)) → Fin na ⊕ Fin nb) i) :
      ⨂[R] (i : Fin (na + nb)), M)
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
        (Fin.append a b) :
      ⨂[R] (i : Fin (na + nb)), M)
⊢ Eq (α := ⨂[R]^(na + nb) M)
    ((reindex R (fun (x : Fin na ⊕ Fin nb) ↦ M) finSumFinEquiv : (a : ⨂[R] (x : Fin na ⊕ Fin nb), M) → ⨂[R]^(na + nb) M)
      ((tprod R (s := fun (i : Fin na ⊕ Fin nb) ↦ M) : (a : (i : Fin na ⊕ Fin nb) → M) → ⨂[R] (i : Fin na ⊕ Fin nb), M)
        fun (i : Fin na ⊕ Fin nb) ↦ Sum.elim a b i))
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
      (Fin.append a b))

Tactic:
refine (reindex_tprod _ _).trans ?_

Premises used: PiTensorProduct.reindex_tprod, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
h :
  (fun (i : Fin (na + nb)) ↦ Sum.elim a b ((Equiv.symm finSumFinEquiv : (a : Fin (na + nb)) → Fin na ⊕ Fin nb) i)) =
    Fin.append a b
⊢ Eq (α := ⨂[R] (i : Fin (na + nb)), M)
    ((tprod R (s := fun (i : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
        fun (i : Fin (na + nb)) ↦ Sum.elim a b ((Equiv.symm finSumFinEquiv : (a : Fin (na + nb)) → Fin na ⊕ Fin nb) i) :
      ⨂[R] (i : Fin (na + nb)), M)
    ((tprod R (s := fun (a : Fin (na + nb)) ↦ M) : (a : (i : Fin (na + nb)) → M) → ⨂[R] (i : Fin (na + nb)), M)
        (Fin.append a b) :
      ⨂[R] (i : Fin (na + nb)), M)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
h :
  Eq.{u_2 + 1} (α := (i : Fin (na + nb)) → M)
    (fun (i : Fin (na + nb)) ↦
      Sum.elim a b (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr i))
    (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b)
⊢ (fun (i : Fin (na + nb)) ↦ Sum.elim a b ((Equiv.symm finSumFinEquiv : (a : Fin (na + nb)) → Fin na ⊕ Fin nb) i)) =
    Fin.append a b

Tactic:
dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, finSumFinEquiv, Fin.append
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
h :
  ∀ (x : Fin (na + nb)),
    Sum.elim a b (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr x) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b x
⊢ Eq.{u_2 + 1} (α := (i : Fin (na + nb)) → M)
    (fun (i : Fin (na + nb)) ↦
      Sum.elim a b (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr i))
    (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b)

Tactic:
apply funext

Premises used: funext
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
h :
  ∀ (i : Fin na),
    Sum.elim a b
        (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr (Fin.castAdd nb i)) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b (Fin.castAdd nb i)
h₁ :
  ∀ (i : Fin nb),
    Sum.elim a b
        (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr (Fin.natAdd na i)) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b (Fin.natAdd na i)
⊢ ∀ (x : Fin (na + nb)),
    Sum.elim a b (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr x) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b x

Tactic:
apply Fin.addCases
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin na),
    Sum.elim a b
        (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr (Fin.castAdd nb i)) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b (Fin.castAdd nb i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin nb),
    Sum.elim a b
        (Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ Fin na ⊕ Fin nb) Sum.inl Sum.inr (Fin.natAdd na i)) =
      Fin.addCases (motive := fun (x : Fin (na + nb)) ↦ M) a b (Fin.natAdd na i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] a)) =
    a
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _
        (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) a) =
    a

Tactic:
rw [gMul_def, gOne_def]

Premises used: TensorPower.gMul_def, TensorPower.gOne_def
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
smul_tprod :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M)
          (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) :
        ⨂[R] (i : Fin n), M) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R]
          HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
            ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a :
              ⨂[R] (i : Fin n), M))) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)

Tactic:
rw [TensorProduct.tmul_smul, map_smul, map_smul, ← gMul_def, tprod_mul_tprod, cast_tprod]

Premises used: TensorProduct.tmul_smul, TensorPower.tprod_mul_tprod, TensorPower.gMul_def, TensorPower.cast_tprod, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
smul_tprod : ∀ (i : Fin n), (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) i = a i
⊢ HSMul.hSMul (β := ⨂[R]^n M) r
      ((tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M)
          (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) :
        ⨂[R] (i : Fin n), M) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)

Tactic:
congr 2 with i
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
i : Fin n
smul_tprod : ((a ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) i = a i
⊢ (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) i = a i

Tactic:
rw [Fin.elim0_append]

Premises used: Fin.elim0_append
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
i : Fin n
⊢ ((a ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) i = a i

Tactic:
congr_arg a (Fin.ext ?_)

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
i : Fin n
smul_tprod : (↑(Fin.cast ⋯ (Fin.cast ⋯ i)) : ℕ) = (↑i : ℕ)
⊢ ((a ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) i = a i

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

Premises used: Fin.ext, congr_arg
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
i : Fin n
⊢ (↑(Fin.cast ⋯ (Fin.cast ⋯ i)) : ℕ) = (↑i : ℕ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] x)) =
    x
hy :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y)) =
    y
add :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        (HAdd.hAdd (α := ⨂[R]^0 M ⊗[R] ⨂[R]^n M)
          ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] x)
          ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y))) =
    x + y
add₁ :
  (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      (HAdd.hAdd (α := ⨂[R]^(0 + n) M) (β := ⨂[R]^(0 + n) M)
        ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] x) :
          ⨂[R]^(0 + n) M)
        ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y) :
          ⨂[R]^(0 + n) M)) =
    x + y
add₂ :
  HAdd.hAdd (α := ⨂[R]^n M) (β := ⨂[R]^n M)
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] x)) :
        ⨂[R]^n M)
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y)) :
        ⨂[R]^n M) =
    x + y
add₃ :
  HAdd.hAdd (β := ⨂[R]^n M) x
      ((cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y)) :
        ⨂[R]^n M) =
    x + y
add₄ add₅ : x + y = x + y
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] (x + y))) =
    x + y

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

Premises used: map_add, TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
a : ⨂[R]^n M
smul_tprod :
  ∀ (r : R) (a : (i : Fin n) → M),
    (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
        ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
          ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R]
            HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
              ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a :
                ⨂[R] (i : Fin n), M))) =
      HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
        ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)
add :
  ∀ (x y : ⨂[R] (i : Fin n), M)
    (hx :
      (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] x)) =
        x)
    (hy :
      (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
            ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] y)) =
        y),
    (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
        ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
          ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R]
            (x + y))) =
      x + y
⊢ (cast R M ⋯ : (a : ⨂[R]^(0 + n) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^0 M ⊗[R] ⨂[R]^n M) → ⨂[R]^(0 + n) M)
        ((tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0 ⊗ₜ[R] a)) =
    a

Tactic:
induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [TensorProduct.tmul_smul, map_smul, 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]

Premises used: TensorProduct.tmul_smul, Fin.elim0_append, map_add, TensorPower.tprod_mul_tprod, Fin.ext, congr_arg, TensorPower.gMul_def, TensorPower.cast_tprod, TensorProduct.tmul_add, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
a : ⨂[R]^n M
rw :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (a ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    a
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ _ 0 a
        (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _)) =
    a

Tactic:
rw [gMul_def, gOne_def]

Premises used: TensorPower.gMul_def, TensorPower.gOne_def
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
smul_tprod :
  HSMul.hSMul (β := ⨂[R]^n M) r
      ((tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M)
          (Fin.append a Fin.elim0 ∘ Fin.cast ⋯) :
        ⨂[R] (i : Fin n), M) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
            ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a :
              ⨂[R] (i : Fin n), M) ⊗ₜ[R]
          (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)

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

Premises used: TensorPower.tprod_mul_tprod, TensorPower.gMul_def, TensorProduct.smul_tmul', TensorPower.cast_tprod, map_smul
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
r : R
a : (i : Fin n) → M
⊢ HSMul.hSMul (β := ⨂[R]^n M) r
      ((tprod R (s := fun (a : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M)
          (Fin.append a Fin.elim0 ∘ Fin.cast ⋯) :
        ⨂[R] (i : Fin n), M) =
    HSMul.hSMul (β := ⨂[R] (i : Fin n), M) r
      ((tprod R (s := fun (x : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) a : ⨂[R] (i : Fin n), M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorPower.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (x ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    x
hy :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    y
add :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        (HAdd.hAdd (α := ⨂[R]^n M ⊗[R] ⨂[R]^0 M)
          (x ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)
          (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0))) =
    x + y
add₁ :
  (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      (HAdd.hAdd (α := ⨂[R]^(n + 0) M) (β := ⨂[R]^(n + 0) M)
        ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (x ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0) :
          ⨂[R]^(n + 0) M)
        ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0) :
          ⨂[R]^(n + 0) M)) =
    x + y
add₂ :
  HAdd.hAdd (α := ⨂[R]^n M) (β := ⨂[R]^n M)
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (x ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) :
        ⨂[R]^n M)
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) :
        ⨂[R]^n M) =
    x + y
add₃ :
  HAdd.hAdd (β := ⨂[R]^n M) x
      ((cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
          ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
            (y ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) :
        ⨂[R]^n M) =
    x + y
add₄ add₅ : x + y = x + y
⊢ (cast R M ⋯ : (a : ⨂[R]^(n + 0) M) → ⨂[R]^n M)
      ((mulEquiv : (a : ⨂[R]^n M ⊗[R] ⨂[R]^0 M) → ⨂[R]^(n + 0) M)
        ((x + y) ⊗ₜ[R] (tprod R (s := fun (i : Fin 0) ↦ M) : (a : (i : Fin 0) → M) → ⨂[R] (i : Fin 0), M) Fin.elim0)) =
    x + y

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

Premises used: map_add, TensorProduct.add_tmul