awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x_1 : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) :=
  HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))
G' : Submodule 𝕜 F :=
  LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
    ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))
e : HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))) ≃ₗ[𝕜]
  ↥(LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))) :=
  LinearMap.quotKerEquivRange
    ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E
  (HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))) :=
  (LinearEquiv.symm (lift (s := E)) :
      (a :
          (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
            (⨂[𝕜] (i : ι), E i) ⧸
              ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker) →
        MultilinearMap 𝕜 E
          ((⨂[𝕜] (i : ι), E i) ⧸
            ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker))
    ((↑e.symm :
        ↥((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).range →ₗ[𝕜]
          (⨂[𝕜] (i : ι), E i) ⧸
            ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker) ∘ₗ
      LinearMap.rangeRestrict
        ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))
x : (i : ι) → E i
⊢ norm.{uF} (E := F) ((f : (a : (i : ι) → E i) → F) x : F) ≤ ‖f‖ * ∏ i : ι, ‖x i‖

Tactic:
exact f.le_opNorm x

Premises used: ContinuousMultilinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
rw :
  LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (injectiveSeminorm (E := E)) (projectiveSeminorm (E := E))

Tactic:
rw [injectiveSeminorm]

Premises used: PiTensorProduct.injectiveSeminorm
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))

Tactic:
csSup_le ?_ ?_

Premises used: csSup_le
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
refine_1 :
  Set.Nonempty (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}
refine_2 :
  ∀ (b : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)),
    Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
        {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
          ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
            p =
              Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
                (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                  Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
                (toDualContinuousMultilinearMap (E := E) G)}
        b →
      b ≤ projectiveSeminorm (E := E)
⊢ LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
              (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
                Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap (E := E) G)})
    (projectiveSeminorm (E := E))

Tactic:
refine csSup_le ?_ ?_

Premises used: csSup_le
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
refine_1 :
  Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}
    0
⊢ Set.Nonempty (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
            (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
              Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
            (toDualContinuousMultilinearMap (E := E) G)}

Tactic:
existsi 0
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
refine_1 :
  Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
    (Seminorm.comp
      (normSeminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
        Seminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
      (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
⊢ ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
    Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
      (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G))

Tactic:
existsi PUnit, inferInstance, inferInstance

Premises used: PUnit
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
refine_1 :
  ∀ (x : ⨂[𝕜] (i : ι), E i),
    Eq (α := ℝ) ((0 : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ)
      ((Seminorm.comp
              (normSeminorm 𝕜
                  (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                    PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
                Seminorm 𝕜
                  (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                    PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
              (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
            (a : ⨂[𝕜] (i : ι), E i) → ℝ)
          x :
        ℝ)
⊢ Eq (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) 0
    (Seminorm.comp
      (normSeminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}) :
        Seminorm 𝕜
          (ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
            PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))
      (toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)}))

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
refine_1 :
  0 =
    norm (E :=
      ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
        PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
      0
refine_1₁ refine_1₂ : Eq (α := ℝ) 0 0
⊢ 0 =
    norm (E :=
      ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
        PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
      ((toDualContinuousMultilinearMap (E := E) PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} :
            (a : ⨂[𝕜] (i : ι), E i) →
              ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
                PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})
          x :
        ContinuousMultilinearMap 𝕜 E PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)} →L[𝕜]
          PUnit.{max (max (uE + 1) (uι + 1)) (u𝕜 + 1)})

Tactic:
rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit.{(max (max uE uι) u𝕜) + 1} x) 0,
      norm_zero]

Premises used: norm_zero
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
hp :
  ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
    p =
      Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G)
refine_2 :
  ∀ (G : Type (max uι u𝕜 uE)) (w : SeminormedAddCommGroup G) (w_1 : NormedSpace 𝕜 G)
    (h :
      p =
        Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
          (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) :
            Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
          (toDualContinuousMultilinearMap (E := E) G)),
    p ≤ projectiveSeminorm (E := E)
⊢ p ≤ projectiveSeminorm (E := E)

Tactic:
obtain ⟨G, _, _, h⟩ := hp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w : SeminormedAddCommGroup G
w_1 : NormedSpace 𝕜 G
h :
  p =
    Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G)
refine_2 :
  LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G))
    (projectiveSeminorm (E := E))
⊢ p ≤ projectiveSeminorm (E := E)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w : SeminormedAddCommGroup G
w_1 : NormedSpace 𝕜 G
h :
  p =
    Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G)
x : ⨂[𝕜] (i : ι), E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)
      ((toDualContinuousMultilinearMap (E := E) G : (a : ⨂[𝕜] (i : ι), E i) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)
          x :
        ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) ≤
    (projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x

Tactic:
toDualContinuousMultilinearMap_le_projectiveSeminorm _

Premises used: PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
w : SeminormedAddCommGroup G
w_1 : NormedSpace 𝕜 G
h :
  p =
    Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G)
x : ⨂[𝕜] (i : ι), E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)
      ((toDualContinuousMultilinearMap (E := E) G : (a : ⨂[𝕜] (i : ι), E i) → ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)
          x :
        ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) ≤
    (projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x

Tactic:
exact toDualContinuousMultilinearMap_le_projectiveSeminorm _

Premises used: PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
⊢ LE.le (α := ℝ) ((injectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (⨂ₜ[𝕜] (i : ι), m i) : ℝ)
    (∏ i : ι, ‖m i‖ : ℝ)

Tactic:
le_trans (injectiveSeminorm_le_projectiveSeminorm _) (projectiveSeminorm_tprod_le m)

Premises used: PiTensorProduct.projectiveSeminorm_tprod_le, PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm, le_trans
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
      (MultilinearMap.mkContinuous (E := E)
        ((LinearEquiv.symm (lift (s := E)) : (a : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) → MultilinearMap 𝕜 E F)
          (↑f : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F))
        ‖f‖ ⋯) ≤
    ‖f‖

Tactic:
MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuous_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
      (MultilinearMap.mkContinuous (E := E)
        ((LinearEquiv.symm (lift (s := E)) : (a : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) → MultilinearMap 𝕜 E F)
          (↑f : (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F))
        ‖f‖ ⋯) ≤
    ‖f‖

Tactic:
exact MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuous_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
⊢ Eq.{uF + 1} (α := F)
    ((((liftIsometry 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →L[𝕜] F) f :
            (⨂[𝕜] (i : ι), E i) →L[𝕜] F) :
          (a : ⨂[𝕜] (i : ι), E i) → F)
        x :
      F)
    ((((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)) :
            (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
          (a : ⨂[𝕜] (i : ι), E i) → F)
        x :
      F)

Tactic:
simp [LinearIsometryEquiv.ofBounds, liftIsometry]

Premises used: PiTensorProduct.liftIsometry, LinearIsometryEquiv.ofBounds
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
H :
  ∀ (x : (i : ι) → E i),
    Eq (α := ⨂[𝕜] (i : ι), E i)
      ((ContinuousMultilinearMap.toMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E)) :
            (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
          x :
        ⨂[𝕜] (i : ι), E i)
      ((tprod 𝕜 (s := E) : (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i) x : ⨂[𝕜] (i : ι), E i)
⊢ Eq (α := MultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i))
    (ContinuousMultilinearMap.toMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E))) (tprod 𝕜 (s := E))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : (i : ι) → E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E i)
    ((ContinuousMultilinearMap.toMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E)) : (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)
    ((tprod 𝕜 (s := E) : (a : (i : ι) → E i) → ⨂[𝕜] (i : ι), E i) x : ⨂[𝕜] (i : ι), E i)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
⊢ (LinearIsometryEquiv.symm (liftIsometry 𝕜 E F) : (a : (⨂[𝕜] (i : ι), E i) →L[𝕜] F) → ContinuousMultilinearMap 𝕜 E F)
      l =
    l.compContinuousMultilinearMap (M₁ := E) (tprodL 𝕜 (E := E))

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
h :
  ∀ (x : ⨂[𝕜] (i : ι), E i),
    Eq (α := ⨂[𝕜] (i : ι), E i)
      ((((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i) :
                  (a : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i)) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
                (tprodL 𝕜 (E := E)) :
              (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) :
            (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i)
          x :
        ⨂[𝕜] (i : ι), E i)
      ((ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i) : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i) x :
        ⨂[𝕜] (i : ι), E i)
⊢ Eq (α := (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
    ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i) :
          (a : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i)) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
        (tprodL 𝕜 (E := E)) :
      (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
    (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i) : (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ⨂[𝕜] (i : ι), E i)
    ((((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i) :
                (a : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] (i : ι), E i)) → (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i)
              (tprodL 𝕜 (E := E)) :
            (⨂[𝕜] (i : ι), E i) →L[𝕜] ⨂[𝕜] (i : ι), E i) :
          (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i)
        x :
      ⨂[𝕜] (i : ι), E i)
    ((ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i) : (a : ⨂[𝕜] (i : ι), E i) → ⨂[𝕜] (i : ι), E i) x : ⨂[𝕜] (i : ι), E i)

Tactic:
simp