awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add₄ : x + y = x + y
Tactic: rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have smul_tprod : ∀ (r : R) (a : (i : Fin n) → M),
  (cast R M sorry : (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: 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]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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)
⊢ (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
have add : ∀ (x y : ⨂[R] (i : Fin n), M)
  (hx :
    (cast R M sorry : (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 sorry : (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 sorry : (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: 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]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have rw : (cast R M sorry : (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
Tactic: rw [gMul_def, gOne_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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)
have 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 sorry) :
      ⨂[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.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add : (cast R M sorry : (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
Tactic: rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add₁ : (cast R M sorry : (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
Tactic: rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add₂ : HAdd.hAdd (α := ⨂[R]^n M) (β := ⨂[R]^n M)
    ((cast R M sorry : (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 sorry : (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
Tactic: rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add₃ : HAdd.hAdd (β := ⨂[R]^n M) x
    ((cast R M sorry : (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
Tactic: rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have add₄ : x + y = x + y
Tactic: rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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
⊢ (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
have smul_tprod : ∀ (r : R) (a : (i : Fin n) → M),
  (cast R M sorry : (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: induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp
  | add x y hx hy =>
    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (goal)
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]^(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)
⊢ (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
have add : ∀ (x y : ⨂[R] (i : Fin n), M)
  (hx :
    (cast R M sorry : (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 sorry : (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),
  (cast R M sorry : (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: induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp
  | add x y hx hy =>
    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
Cleared hypotheses: a