awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : x = 0
⊢ normalize (normalize x) = normalize x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize (normalize x) = normalize x

Tactic:
simp [normalize_eq_self_of_norm_eq_one, hx]

Premises used: NormedSpace.normalize_eq_self_of_norm_eq_one
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ normalize (-x) = -normalize x

Tactic:
simp [normalize]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
hr : 0 < r
x : V
⊢ normalize (r • x) = normalize x

Tactic:
simp [normalize, norm_smul, smul_smul, abs_of_pos hr, hr.ne']

Premises used: norm_smul, smul_smul, LT.lt.ne', abs_of_pos, NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
hr : r < 0
x : V
linarith : -r ≤ 0 → r - 0 + (-r - 0) = 0
⊢ 0 < -r

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
hr : r < 0
x : V
⊢ normalize (r • x) = -normalize x

Tactic:
simpa using normalize_smul_of_pos (show 0 < -r by linarith) (-x)

Premises used: NormedSpace.normalize_smul_of_pos, Neg.neg
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
inl :
  ∀ (h_pos : 0 < r),
    normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
inr :
  normalize (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ) (normalize x)
inr₁ :
  ∀ (h_neg : r < 0),
    normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)

Tactic:
rcases lt_trichotomy 0 r with (h_pos | rfl | h_neg)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
h_pos : 0 < r
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)

Tactic:
simp [normalize_smul_of_pos, h_pos]

Premises used: NormedSpace.normalize_smul_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ normalize (HSMul.hSMul (α := ℝ) 0 x) =
    HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ) (normalize x)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
r : ℝ
x : V
h_neg : r < 0
⊢ normalize (r • x) = HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) r) : ℝ) (normalize x)

Tactic:
simp [normalize_smul_of_neg, h_neg]

Premises used: NormedSpace.normalize_smul_of_neg
-- 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
x : ⨂[𝕜] (i : ι), E i
x_1 : ContinuousMultilinearMap 𝕜 E F
⊢ norm.{uF} (E := F)
      (((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                  (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                x ∘ₗ
              ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E) :
            (a : ContinuousMultilinearMap 𝕜 E F) → F)
          x_1 :
        F) ≤
    HMul.hMul (α := ℝ) ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ) ‖x_1‖

Tactic:
simpa [mul_comm] using norm_eval_le_projectiveSeminorm ..

Premises used: PiTensorProduct.norm_eval_le_projectiveSeminorm, mul_comm
-- 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
x y : ⨂[𝕜] (i : ι), E i
x_1 : ContinuousMultilinearMap 𝕜 E F
⊢ Eq.{uF + 1} (α := F)
    (((LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
              ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                    (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                  (x + y) ∘ₗ
                ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
              ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (x + y)) ⋯ :
            ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    x ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    y ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) y) ⋯ :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)

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
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
h :
  ∀ (x_1 : ContinuousMultilinearMap 𝕜 E F),
    Eq.{uF + 1} (α := F)
      (((LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    (a • x) ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (a • x)) ⋯ :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
            (a : ContinuousMultilinearMap 𝕜 E F) → F)
          x_1 :
        F)
      ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
              (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                  ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                        (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                      x ∘ₗ
                    ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                  ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
                ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
            (a : ContinuousMultilinearMap 𝕜 E F) → F)
          x_1 :
        F)
⊢ LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
      ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
            (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
          (a • x) ∘ₗ
        ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
      ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (a • x)) ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
          ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
              x ∘ₗ
            ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
          ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)

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)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a : 𝕜
x : ⨂[𝕜] (i : ι), E i
x_1 : ContinuousMultilinearMap 𝕜 E F
⊢ Eq.{uF + 1} (α := F)
    (((LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
              ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                    (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                  (a • x) ∘ₗ
                ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
              ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (a • x)) ⋯ :
            ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
    ((HSMul.hSMul (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    x ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)

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
x : ⨂[𝕜] (i : ι), E i
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
        ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
              (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
            x ∘ₗ
          ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
        ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯) ≤
    (projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x

Tactic:
apply LinearMap.mkContinuous_norm_le _ (apply_nonneg _ _)

Premises used: LinearMap.mkContinuous_norm_le, NonnegHomClass.apply_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)
h :
  Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
    (upperBounds
      {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))
⊢ BddAbove (α := 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:
use projectiveSeminorm

Premises used: PiTensorProduct.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)
h :
  ∀ (x : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (x_1 : Type (max uι u𝕜 uE)) (x_2 : SeminormedAddCommGroup x_1)
    (x_3 : NormedSpace 𝕜 x_1)
    (h :
      x =
        Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1) (σ₁₂ := RingHom.id 𝕜)
          (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1) :
            Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1))
          (toDualContinuousMultilinearMap (E := E) x_1)),
    x ≤ projectiveSeminorm (E := E)
⊢ Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
    (upperBounds
      {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:
simp only [mem_upperBounds, Set.mem_setOf_eq, forall_exists_index]

Premises used: forall_exists_index, Set.mem_setOf_eq, mem_upperBounds
-- 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)
h :
  ∀ (x : SeminormedAddCommGroup G) (x_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)
⊢ ∀ (x : SeminormedAddCommGroup G) (x_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)

Tactic:
_
-- 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)
x : SeminormedAddCommGroup G
h :
  ∀ (x_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)
⊢ ∀ (x_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)

Tactic:
_
-- 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)
x_1 : SeminormedAddCommGroup G
x_2 : NormedSpace 𝕜 G
hp :
  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
⊢ LE.le (α := (fun (a : ⨂[𝕜] (i : ι), E i) ↦ ℝ) x)
    ((fun (f : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) ↦ ((⇑f : (a : ⨂[𝕜] (i : ι), E i) → ℝ) : (a : ⨂[𝕜] (i : ι), E i) → ℝ)) p
      x)
    ((fun (f : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) ↦ ((⇑f : (a : ⨂[𝕜] (i : ι), E i) → ℝ) : (a : ⨂[𝕜] (i : ι), E i) → ℝ))
      (projectiveSeminorm (E := E)) x)

Tactic:
simpa [hp] using 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)
x : ⨂[𝕜] (i : ι), E i
⊢ Eq (α := ℝ) ((injectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ)
    (⨆ (p :
        (↑{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)} :
          Type (max (max uE uι) u𝕜))),
        ((↑p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x :
      ℝ)

Tactic:
simpa only [injectiveSeminorm, Set.coe_setOf, Set.mem_setOf_eq]
    using Seminorm.sSup_apply dualSeminorms_bounded

Premises used: Set.mem_setOf_eq, PiTensorProduct.dualSeminorms_bounded, Set.coe_setOf, PiTensorProduct.injectiveSeminorm, Seminorm.sSup_apply
-- 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:
f.le_opNorm x

Premises used: ContinuousMultilinearMap.le_opNorm