awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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) =
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
Tactic: rw [φ₁.map_add, φ₂.map_add, hx, hy]
-- 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)
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)
rw₁ :
  HAdd.hAdd (α := E) (β := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : 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) =
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
Tactic: rw [φ₁.map_add, φ₂.map_add, hx, hy]
-- 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)
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)
rw₁ :
  HAdd.hAdd (α := E) (β := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
rw₂ :
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : 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) =
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
Tactic: rw [φ₁.map_add, φ₂.map_add, hx, hy]
-- 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))
⊢ ∀ (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)
have refine : ∀ (z : ⨂[R] (i : ι), s i) (r : R) (f : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
Tactic: refine fun z ↦
    PiTensorProduct.induction_on' z ?_ fun {x y} hx hy ↦ by rw [φ₁.map_add, φ₂.map_add, hx, hy]
-- 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 : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
have rw : HSMul.hSMul (β := E) r
    ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E) =
  HSMul.hSMul (β := E) r
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
Tactic: rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]
-- 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 : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ HSMul.hSMul (β := E) r
      ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E) =
    HSMul.hSMul (β := E) r
      ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E)
have h : Eq.{u_9 + 1} (α := E)
  ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
    E)
  ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
    E)
Tactic: apply congr_arg
-- 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
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z, f)) 0
have simp_rw : HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E) = 0
Tactic: simp_rw [map_coord_zero φ i hf, smul_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
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
simp_rw simp_rw₁ : HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E) = 0
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z, f)) 0
have simp_rw₂ : HSMul.hSMul (β := E) z 0 = 0
Tactic: simp_rw [map_coord_zero φ i hf, smul_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
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (0, f)) 0
have simp_rw : HSMul.hSMul.{u_4, u_9, u_9} (α := R) (β := E) 0 ((φ : (a : (i : ι) → s i) → E) f : E) = 0
Tactic: simp_rw [zero_smul]
-- 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
φ : MultilinearMap R s E
inst_8 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ HAdd.hAdd (α := E)
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₁))
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₂)) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
      (z, update (β := s) f i (m₁ + m₂))
have simp_rw : HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₁) : E) +
    HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₂) : E) =
  HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i (m₁ + m₂)) : E)
Tactic: simp_rw [← smul_add, φ.map_update_add]
-- 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
φ : MultilinearMap R s E
inst_8 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
simp_rw simp_rw₁ :
  HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₁) : E) +
      HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₂) : E) =
    HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i (m₁ + m₂)) : E)
⊢ HAdd.hAdd (α := E)
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₁))
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₂)) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
      (z, update (β := s) f i (m₁ + m₂))
have simp_rw₂ : z •
    HAdd.hAdd (α := E) (β := E) ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₁) : E)
      ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₂) : E) =
  HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i (m₁ + m₂)) : E)
Tactic: simp_rw [← smul_add, φ.map_update_add]
-- 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
φ : MultilinearMap R s E
z₁ z₂ : R
f : (i : ι) → s i
⊢ HAdd.hAdd (α := E)
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁, f))
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₂, f)) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁ + z₂, f)
have rw : HSMul.hSMul (β := E) ((z₁, f).1 + (z₂, f).1) ((φ : (a : (i : ι) → s i) → E) (z₁, f).2 : E) =
  (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁ + z₂, f)
Tactic: rw [← add_smul]
-- 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
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)
have simp : Eq.{u_9 + 1} (α := E)
  ((AddCon.lift (addConGen (Eqv R s))
          ((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
            fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
          sorry :
        (a : ⨂[R] (i : ι), s i) → E)
      (↑(FreeAddMonoid.of (1, f)) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) :
    E)
  ((φ : (a : (i : ι) → s i) → E) f : E)
Tactic: simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk']
-- 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
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((AddCon.lift (addConGen (Eqv R s))
            ((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
              fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
            ⋯ :
          (a : ⨂[R] (i : ι), s i) → E)
        (↑(FreeAddMonoid.of (1, f)) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)
have conv_lhs : Eq.{u_9 + 1} (α := E)
  (((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
          fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E) :
        (a : FreeAddMonoid (R × ((i : ι) → s i))) → E)
      (FreeAddMonoid.of (1, f)) :
    E)
  ((φ : (a : (i : ι) → s i) → E) f : E)
Tactic: conv_lhs => apply AddCon.lift_coe
-- 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
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E)
have refine_1 : ∀ (r_1 : R) (f : (i : ι) → s i),
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) r_1 f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r_1 f) : E)
Tactic: refine PiTensorProduct.induction_on' 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
refine_1 :
  ∀ (r_1 : R) (f : (i : ι) → s i),
    (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
        (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) r_1 f)) =
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r_1 f) : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E)
have refine_2 : ∀ (x y : ⨂[R] (i : ι), s i),
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E) →
    (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) =
        HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) →
      (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • (x + y)) =
        HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)
Tactic: refine PiTensorProduct.induction_on' 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
have refine_1 : (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) (r • z) f) =
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
Tactic: rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
-- 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
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
refine_1 :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) (r • z) f) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
have refine_1₁ : HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
Tactic: rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
-- 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
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
refine_1 :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) (r • z) f) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
refine_1₁ :
  HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
have refine_1₂ : HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
  r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)
Tactic: rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
-- 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
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
refine_1 :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) (r • z) f) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
refine_1₁ :
  HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
refine_1₂ :
  HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
    r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
have refine_1₃ : r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E) =
  r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)
Tactic: rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
-- 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
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E)
ihy :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • (z + y)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
have refine_2 : (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z + r • y) =
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
Tactic: rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]