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
φ : 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)
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)
⊢ (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₁ : HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) : E)
    ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
  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]
-- 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)
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)
refine_2₁ :
  HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) : E)
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + 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₂ : HAdd.hAdd (β := E) (HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E))
    ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
  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]
-- 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)
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)
refine_2₁ :
  HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) : E)
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₂ :
  HAdd.hAdd (β := E) (HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E))
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + 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₃ : HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
  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]
-- 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)
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)
refine_2₁ :
  HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) : E)
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₂ :
  HAdd.hAdd (β := E) (HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E))
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₃ :
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + 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₄ : HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
  r •
    HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E)
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E)
Tactic: rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]
-- 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)
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)
refine_2₁ :
  HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • z) : E)
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₂ :
  HAdd.hAdd (β := E) (HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E))
      ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₃ :
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (z + y) : E)
refine_2₄ :
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    r •
      HAdd.hAdd (α := E) (β := E) ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E)
        ((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₅ : HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
  HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) z : E) +
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E)
Tactic: rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_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
⊢ (let __src := liftAux (s := s) (φ₁ + φ₂);
    { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    HAdd.hAdd (α := (⨂[R] (i : ι), s i) →ₗ[R] E)
      (let __src := liftAux (s := s) φ₁;
      { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ :
        (⨂[R] (i : ι), s i) →ₗ[R] E })
      (let __src := liftAux (s := s) φ₂;
      { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ :
        (⨂[R] (i : ι), s i) →ₗ[R] E })
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            (let __src := liftAux (s := s) (φ₁ + φ₂);
            { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry })
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    (((HAdd.hAdd (α := (⨂[R] (i : ι), s i) →ₗ[R] E)
                (let __src := liftAux (s := s) φ₁;
                { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry :
                  (⨂[R] (i : ι), s i) →ₗ[R] E })
                (let __src := liftAux (s := s) φ₂;
                { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry :
                  (⨂[R] (i : ι), s i) →ₗ[R] E })).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
Tactic: ext
-- 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
r : R
φ₂ : MultilinearMap R s E
⊢ (let __src := liftAux (s := s) (r • φ₂);
    { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ }) =
    HSMul.hSMul (α := R) (β := (⨂[R] (i : ι), s i) →ₗ[R] E) ((RingHom.id R : (a : R) → R) r : R)
      (let __src := liftAux (s := s) φ₂;
      { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ :
        (⨂[R] (i : ι), s i) →ₗ[R] E })
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            (let __src := liftAux (s := s) (r • φ₂);
            { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry })
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    (((HSMul.hSMul (α := R) (β := (⨂[R] (i : ι), s i) →ₗ[R] E) ((RingHom.id R : (a : R) → R) r : R)
                (let __src := liftAux (s := s) φ₂;
                { toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry :
                  (⨂[R] (i : ι), s i) →ₗ[R] E })).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
Tactic: ext
-- 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
⊢ (fun (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) ↦ φ'.compMultilinearMap (M₁ := s) (tprod R (s := s)))
      ((fun (φ : MultilinearMap R s E) ↦
          let __src := liftAux (s := s) φ;
          ({ toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ } :
            (⨂[R] (i : ι), s i) →ₗ[R] E))
        φ) =
    φ
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    (((fun (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) ↦ φ'.compMultilinearMap (M₁ := s) (tprod R (s := s)))
            ((fun (φ : MultilinearMap R s E) ↦
                let __src := liftAux (s := s) φ;
                ({ toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry } :
                  (⨂[R] (i : ι), s i) →ₗ[R] E))
              φ) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    ((φ : (a : (i : ι) → s i) → E) x : E)
Tactic: ext
-- 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
φ : (⨂[R] (i : ι), s i) →ₗ[R] E
⊢ (fun (φ : MultilinearMap R s E) ↦
        let __src := liftAux (s := s) φ;
        ({ toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := ⋯, map_smul' := ⋯ } :
          (⨂[R] (i : ι), s i) →ₗ[R] E))
      ((fun (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) ↦ φ'.compMultilinearMap (M₁ := s) (tprod R (s := s))) φ) =
    φ
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((fun (φ : MultilinearMap R s E) ↦
                let __src := liftAux (s := s) φ;
                ({ toFun := (↑__src : ZeroHom (⨂[R] (i : ι), s i) E).toFun, map_add' := sorry, map_smul' := sorry } :
                  (⨂[R] (i : ι), s i) →ₗ[R] E))
              ((fun (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) ↦ φ'.compMultilinearMap (M₁ := s) (tprod R (s := s))) φ))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    ((φ.compMultilinearMap (M₁ := s) (tprod R (s := s)) : (a : (i : ι) → s i) → E) x : E)
Tactic: 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ (map (s := s) (t := t) f).range =
    Submodule.span R
      {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1}
have rw : Eq (α := Submodule R (⨂[R] (i : ι), t i))
  (Submodule.span R
    (Set.range (ι := (i : ι) → s i)
      (comp (β := ⨂[R] (i : ι), s i) (⇑(map (s := s) (t := t) f) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
        (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i))))
  (Submodule.span R
    {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1})
Tactic: rw [← Submodule.map_top, ← span_tprod_eq_top, Submodule.map_span, ← Set.range_comp]
-- 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ Eq (α := Submodule R (⨂[R] (i : ι), t i))
    (Submodule.span R
      (Set.range (ι := (i : ι) → s i)
        (comp (β := ⨂[R] (i : ι), s i) (⇑(map (s := s) (t := t) f) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
          (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i))))
    (Submodule.span R
      {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1})
have h : Eq (α := Set (⨂[R] (i : ι), t i))
  (Set.range (ι := (i : ι) → s i)
    (comp (β := ⨂[R] (i : ι), s i) (⇑(map (s := s) (t := t) f) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
      (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)))
  {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1}
Tactic: apply congrArg
-- 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ Eq (α := Set (⨂[R] (i : ι), t i))
    (Set.range (ι := (i : ι) → s i)
      (comp (β := ⨂[R] (i : ι), s i) (⇑(map (s := s) (t := t) f) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
        (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)))
    {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1}
have h : ∀ (x : ⨂[R] (i : ι), t i),
  Membership.mem (γ := Set (⨂[R] (i : ι), t i))
      (Set.range (ι := (i : ι) → s i)
        (comp (β := ⨂[R] (i : ι), s i) (⇑(map (s := s) (t := t) f) : (a : ⨂[R] (i : ι), s i) → ⨂[R] (i : ι), t i)
          (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)))
      x ↔
    Membership.mem (γ := Set (⨂[R] (i : ι), t i))
      {t_1 : ⨂[R] (i : ι), t i | ∃ (m : (i : ι) → s i), (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (m i)) = t_1} x
Tactic: ext 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)
t : ι → Type u_11
t' : ι → Type u_12
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_5 : (i : ι) → AddCommMonoid (t' i)
inst_6 : (i : ι) → Module.{u_4, u_12} R (t' i)
g : (i : ι) → LinearMap.{u_4, u_4, u_11, u_12} (RingHom.id R) (t i) (t' i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ (map (s := s) (t := t') fun (i : ι) ↦ g i ∘ₗ f i) = map (s := t) (t := t') g ∘ₗ map (s := s) (t := t) f
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), t' i)
    ((LinearMap.compMultilinearMap (M₁ := s) (map (s := s) (t := t') fun (i : ι) ↦ g i ∘ₗ f i) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t' i)
        x :
      ⨂[R] (i : ι), t' i)
    (((map (s := t) (t := t') g ∘ₗ map (s := s) (t := t) f).compMultilinearMap (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), t' i)
        x :
      ⨂[R] (i : ι), t' i)
Tactic: 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
t : ι → Type u_11
inst_5 : (i : ι) → AddCommMonoid (t i)
inst_6 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
h : MultilinearMap R t E
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] E)
    ((lift (s := t) : (a : MultilinearMap R t E) → (⨂[R] (i : ι), t i) →ₗ[R] E) h ∘ₗ map (s := s) (t := t) f)
    ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E)
      (h.compLinearMap (M₁ := s) (M₁' := t) f))
have H : ∀ (x : (i : ι) → s i),
  Eq.{u_9 + 1} (α := E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((lift (s := t) : (a : MultilinearMap R t E) → (⨂[R] (i : ι), t i) →ₗ[R] E) h ∘ₗ map (s := s) (t := t) f)
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    ((LinearMap.compMultilinearMap (M₁ := s)
            ((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E)
              (h.compLinearMap (M₁ := s) (M₁' := t) f))
            (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)
Tactic: 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)
⊢ Eq (α := (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i) (map (s := s) (t := s) fun (i : ι) ↦ LinearMap.id) LinearMap.id
have H : ∀ (x : (i : ι) → s i),
  Eq (α := ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) (map (s := s) (t := s) fun (i : ι) ↦ LinearMap.id) (tprod R (s := s)) :
          (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        x :
      ⨂[R] (i : ι), s i)
    ((LinearMap.compMultilinearMap (M₁ := s) LinearMap.id (tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
        x :
      ⨂[R] (i : ι), s i)
Tactic: 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)
t : ι → Type u_11
inst_3 : (i : ι) → AddCommMonoid (t i)
inst_4 : (i : ι) → Module.{u_4, u_11} R (t i)
f : (i : ι) → LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
inst_5 : DecidableEq ι
i : ι
x : (i : ι) → s i
u : LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s i) (t i)
⊢ Eq (α := (j : ι) → t j)
    (fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j : (a : s j) → t j)
        (x j))
    (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)))
have h : ∀ (j : ι),
  Eq.{u_11 + 1} (α := t j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u_4, u_4, u_7, u_11} (RingHom.id R) (s a) (t a)) f i u j : (a : s j) → t j)
        (x j) :
      t j)
    (update (β := t) (fun (j : ι) ↦ (f j : (a : s j) → t j) (x j)) i ((u : (a : s i) → t i) (x i)) j : t j)
Tactic: ext j