awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
simp_rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (HSMul.hSMul.{u_5, u_4, u_4} (α := R₁) 0 r) f) 0
⊢ HSMul.hSMul (α := R₁) (β := ⨂[R] (i : ι), s i) 0 (tprodCoeff R (s := s) r f) = 0
have simp_rw₁ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 0 f) 0
Tactic: simp_rw [smul_tprodCoeff', zero_smul, zero_tprodCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x_1 x y : ⨂[R] (i : ι), s i
ihx : HSMul.hSMul (α := R₁) 0 x = 0
ihy : HSMul.hSMul (α := R₁) 0 y = 0
⊢ HSMul.hSMul (α := R₁) 0 (x + y) = 0
have simp_rw : HSMul.hSMul (α := R₁) 0 x + HSMul.hSMul (α := R₁) 0 y = 0
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x_1 x y : ⨂[R] (i : ι), s i
ihx : HSMul.hSMul (α := R₁) 0 x = 0
ihy : HSMul.hSMul (α := R₁) 0 y = 0
simp_rw : HSMul.hSMul (α := R₁) 0 x + HSMul.hSMul (α := R₁) 0 y = 0
⊢ HSMul.hSMul (α := R₁) 0 (x + y) = 0
have simp_rw₁ : 0 + HSMul.hSMul (α := R₁) 0 y = 0
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x_1 x y : ⨂[R] (i : ι), s i
ihx : HSMul.hSMul (α := R₁) 0 x = 0
ihy : HSMul.hSMul (α := R₁) 0 y = 0
simp_rw : HSMul.hSMul (α := R₁) 0 x + HSMul.hSMul (α := R₁) 0 y = 0
simp_rw₁ : 0 + HSMul.hSMul (α := R₁) 0 y = 0
⊢ HSMul.hSMul (α := R₁) 0 (x + y) = 0
have simp_rw₂ : HAdd.hAdd (α := ⨂[R] (i : ι), s i) 0 0 = 0
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
x_1 : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) 1 (update (β := s) f i x))
have rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
  (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1) (update (β := s) f i x))
Tactic: rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
x_1 : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1) (update (β := s) f i x))
⊢ tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) 1 (update (β := s) f i x))
have rw₁ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
  (tprodCoeff R (s := s) 1 (update (β := s) (update (β := s) f i x) i (r • update (β := s) f i x i)))
Tactic: rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
x_1 : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1) (update (β := s) f i x))
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) (update (β := s) f i x) i (r • update (β := s) f i x i)))
⊢ tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) 1 (update (β := s) f i x))
have rw₂ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
  (tprodCoeff R (s := s) 1 (update (β := s) f i (r • update (β := s) f i x i)))
Tactic: rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
x_1 : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1) (update (β := s) f i x))
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) (update (β := s) f i x) i (r • update (β := s) f i x i)))
rw₂ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) f i (r • update (β := s) f i x i)))
⊢ tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) 1 (update (β := s) f i x))
have rw₃ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
  (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
Tactic: rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
z : R
f : (i : ι) → s i
⊢ tprodCoeff R (s := s) z f =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
have this : z = HSMul.hSMul (β := R) z 1
Tactic: have : z = z • (1 : R) := by simp only [mul_one, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
z : R
f : (i : ι) → s i
this : z = HSMul.hSMul (β := R) z 1
| tprodCoeff R (s := s) z f
have rw : tprodCoeff R (s := s) (HSMul.hSMul (β := R) z 1) f
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
z : R
f : (i : ι) → s i
this : z = HSMul.hSMul (β := R) z 1
⊢ tprodCoeff R (s := s) z f =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
have conv_lhs : tprodCoeff R (s := s) (HSMul.hSMul (β := R) z 1) f =
  HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
    ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
b : R × ((i : ι) → s i)
a : FreeAddMonoid (R × ((i : ι) → s i))
ih :
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑a : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) a)))
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          (FreeAddMonoid.of b + a))))
have add_of : (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient) =
  HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) b.1 fun (i : ι) ↦ b.2 i)
    (↑a : (addConGen (Eqv R s)).Quotient)
Tactic: rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))
have zero : Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑0 : (addConGen (Eqv R s)).Quotient)
  (List.sum
    (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
Tactic: induction p using FreeAddMonoid.inductionOn' with
  | zero => rfl
  | add_of b a ih =>
    rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]
    rfl
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
zero :
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑0 : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))
have add_of : ∀ (b : R × ((i : ι) → s i)) (a : FreeAddMonoid (R × ((i : ι) → s i)))
  (ih :
    Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑a : (addConGen (Eqv R s)).Quotient)
      (List.sum
        (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) a)))),
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          (FreeAddMonoid.of b + a))))
Tactic: induction p using FreeAddMonoid.inductionOn' with
  | zero => rfl
  | add_of b a ih =>
    rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]
    rfl
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
x : ⨂[R] (i : ι), s i
⊢ x.lifts (s := s).Nonempty
have existsi : Quot.out (r :=
    (⇑(addConGen (Eqv R fun (i : ι) ↦ s i)).toSetoid :
      FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) →
        FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) → Prop))
    x ∈
  x.lifts (s := s)
Tactic: existsi Quot.out x
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
⊢ Membership.mem (γ := Set (FreeAddMonoid (R × ((i : ι) → s i)))) (lifts (s := s) 0) 0
have rw : Eq (α := ⨂[R] (i : ι), s i)
  (List.sum
    (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
  0
Tactic: rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
rw :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
    0
⊢ Membership.mem (γ := Set (FreeAddMonoid (R × ((i : ι) → s i)))) (lifts (s := s) 0) 0
have rw₁ : Eq (α := ⨂[R] (i : ι), s i)
  (List.sum
    (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i)) []))
  0
Tactic: rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
rw :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
    0
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i)) []))
    0
⊢ Membership.mem (γ := Set (FreeAddMonoid (R × ((i : ι) → s i)))) (lifts (s := s) 0) 0
have rw₂ : Eq (α := ⨂[R] (i : ι), s i) (List.sum []) 0
Tactic: rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
rw :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
    0
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i)) []))
    0
rw₂ : Eq (α := ⨂[R] (i : ι), s i) (List.sum []) 0
⊢ Membership.mem (γ := Set (FreeAddMonoid (R × ((i : ι) → s i)))) (lifts (s := s) 0) 0
have rw₃ : Eq (α := ⨂[R] (i : ι), s i) 0 0
Tactic: rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts (s := s)
hq : q ∈ y.lifts (s := s)
⊢ HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
      (↑q : (addConGen (Eqv R s)).Quotient) =
    x + y
have rw : x + (↑q : (addConGen (Eqv R s)).Quotient) = x + y
Tactic: rw [hp, hq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts (s := s)
hq : q ∈ y.lifts (s := s)
rw : x + (↑q : (addConGen (Eqv R s)).Quotient) = x + y
⊢ HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
      (↑q : (addConGen (Eqv R s)).Quotient) =
    x + y
have rw₁ : x + y = x + y
Tactic: rw [hp, hq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h :
  List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)) =
    x
a : R
⊢ List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          ((FreeAddMonoid.map fun (y : R × ((i : ι) → s i)) ↦ (a * y.1, y.2) :
              (a : FreeAddMonoid (R × ((i : ι) → s i))) → FreeAddMonoid (R × ((i : ι) → s i)))
            p))) =
    a • x
have rw : List.sum
    (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
      ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
        ((FreeAddMonoid.map fun (y : R × ((i : ι) → s i)) ↦ (a * y.1, y.2) :
            (a : FreeAddMonoid (R × ((i : ι) → s i))) → FreeAddMonoid (R × ((i : ι) → s i)))
          p))) =
  HSMul.hSMul (β := ⨂[R] (i : ι), s i) a
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
smul_tprod :
  ∀ (r : R) (f : (i : ι) → s i),
    motive
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i))
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z
have smul_tprod₁ : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R (s := s) r f)
Tactic: simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod
Cleared hypotheses: smul_tprod
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
⊢ φ₁ = φ₂
have refine : ∀ (x : ⨂[R] (i : ι), s i),
  Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E)
Tactic: refine LinearMap.ext ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z x y : ⨂[R] (i : ι), s i
hx : Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E)
hy : Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
⊢ Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)
have rw : HAdd.hAdd (α := E) (β := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
  (φ₂ : (a : ⨂[R] (i : ι), s i) → E) (x + y)
Tactic: rw [φ₁.map_add, φ₂.map_add, hx, hy]