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 σ₁₂
f : E →SL[σ₁₂] F
x y : E
simp_rw : ‖HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)‖ ≤ ‖f‖ * ‖x - y‖
simp_rw₁ : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) (x - y) : F) ≤ ‖f‖ * ‖x - y‖
⊢ dist.{u_5} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) ≤ ‖f‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, ← map_sub, f.le_opNorm]

Premises used: dist_eq_norm, map_sub, 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
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
b0 : 0 ≤ a
⊢ ‖f‖ * ‖x‖ ≤ a * b

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
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ 0 ≤ a

Tactic:
(opNorm_nonneg f).trans hf

Premises used: ContinuousLinearMap.opNorm_nonneg, 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 σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ 0 ≤ a

Tactic:
exact (opNorm_nonneg f).trans hf

Premises used: ContinuousLinearMap.opNorm_nonneg, 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 σ₁₂
f : E →SL[σ₁₂] F
c : ℝ
x : E
h : ‖x‖ ≤ c
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * c

Tactic:
f.le_of_opNorm_le_of_le le_rfl h

Premises used: ContinuousLinearMap.le_of_opNorm_le_of_le, le_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 : ℝ
h : ‖f‖ ≤ c
x : E
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖

Tactic:
f.le_of_opNorm_le_of_le h le_rfl

Premises used: ContinuousLinearMap.le_of_opNorm_le_of_le, le_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
M : ℝ
hMp : 0 ≤ M
⊢ ‖f‖ ≤ M ↔ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖

Tactic:
⟨f.le_of_opNorm_le, opNorm_le_bound f hMp⟩

Premises used: ContinuousLinearMap.opNorm_le_bound, ContinuousLinearMap.le_of_opNorm_le, Iff.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 σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) / ‖x‖ ≤ ‖f‖

Tactic:
div_le_of_le_mul₀ (norm_nonneg _) f.opNorm_nonneg (le_opNorm _ _)

Premises used: div_le_of_le_mul₀, ContinuousLinearMap.le_opNorm, ContinuousLinearMap.opNorm_nonneg, 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 σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖

Tactic:
mul_one ‖f‖ ▸ f.le_opNorm_of_le

Premises used: Norm.norm, Eq.rec, ContinuousLinearMap.le_opNorm_of_le, mul_one
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
rw : ∀ ⦃s : Set E⦄, Bornology.IsBounded s → Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
⊢ comap (⇑ℓ : (a : E) → F) (cobounded F) ≤ cobounded E

Tactic:
rw [Bornology.comap_cobounded_le_iff]

Premises used: Bornology.comap_cobounded_le_iff
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
obtain : ∀ (M : ℝ) (hM : ∀ x ∈ s, ‖x‖ ≤ M), Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)
⊢ Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)

Tactic:
obtain ⟨M, hM⟩ := hs.exists_norm_le

Premises used: Bornology.IsBounded.exists_norm_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
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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
rw : ∃ (C : ℝ), ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ C
⊢ Bornology.IsBounded.{u_5} (α := F) ((⇑ℓ : (a : E) → F) '' s)

Tactic:
rw [isBounded_iff_forall_norm_le]

Premises used: isBounded_iff_forall_norm_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
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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
h₁ : ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ ‖ℓ‖ * M
⊢ ∃ (C : ℝ), ∀ (x : F), Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) x → ‖x‖ ≤ C

Tactic:
use ‖ℓ‖ * M
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
h₁ : ∀ (σ : E) (hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y), ‖y‖ ≤ ‖ℓ‖ * M
⊢ ‖y‖ ≤ ‖ℓ‖ * M

Tactic:
obtain ⟨σ, hσ⟩ := (mem_image _ _ _).1 hy

Premises used: Set.mem_image, Iff.mp
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
rw rw₁ : ‖y‖ ≤ ‖y‖
⊢ ‖y‖ ≤ Norm.norm.{u_5} (E := F) ((ℓ : (a : E) → F) σ : F)

Tactic:
rw [hσ.2]

Premises used: And.right
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
⊢ Norm.norm.{u_5} (E := F) ((ℓ : (a : E) → F) σ : F) ≤ ‖ℓ‖ * ‖σ‖

Tactic:
ContinuousLinearMap.le_opNorm ℓ σ

Premises used: ContinuousLinearMap.le_opNorm
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
⊢ ‖ℓ‖ ≤ ‖ℓ‖

Tactic:
rfl
-- 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
inst_13 : RingHomIsometric σ₁₂
inst_14 : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : Membership.mem (γ := Set F) ((⇑ℓ : (a : E) → F) '' s) y
σ : E
hσ : σ ∈ s ∧ (ℓ : (a : E) → F) σ = y
calc : ‖y‖ ≤ Norm.norm.{u_5} (E := F) ((ℓ : (a : E) → F) σ : F)
⊢ ‖y‖ ≤ ‖ℓ‖ * M

Tactic:
calc ‖y‖
      _ ≤ ‖ℓ σ‖ := by rw [hσ.2]
      _ ≤ ‖ℓ‖ * ‖σ‖ := ContinuousLinearMap.le_opNorm ℓ σ
      _ ≤ ‖ℓ‖ * M := mul_le_mul (by rfl) (hM σ hσ.1) (norm_nonneg σ) (opNorm_nonneg ℓ)

Premises used: ContinuousLinearMap.le_opNorm, And.left, mul_le_mul, ContinuousLinearMap.opNorm_nonneg, 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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
f.opNorm_le_bound' hC fun _ hx => SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf hx

Premises used: ContinuousLinearMap.opNorm_le_bound', SemilinearMapClass.bound_of_shell_semi_normed
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_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
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖f‖ ≤ C

Tactic:
opNorm_le_of_shell ε_pos hC hc fun x _ hx => hf x ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
refine : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ∀ (hx : ‖x‖ < ε), Membership.mem (γ := Set E) (ball 0 ε) x
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_shell ε_pos hC hc fun x _ hx => hf x ?_

Premises used: ContinuousLinearMap.opNorm_le_of_shell
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ (x : E), Membership.mem (γ := Set E) (ball 0 ε) x → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
x : E
h : ε / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < ε
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set E) {x : E | ‖x‖ < ε} x
⊢ Membership.mem (γ := Set E) (ball 0 ε) x

Tactic:
rwa [ball_zero_eq]

Premises used: ball_zero_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 σ₁₂
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ᶠ (x : E) in 𝓝 0, Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
let ⟨_, ε0, hε⟩ := Metric.eventually_nhds_iff_ball.1 hf
  opNorm_le_of_ball ε0 hC hε

Premises used: Norm.norm, ContinuousLinearMap.opNorm_le_of_ball, LE.le, Iff.mp, Metric.eventually_nhds_iff_ball, _private.0.ContinuousLinearMap.opNorm_le_of_nhds_zero.match_1
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
pos : ∀ (h0 : c = 0), ‖f‖ ≤ C
neg : ∀ (h0 : ¬c = 0), ‖f‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
by_cases h0 : c = 0
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
⊢ ‖f‖ ≤ C

Tactic:
opNorm_le_of_ball ε_pos hC fun x hx => hf x ?_ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_ball
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
pos : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 ε) x), ε * ‖c‖ ≤ ‖x‖
pos₁ : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 ε) x), ‖x‖ < ε
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_ball ε_pos hC fun x hx => hf x ?_ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_ball
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
x : E
hx : Membership.mem (γ := Set E) (ball 0 ε) x
⊢ ε * ‖c‖ ≤ ‖x‖

Tactic:
simp [h0]
-- 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 : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : c = 0
x : E
hx : Membership.mem (γ := Set E) (ball 0 ε) x
pos pos₁ pos₂ pos₃ : ∀ (hx : Membership.mem (γ := Set E) {x : E | ‖x‖ < ε} x), ‖x‖ < ε
⊢ ‖x‖ < ε

Tactic:
rwa [ball_zero_eq] at hx

Premises used: ball_zero_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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
⊢ 1 < ‖c⁻¹‖

Tactic:
rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc

Premises used: Iff.mpr, norm_pos_iff, inv_lt_one₀, norm_inv, inv_inv, inv_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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
h0 : ¬c = 0
hc₁ : 1 < ‖c⁻¹‖
⊢ ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc

Premises used: Iff.mpr, norm_pos_iff, inv_lt_one₀, norm_inv, inv_inv, inv_ne_zero