awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
refine_2₅ 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)
⊢ (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)

Tactic:
rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]

Premises used: PiTensorProduct.liftAux, AddMonoidHom.map_add, smul_add
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ })
              (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' := ⋯, 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 })).compMultilinearMap
              (M₁ := s) (tprod R (s := s)) :
            (a : (i : ι) → s i) → E)
          x :
        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 })

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ })
            (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' := ⋯, 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 })).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)

Tactic:
simp [liftAux_tprod]

Premises used: PiTensorProduct.liftAux_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ })
              (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' := ⋯, map_smul' := ⋯ :
                    (⨂[R] (i : ι), s i) →ₗ[R] E })).compMultilinearMap
              (M₁ := s) (tprod R (s := s)) :
            (a : (i : ι) → s i) → E)
          x :
        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 })

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ })
            (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' := ⋯, map_smul' := ⋯ :
                  (⨂[R] (i : ι), s i) →ₗ[R] E })).compMultilinearMap
            (M₁ := s) (tprod R (s := s)) :
          (a : (i : ι) → s i) → E)
        x :
      E)

Tactic:
simp [liftAux_tprod]

Premises used: PiTensorProduct.liftAux_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ } :
                    (⨂[R] (i : ι), s i) →ₗ[R] E))
                φ) :
            (a : (i : ι) → s i) → E)
          x :
        E)
      ((φ : (a : (i : ι) → s i) → E) x : 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))
        φ) =
    φ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ } :
                  (⨂[R] (i : ι), s i) →ₗ[R] E))
              φ) :
          (a : (i : ι) → s i) → E)
        x :
      E)
    ((φ : (a : (i : ι) → s i) → E) x : E)

Tactic:
simp [liftAux_tprod, LinearMap.compMultilinearMap]

Premises used: PiTensorProduct.liftAux_tprod, LinearMap.compMultilinearMap
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ } :
                    (⨂[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)
⊢ (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))) φ) =
    φ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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' := ⋯, map_smul' := ⋯ } :
                  (⨂[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:
simp [liftAux_tprod]

Premises used: PiTensorProduct.liftAux_tprod
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
    ((((lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E) φ : (⨂[R] (i : ι), s i) →ₗ[R] E) :
          (a : ⨂[R] (i : ι), s i) → E)
        ((PiTensorProduct.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)

Tactic:
liftAux_tprod φ f

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, PiTensorProduct.liftAux_tprod, FreeAddMonoid.sumAux
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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] (i : ι), s i) →ₗ[R] E
H : φ'.compMultilinearMap (M₁ := s) (PiTensorProduct.tprod R (s := s)) = φ
⊢ φ' = (lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E) φ

Tactic:
ext <| H.symm ▸ (lift.symm_apply_apply φ).symm

Premises used: Eq.rec, LinearEquiv.symm_apply_apply, Eq.symm, PiTensorProduct.lift, PiTensorProduct.ext
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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] (i : ι), s i) →ₗ[R] E
H :
  ∀ (f : (i : ι) → s i),
    Eq.{u_9 + 1} (α := E)
      ((φ' : (a : ⨂[R] (i : ι), s i) → E)
          ((PiTensorProduct.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)
⊢ φ' = (lift (s := s) : (a : MultilinearMap R s E) → (⨂[R] (i : ι), s i) →ₗ[R] E) φ

Tactic:
lift.unique' (MultilinearMap.ext H)

Premises used: MultilinearMap.ext, PiTensorProduct.lift.unique'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
⊢ (LinearEquiv.symm (lift (s := s)) : (a : (⨂[R] (i : ι), s i) →ₗ[R] E) → MultilinearMap R s E) φ' =
    φ'.compMultilinearMap (M₁ := s) (tprod R (s := s))

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
    ((lift (s := s) : (a : MultilinearMap R s (⨂[R] (i : ι), s i)) → (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)
        (tprod R (s := s)) :
      (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)
    (LinearMap.id : (⨂[R] (i : ι), s i) →ₗ[R] ⨂[R] (i : ι), s i)

Tactic:
Eq.symm <| lift.unique' rfl

Premises used: PiTensorProduct.lift.unique', Eq.symm, rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
x : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), t 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) :
      ⨂[R] (i : ι), t i)
    (⨂ₜ[R] (i : ι), (f i : (a : s i) → t i) (x i) : ⨂[R] (i : ι), t i)

Tactic:
lift.tprod _

Premises used: PiTensorProduct.lift.tprod, PiTensorProduct.tprodCoeff, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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})
⊢ (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}

Tactic:
rw [← Submodule.map_top, ← span_tprod_eq_top, Submodule.map_span, ← Set.range_comp]

Premises used: Set.range_comp, Submodule.map_top, Submodule.map_span, PiTensorProduct.span_tprod_eq_top
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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}
⊢ 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:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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
⊢ 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:
ext x
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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:
simp only [Set.mem_range, comp_apply, map_tprod, Set.mem_setOf_eq]

Premises used: Set.mem_range, Set.mem_setOf_eq, PiTensorProduct.map_tprod, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
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)
⊢ (map (s := s) (t := t') fun (i : ι) ↦ g i ∘ₗ f i) = map (s := t) (t := t') g ∘ₗ map (s := s) (t := t) f

Tactic:
ext