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
ιι : Type u_3
ι : ιι → Type u_4
ai : ιι
a : ⨂[R] (x : ι ai), M
bi : ιι
b : ⨂[R] (x : ι bi), M
hi : ai = bi
h : (reindex R (fun (x : ι ai) ↦ M) (Equiv.cast ⋯) : (a : ⨂[R] (i : ι ai), M) → ⨂[R] (i : ι bi), M) a = b
⊢ Eq (α := GradedMonoid fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai a)
    (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) bi b)
have subst : ∀ (b : ⨂[R] (x : ι ai), M)
  (h : (reindex R (fun (x : ι ai) ↦ M) (Equiv.cast sorry) : (a : ⨂[R] (i : ι ai), M) → ⨂[R] (i : ι ai), M) a = b),
  Eq (α := GradedMonoid fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai a)
    (Sigma.mk (β := fun (ii : ιι) ↦ ⨂[R] (x : ι ii), M) ai b)
Tactic: subst hi
Cleared hypotheses: bi, b, hi, h
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (cast R M h : (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M) (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
⊢ a = b
have refine : (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (Equiv.cast sorry) :
      (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
    (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
  b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
Tactic: refine gradedMonoid_eq_of_reindex_cast h ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Basic (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (cast R M h : (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M) (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
⊢ (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (Equiv.cast ⋯) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
have h2₁ : (reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
      (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
    (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
  b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
Tactic: rw [cast] at h2
Cleared hypotheses: h2
-- 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
a b : GradedMonoid fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M
h : a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M) = b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
h2 :
  (reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
        (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
      (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) =
    b.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)
rw :
  (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (finCongr h) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
rw₁ : a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M) = b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
⊢ (reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (Equiv.cast ⋯) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) =
    b.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)
have rw₂ : Eq (α := ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
  ((reindex R (fun (x : Fin (a.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))) ↦ M) (finCongr h) :
        (a : ⨂[R] (i : Fin a.fst), M) → ⨂[R] (i : Fin b.fst), M)
      (a.snd (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M)) :
    ⨂[R] (i : Fin (b.fst (β := fun (ii : ℕ) ↦ ⨂[R] (x : Fin ii), M))), M)
  ((reindex R (fun (x : Fin (a.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M))) ↦ M) (finCongr h) :
        (a : ⨂[R]^a.fst M) → ⨂[R]^b.fst M)
      (a.snd (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) :
    ⨂[R]^(b.fst (β := fun (n : ℕ) ↦ ⨂[R] (x : Fin n), M)) M)
Tactic: rw [← finCongr_eq_equivCast, ← h2]
-- 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
i j : ℕ
h : i = j
⊢ Eq (α := (a : ⨂[R]^i M) → ⨂[R]^j M) ((⇑(cast R M h) : (a : ⨂[R]^i M) → ⨂[R]^j M) : (a : ⨂[R]^i M) → ⨂[R]^j M)
    (_root_.cast ⋯ : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) j)
have subst : Eq (α := (a : ⨂[R]^i M) → ⨂[R]^i M) ((⇑(cast R M sorry) : (a : ⨂[R]^i M) → ⨂[R]^i M) : (a : ⨂[R]^i M) → ⨂[R]^i M)
  (_root_.cast sorry : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)
Tactic: subst h
Cleared hypotheses: j, h
-- 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
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)
have 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 sorry : (a : (fun (i : ℕ) ↦ ⨂[R]^i M) i) → (fun (i : ℕ) ↦ ⨂[R]^i M) i)
Tactic: rw [cast_refl]
-- 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
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)
        ((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)
have 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))
Tactic: rw [tmulEquiv_apply R M a b]
-- 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
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))
have 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)
Tactic: refine (reindex_tprod _ _).trans ?_
-- 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
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ 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)
have 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
Tactic: congr 1
-- 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
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ (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
have 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)
Tactic: dsimp only [Fin.append, finSumFinEquiv, Equiv.coe_fn_symm_mk]
-- 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
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ 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)
have 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
Tactic: apply funext
-- 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
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (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
have 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)
Tactic: apply Fin.addCases
-- 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
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)
⊢ ∀ (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
have 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)
Tactic: apply Fin.addCases
-- 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)
      (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ⨂[R]^i M) instAddNat _ 0 _
        (@GradedMonoid.GOne.one _ (fun (i : ℕ) ↦ ⨂[R]^i M) MulZeroClass.toZero _) a) =
    a
have rw : (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] a)) =
  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]^(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)
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 Fin.elim0 a ∘ 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.tmul_smul, map_smul, map_smul, ← gMul_def, tprod_mul_tprod, 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 : ℕ
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 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)
have smul_tprod : ∀ (i : Fin n), (Fin.append Fin.elim0 a ∘ Fin.cast sorry) i = a i
Tactic: congr 2 with i
-- 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
i : Fin n
⊢ (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) i = a i
have smul_tprod : ((a ∘ Fin.cast sorry) ∘ Fin.cast sorry) i = a i
Tactic: rw [Fin.elim0_append]
-- 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
i : Fin n
⊢ ((a ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) i = a i
have smul_tprod : (↑(Fin.cast sorry (Fin.cast sorry i)) : ℕ) = (↑i : ℕ)
Tactic: refine congr_arg a (Fin.ext ?_)
-- 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
⊢ (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 : (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)
      (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
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 : ℕ
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
⊢ (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₁ : (cast R M sorry : (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
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 : ℕ
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
⊢ (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₂ : HAdd.hAdd (α := ⨂[R]^n M) (β := ⨂[R]^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] x)) :
      ⨂[R]^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] y)) :
      ⨂[R]^n M) =
  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 : ℕ
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
⊢ (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₃ : HAdd.hAdd (β := ⨂[R]^n M) x
    ((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)) :
      ⨂[R]^n M) =
  x + y
Tactic: rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]