awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
refine_1 :
  ∀ (f : E →SL[σ₁₂] F), (∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1) → ‖f‖ ≤ ‖c‖
⊢ (IsVonNBounded.{u_1, u_4} 𝕜 (E := E) (closedBall 0 1, closedBall 0 1).1 ∧
      Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1, closedBall 0 1).2) ∧
    Subset (α := Set (E →SL[σ₁₂] F))
      {f : E →SL[σ₁₂] F |
        ∀ (x : E),
          Membership.mem (γ := Set E) (closedBall 0 1, closedBall 0 1).1 x →
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 1, closedBall 0 1).2
              ((f : (a : E) → F) x : F)}
      (Seminorm.closedBall ContinuousLinearMap.seminorm 0 ‖c‖)

Tactic:
suffices ∀ f : E →SL[σ₁₂] F, (∀ x, ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) → ‖f‖ ≤ ‖c‖ by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, subset_def] using this
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1
⊢ ‖f‖ ≤ ‖c‖

Tactic:
opNorm_le_of_shell (f := f) one_pos (norm_nonneg c) hc fun x hcx hx ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell, one_pos, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1
refine_1 :
  ∀ (x : E) (hcx : 1 / ‖c‖ ≤ ‖x‖) (hx : ‖x‖ < 1), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖x‖
⊢ ‖f‖ ≤ ‖c‖

Tactic:
refine opNorm_le_of_shell (f := f) one_pos (norm_nonneg c) hc fun x hcx hx ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell, one_pos, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1
x : E
hcx : 1 / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < 1
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖x‖

Tactic:
(hf x hx.le).trans ((div_le_iff₀' <| one_pos.trans hc).1 hcx)

Premises used: LT.lt.le, Iff.mp, LT.lt.trans, LE.le.trans, div_le_iff₀', one_pos
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1
x : E
hcx : 1 / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < 1
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖x‖

Tactic:
exact (hf x hx.le).trans ((div_le_iff₀' <| one_pos.trans hc).1 hcx)

Premises used: LT.lt.le, Iff.mp, LT.lt.trans, LE.le.trans, div_le_iff₀', one_pos
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
refine_2 :
  ∀ (ε : ℝ) (hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε),
    ∃ r_1 > 0,
      Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
        {f : E →SL[σ₁₂] F |
          ∀ x ∈ (s, r).1,
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}

Tactic:
rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩

Premises used: NormedSpace.isVonNBounded_iff', Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
refine_2 :
  ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hδ : ε * δ < (s, r).2),
    ∃ r_1 > 0,
      Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
        {f : E →SL[σ₁₂] F |
          ∀ x ∈ (s, r).1,
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}

Tactic:
rcases exists_pos_mul_lt hr ε with ⟨δ, hδ₀, hδ⟩

Premises used: exists_pos_mul_lt
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}

Tactic:
⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
refine_2 :
  ∀ (f : E →SL[σ₁₂] F)
    (hf : Membership.mem (γ := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 δ) f) (x : E)
    (hx : x ∈ (s, r).1),
    Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}

Tactic:
refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
hf : Membership.mem (γ := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 δ) f
x : E
hx : x ∈ (s, r).1
refine_2 :
  ∀ (hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ),
    Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r
⊢ Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)

Tactic:
simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢

Premises used: Seminorm.mem_ball_zero, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ
refine_2 :
  ∀ (hδ : δ * ε < (s, r).2) (f : E →SL[σ₁₂] F) (x : E) (hx : x ∈ (s, r).1)
    (hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ),
    Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r

Tactic:
rw [mul_comm] at hδ

Premises used: mul_comm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : δ * ε < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r

Tactic:
le_trans (le_of_opNorm_le_of_le _ hf.le (hε _ hx)) hδ.le

Premises used: ContinuousLinearMap.le_of_opNorm_le_of_le, LT.lt.le, le_trans
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : δ * ε < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r

Tactic:
exact le_trans (le_of_opNorm_le_of_le _ hf.le (hε _ hx)) hδ.le

Premises used: ContinuousLinearMap.le_of_opNorm_le_of_le, LT.lt.le, le_trans
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : NontrivialTopology E
⊢ nnnorm (E := E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E) = 1

Tactic:
NNReal.eq norm_id

Premises used: NNReal.eq, ContinuousLinearMap.norm_id
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ 0 ≤ ‖h‖ * ‖f‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
rw : Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * (‖f‖ * ‖x‖)
⊢ Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * ‖f‖ * ‖x‖

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * (‖f‖ * ‖x‖)

Tactic:
h.le_opNorm_of_le (f.le_opNorm x)

Premises used: ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm_of_le
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * (‖f‖ * ‖x‖)

Tactic:
exact h.le_opNorm_of_le (f.le_opNorm x)

Premises used: ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm_of_le
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst_7 : Subsingleton E
⊢ ‖f‖ = 0

Tactic:
norm_of_subsingleton f

Premises used: norm_of_subsingleton
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
simp_rw : ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal ‖f‖ * ENNReal.ofReal ‖x‖
⊢ enorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ₑ * ‖x‖ₑ

Tactic:
simp_rw [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ 0 ≤ ‖f‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
rw : ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal (‖f‖ * ‖x‖)
⊢ ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal ‖f‖ * ENNReal.ofReal ‖x‖

Tactic:
rw [← ENNReal.ofReal_mul (by positivity)]

Premises used: ENNReal.ofReal_mul
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
h : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * ‖x‖
⊢ ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal (‖f‖ * ‖x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * ‖x‖

Tactic:
f.le_opNorm x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * ‖x‖

Tactic:
exact f.le_opNorm x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
obtain : ∀ (x : E) (hx : ‖x‖ ≠ 0), ‖f‖ = a
⊢ ‖f‖ = a

Tactic:
obtain ⟨x, hx⟩ := exists_norm_ne_zero E

Premises used: exists_norm_ne_zero
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : ‖x‖ ≠ 0
⊢ 0 < ‖x‖

Tactic:
replace hx : 0 < ‖x‖ := lt_of_le_of_ne' (norm_nonneg _) hx
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
⊢ 0 ≤ a

Tactic:
simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)

Premises used: mul_nonneg_iff_of_pos_right, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
⊢ 0 ≤ a

Tactic:
have ha : 0 ≤ a := by simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
apply : a ≤ ‖f‖
⊢ ‖f‖ = a

Tactic:
apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))

Premises used: ContinuousLinearMap.opNorm_le_bound, le_antisymm, le_of_eq
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ a ≤ ‖f‖

Tactic:
simpa only [hf, hx, mul_le_mul_iff_left₀] using f.le_opNorm x

Premises used: ContinuousLinearMap.le_opNorm, mul_le_mul_iff_left₀