awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : DenselyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h : Nontrivial E
this : NormedSpace ℝ E
ub : ℝ≥0
hub : ub < ‖f‖₊
x : E
hx : ‖x‖₊ = 1
hxf : ub < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) a ∧
      ub < a

Tactic:
exact ⟨_, ⟨x, by simpa using congrArg NNReal.toReal hx, rfl⟩, hxf⟩
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : DenselyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
⊢ sSup ((fun (x : E) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖

Tactic:
simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_sphere_eq_nnnorm

Premises used: Iff.mpr, Set.image_image, NNReal.coe_sSup, ContinuousLinearMap.sSup_sphere_eq_nnnorm, NNReal.coe_inj
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
inst_7 : RingHomIsometric σ₁₂
f : E →ₛₗᵢ[σ₁₂] F
⊢ ∀ (x : E), norm.{u_5} (E := F) ((f.toContinuousLinearMap : (a : E) → F) x : F) = 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
inst_7 : RingHomIsometric σ₁₂
f : E →ₛₗᵢ[σ₁₂] F
⊢ ‖f.toContinuousLinearMap‖₊ = 1

Tactic:
Subtype.ext f.norm_toContinuousLinearMap

Premises used: LinearIsometry.norm_toContinuousLinearMap, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
inst_7 : RingHomIsometric σ₁₂
f : E →ₛₗᵢ[σ₁₂] F
⊢ ‖f.toContinuousLinearMap‖ₑ = 1

Tactic:
congrArg _ f.nnnorm_toContinuousLinearMap

Premises used: LinearIsometry.nnnorm_toContinuousLinearMap, ENNReal.ofNNReal, congrArg, WithTop.some
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 σ₁₂
f : F →ₛₗᵢ[σ₂₃] G
g : E →SL[σ₁₂] F
x : E
⊢ norm.{u_7} (E := G) ((f.toContinuousLinearMap ∘SL g : (a : E) → G) x : G) =
    norm.{u_5} (E := F) ((g : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f_1 : E →SL[σ₁₂] F
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₁₃
a : F →ₛₗᵢ[σ₂₃] G
f g : E →SL[σ₁₂] F
⊢ a.toContinuousLinearMap ∘SL (f + g) = a.toContinuousLinearMap ∘SL f + a.toContinuousLinearMap ∘SL g

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f_1 : E →SL[σ₁₂] F
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₁₃
a : F →ₛₗᵢ[σ₂₃] G
c : 𝕜₂
f : E →SL[σ₁₂] F
⊢ a.toContinuousLinearMap ∘SL (c • f) =
    HSMul.hSMul (α := 𝕜₃) ((σ₂₃ : (a : 𝕜₂) → 𝕜₃) c : 𝕜₃) (a.toContinuousLinearMap ∘SL f)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
f_1 : E →SL[σ₁₂] F
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₁₃
a : F →ₛₗᵢ[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ norm (E := E →SL[σ₁₃] G)
      (({ toFun := fun (f : E →SL[σ₁₂] F) ↦ a.toContinuousLinearMap ∘SL f, map_add' := ⋯, map_smul' := ⋯ :
              (E →SL[σ₁₂] F) →ₛₗ[σ₂₃] E →SL[σ₁₃] G } :
            (a : E →SL[σ₁₂] F) → E →SL[σ₁₃] G)
          f :
        E →SL[σ₁₃] G) =
    ‖f‖

Tactic:
simp [a.norm_toContinuousLinearMap_comp]

Premises used: LinearIsometry.norm_toContinuousLinearMap_comp
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
inst_9 : RingHomIsometric σ₁₂
e : E ≃ₛₗᵢ[σ₁₂] F
⊢ ‖(↑(↑e : E ≃SL[σ₁₂] F) : E →SL[σ₁₂] F)‖ = 1

Tactic:
e.toLinearIsometry.norm_toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.norm_toContinuousLinearMap, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
inst_9 : RingHomIsometric σ₁₂
e : E ≃ₛₗᵢ[σ₁₂] F
⊢ ‖(↑(↑e : E ≃SL[σ₁₂] F) : E →SL[σ₁₂] F)‖₊ = 1

Tactic:
e.toLinearIsometry.nnnorm_toContinuousLinearMap

Premises used: LinearIsometry.nnnorm_toContinuousLinearMap, LinearIsometryEquiv.toLinearIsometry, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
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 : NontrivialTopology E
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
inst_9 : RingHomIsometric σ₁₂
e : E ≃ₛₗᵢ[σ₁₂] F
⊢ ‖(↑(↑e : E ≃SL[σ₁₂] F) : E →SL[σ₁₂] F)‖ₑ = 1

Tactic:
e.toLinearIsometry.enorm_toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.enorm_toContinuousLinearMap, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] 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
pos : ∀ (hx : x = 0), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
neg : ∀ (hx : ¬x = 0), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] 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:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] 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:
SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)

Premises used: Iff.mpr, SemilinearMapClass.bound_of_shell_semi_normed, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] 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:
exact SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)

Premises used: Iff.mpr, SemilinearMapClass.bound_of_shell_semi_normed, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
obtain : ∀ (k : 𝕜) (hk : 1 < ‖k‖), ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖
⊢ ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖

Tactic:
obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial 𝕜 _

Premises used: NontriviallyNormedField.non_trivial
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
h₁ : ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c * (‖k‖ / r) * ‖z‖
⊢ ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖

Tactic:
use c * (‖k‖ / r)

Premises used: Norm.norm, HDiv.hDiv
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
⊢ norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c * (‖k‖ / r) * ‖z‖

Tactic:
bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _

Premises used: LinearMap.bound_of_shell
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z : E
h₁ :
  ∀ (x : E) (hko : r / ‖k‖ ≤ ‖x‖) (hxo : ‖x‖ < r),
    norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) x : Fₗ) ≤ c * (‖k‖ / r) * ‖x‖
⊢ norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c * (‖k‖ / r) * ‖z‖

Tactic:
refine bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _

Premises used: LinearMap.bound_of_shell
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) x : Fₗ) ≤ c

Tactic:
h _ (mem_ball_zero_iff.mpr hxo)

Premises used: Iff.mpr, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ c ≤ c * (‖x‖ * ‖k‖ / r)

Tactic:
le_mul_of_one_le_right ?_ ?_

Premises used: le_mul_of_one_le_right
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ c * (‖x‖ * ‖k‖ / r) = c * (‖k‖ / r) * ‖x‖

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
h₁ : 0 ≤ c
h₂ : 1 ≤ ‖x‖ * ‖k‖ / r
⊢ norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) x : Fₗ) ≤ c * (‖k‖ / r) * ‖x‖

Tactic:
calc
    ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
    _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
    _ = _ := by ring

Premises used: Iff.mpr, Norm.norm, HMul.hMul, HDiv.hDiv, le_mul_of_one_le_right, DFunLike.coe, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ Membership.mem (γ := Set E) (ball 0 r) 0

Tactic:
simp [r_pos]
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

Tactic:
exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))

Premises used: OfNat.ofNat, norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ r ≤ ‖x‖ * ‖k‖

Tactic:
rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko

Premises used: div_le_iff₀, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
hko₁ : r ≤ ‖x‖ * ‖k‖
⊢ ‖x‖ < r

Tactic:
rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko

Premises used: div_le_iff₀, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r ≤ ‖x‖ * ‖k‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r

Tactic:
(one_le_div r_pos).mpr hko

Premises used: Iff.mpr, one_le_div
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup Fₗ
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r ≤ ‖x‖ * ‖k‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r

Tactic:
exact (one_le_div r_pos).mpr hko

Premises used: Iff.mpr, one_le_div
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
rcases :
  ∀ (ε : ℝ) (ε0 : 0 < ε)
    (hε : Subset.{u_4} (α := Set E) (Set.preimage.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (ball 0 ε)) (ball 0 1)),
    ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩

Premises used: Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Iff.mp, Metric.nhds_basis_ball, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ
ε0 : 0 < ε
hε : Subset.{u_4} (α := Set E) (Set.preimage.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (ball 0 ε)) (ball 0 1)
⊢ ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ε → ‖x‖ < 1

Tactic:
simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε

Premises used: Set.subset_def, Set.mem_preimage, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ε → ‖x‖ < 1
⊢ 0 ≤ ε

Tactic:
ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ε → ‖x‖ < 1
lift :
  ∀ (ε : ℝ≥0) (ε0 : 0 < (↑ε : ℝ)) (hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1),
    ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
lift ε to ℝ≥0 using ε0.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Operator.NormedSpace
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : LE.le.{u_4} (α := Filter E) (Filter.comap.{u_4, u_5} (β := F) (⇑f : (a : E) → F) (𝓝 0)) (𝓝 0)
ε : ℝ≥0
ε0 : 0 < (↑ε : ℝ)
hε : ∀ (x : E), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) < (↑ε : ℝ) → ‖x‖ < 1
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)

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

Premises used: NormedField.exists_one_lt_norm