awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
⊢ Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F') →
    sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
refine :
  ∀ (h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')),
    Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')
⊢ sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F') ↔
    Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')
grw : Convex.{0, u_9} ℝ (E := F') (Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F'))
⊢ Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')

Tactic:
grw [← (closedBall_subset_range_iff_surjective x hr), ← convexHull_sphere_eq_closedBall x hr.le,
    convexHull_mono h, (convexHull_eq_self (𝕜 := ℝ) (s := Set.range ↑f)).mpr]

Premises used: Iff.mpr, LT.lt.le, closedBall_subset_range_iff_surjective, convexHull_sphere_eq_closedBall, convexHull_mono, convexHull_eq_self
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')
⊢ Convex.{0, u_9} ℝ (E := F') (Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F'))

Tactic:
Submodule.Convex.semilinear_range (E := F') (F' := E) (σ := τ) f

Premises used: setOf, SemilinearMapClass.semilinearMap, Set.range, Submodule.Convex.semilinear_range
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')
⊢ Convex.{0, u_9} ℝ (E := F') (Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F'))

Tactic:
exact Submodule.Convex.semilinear_range (E := F') (F' := E) (σ := τ) f

Premises used: SemilinearMapClass.semilinearMap, Submodule.Convex.semilinear_range
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
x : E
hx : ‖x‖ = 0
rw : ∀ (hx : 0 ⤳ x), Specializes.{u_5} (X := F) ((f : (a : E) → F) 0 : F) ((f : (a : E) → F) x : F)
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = 0

Tactic:
rw [← mem_closure_zero_iff_norm, ← specializes_iff_mem_closure, ← map_zero f] at *

Premises used: specializes_iff_mem_closure, map_zero, mem_closure_zero_iff_norm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
x : E
hx : 0 ⤳ x
⊢ Specializes.{u_5} (X := F) ((f : (a : E) → F) 0 : F) ((f : (a : E) → F) x : F)

Tactic:
hx.map hf

Premises used: Specializes.map
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
x : E
hx : 0 ⤳ x
⊢ Specializes.{u_5} (X := F) ((f : (a : E) → F) 0 : F) ((f : (a : E) → F) x : F)

Tactic:
exact hx.map hf

Premises used: Specializes.map
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : RingHomIsometric σ₁₂
inst_8 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x : E
hx : ‖x‖ ≠ 0
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
(normSeminorm 𝕜 E).bound_of_shell ((normSeminorm 𝕜₂ F).comp ⟨⟨f, map_add f⟩, map_smulₛₗ f⟩)
    ε_pos hc hf hx

Premises used: Seminorm.bound_of_shell, map_add, MulActionSemiHomClass.map_smulₛₗ, normSeminorm, LinearMap.mk, Seminorm.comp, AddHom.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : RingHomIsometric σ₁₂
inst_8 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
let φ : E →ₛₗ[σ₁₂] F := ⟨⟨f, map_add f⟩, map_smulₛₗ f⟩
  ((normSeminorm 𝕜₂ F).comp φ).bound_of_continuous_normedSpace (continuous_norm.comp hf)

Premises used: Seminorm.bound_of_continuous_normedSpace, Continuous.comp, map_add, MulActionSemiHomClass.map_smulₛₗ, normSeminorm, LinearMap.mk, Seminorm.comp, AddHom.mk, DFunLike.coe, continuous_norm
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : RingHomIsometric σ₁₂
inst_8 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
⊢ ∃ (C : ℝ≥0), 0 < C ∧ ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖₊

Tactic:
let ⟨c, hc, hcf⟩ := SemilinearMapClass.bound_of_continuous f hf; ⟨⟨c, hc.le⟩, hc, hcf⟩

Premises used: SemilinearMapClass.bound_of_continuous, Exists, _private.0.SemilinearMapClass.nnbound_of_continuous.match_1, LT.lt.le, Subtype.mk, And, And.intro, LT.lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : RingHomIsometric σ₁₂
inst_8 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
⊢ ∃ (C : ℝ≥0), 0 < C ∧ ∀ (x : E), enorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑C : ENNReal) * ‖x‖ₑ

Tactic:
let ⟨c, hc, hcf⟩ := SemilinearMapClass.nnbound_of_continuous f hf
  ⟨c, hc, fun x => ENNReal.coe_mono <| hcf x⟩

Premises used: _private.0.SemilinearMapClass.ebound_of_continuous.match_1, SemilinearMapClass.nnbound_of_continuous, Exists, And, And.intro, LT.lt, Exists.intro, ENNReal.coe_mono, OfNat.ofNat
-- 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
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
SemilinearMapClass.bound_of_continuous f f.2

Premises used: SemilinearMapClass.bound_of_continuous, ContinuousLinearMap.cont
-- 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
⊢ ∃ (C : ℝ≥0), 0 < C ∧ ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖₊

Tactic:
SemilinearMapClass.nnbound_of_continuous f f.2

Premises used: SemilinearMapClass.nnbound_of_continuous, ContinuousLinearMap.cont
-- 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
⊢ ∃ (C : ℝ≥0), 0 < C ∧ ∀ (x : E), enorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑C : ENNReal) * ‖x‖ₑ

Tactic:
SemilinearMapClass.ebound_of_continuous f f.2

Premises used: SemilinearMapClass.ebound_of_continuous, ContinuousLinearMap.cont
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup Fₗ
inst_3 : SeminormedAddCommGroup G
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NontriviallyNormedField 𝕜₂
inst_6 : NontriviallyNormedField 𝕜₃
inst_7 : NormedSpace 𝕜 E
inst_8 : NormedSpace 𝕜₂ F
inst_9 : NormedSpace 𝕜 Fₗ
inst_10 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_12 : FunLike 𝓕 E F
v : E
hv : ‖v‖ = 1
x : 𝕜
⊢ norm.{u_4} (E := E) ((LinearMap.toSpanSingleton 𝕜 E v : (a : 𝕜) → E) x : E) = ‖x‖

Tactic:
simp [norm_smul, hv]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
v : E
hv : ‖v‖ = 1
a : 𝕜
⊢ (LinearIsometry.toSpanSingleton 𝕜 E hv : (a : 𝕜) → E) a = a • v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
v : E
hv : ‖v‖ = 1
⊢ Eq (α := 𝕜 →ₗ[𝕜] E) (LinearIsometry.toLinearMap (LinearIsometry.toSpanSingleton 𝕜 E hv))
    (LinearMap.toSpanSingleton 𝕜 E v)

Tactic:
rfl

Premises used: LinearMap.smulRight, LinearMap.toSpanSingleton, rfl
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}

Tactic:
rfl

Premises used: ContinuousLinearMap.opNorm, rfl
-- 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
⊢ ∃ (c : ℝ),
    Membership.mem (γ := Set ℝ)
      {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖} c

Tactic:
let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

Premises used: _private.0.ContinuousLinearMap.bounds_nonempty.match_1, setOf, le_of_lt, Membership.mem, Exists, LE.le, And, And.intro, Exists.intro, OfNat.ofNat, ContinuousLinearMap.bound
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ BddBelow (α := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}

Tactic:
⟨0, fun _ ⟨hn, _⟩ => hn⟩

Premises used: _private.0.ContinuousLinearMap.bounds_bddBelow.match_1, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- 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
⊢ IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖} ‖f‖

Tactic:
IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Premises used: ContinuousLinearMap.bounds_nonempty, ContinuousLinearMap.opNorm, ContinuousLinearMap.bounds_bddBelow, IsClosed.isLeast_csInf
-- 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
refine : IsClosed (X := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}
⊢ IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖} ‖f‖

Tactic:
refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Premises used: ContinuousLinearMap.bounds_nonempty, ContinuousLinearMap.bounds_bddBelow, IsClosed.isLeast_csInf
-- 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
simp :
  IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})
⊢ IsClosed (X := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}

Tactic:
simp only [setOf_and, setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall
-- 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
⊢ IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})

Tactic:
isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_

Premises used: Set.Ici, setOf, isClosed_le, IsClosed.inter, isClosed_iInter, isClosed_Ici
-- 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
refine_1 : ∀ (x : E), Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
refine_2 : ∀ (x : E), Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ x_1 * ‖x‖
⊢ IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})

Tactic:
refine isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_

Premises used: isClosed_le, IsClosed.inter, isClosed_iInter, isClosed_Ici
-- 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
⊢ Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
fun_prop
-- 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
⊢ Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ x_1 * ‖x‖

Tactic:
fun_prop
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖
⊢ ‖f‖ ≤ M

Tactic:
csInf_le bounds_bddBelow ⟨hMp, hM⟩

Premises used: ContinuousLinearMap.opNorm, ContinuousLinearMap.bounds_bddBelow, And.intro, csInf_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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : E), ‖x‖ ≠ 0 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖
x : E
h : ‖x‖ = 0
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖

Tactic:
simp only [h, mul_zero, norm_image_of_norm_eq_zero f f.2 h, le_refl]

Premises used: le_refl, MulZeroClass.mul_zero, norm_image_of_norm_eq_zero, ContinuousLinearMap.cont
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
φ : E →SL[σ₁₂] F
M : ℝ
M_nonneg : 0 ≤ M
h_above : ∀ (x : E), Norm.norm.{u_5} (E := F) ((φ : (a : E) → F) x : F) ≤ M * ‖x‖
h_below : ∀ N ≥ 0, (∀ (x : E), Norm.norm.{u_5} (E := F) ((φ : (a : E) → F) x : F) ≤ N * ‖x‖) → M ≤ N
⊢ ‖φ‖ = M

Tactic:
le_antisymm (φ.opNorm_le_bound M_nonneg h_above)
    ((le_csInf_iff ContinuousLinearMap.bounds_bddBelow ⟨M, M_nonneg, h_above⟩).mpr
      fun N ⟨N_nonneg, hN⟩ => h_below N N_nonneg hN)

Premises used: Iff.mpr, le_csInf_iff, ContinuousLinearMap.bounds_bddBelow, ContinuousLinearMap.opNorm_le_bound, _private.0.ContinuousLinearMap.bounds_bddBelow.match_1, LE.le, le_antisymm, 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_def, neg_apply, norm_neg]

Premises used: ContinuousLinearMap.norm_def, ContinuousLinearMap.neg_apply, norm_neg
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ 0 ≤ ‖f‖

Tactic:
Real.sInf_nonneg fun _ ↦ And.left

Premises used: ContinuousLinearMap.opNorm, Real.sInf_nonneg, And.left
-- 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
σ₁₂ : 𝕜 →+* 𝕜₂
x : E
⊢ Norm.norm.{u_5} (E := F) ((0 : (a : E) → F) x : F) ≤ 0 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Basic
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
x : E
⊢ Norm.norm (E := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E) ≤ 1 * ‖x‖

Tactic:
simp
-- 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:
(isLeast_opNorm f).1.2 x

Premises used: And.right, And.left, ContinuousLinearMap.isLeast_opNorm