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 : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ nnnorm.{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.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ENNReal) ≤ (↑‖f‖₊ : ENNReal) * (↑‖x‖₊ : ENNReal)

Tactic:
mod_cast le_opNNNorm ..

Premises used: ENNReal.ofNNReal, cast, WithTop.some, ENNReal.coe_le_coe._simp_1, ContinuousLinearMap.le_opNNNorm, Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ENNReal) ≤ (↑‖f‖₊ : ENNReal) * (↑‖x‖₊ : ENNReal)

Tactic:
exact mod_cast le_opNNNorm ..

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

Tactic:
dist_le_opNorm f x y

Premises used: ContinuousLinearMap.dist_le_opNorm
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ LipschitzWith.{u_4, u_5} (α := E) (β := F) ‖f‖₊ (⇑f : (a : E) → F)

Tactic:
AddMonoidHomClass.lipschitz_of_bound_nnnorm f _ f.le_opNNNorm

Premises used: AddMonoidHomClass.lipschitz_of_bound_nnnorm, ContinuousLinearMap.le_opNNNorm
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
x : E
⊢ LipschitzWith (β := F) ‖x‖₊ fun (f : E →SL[σ₁₂] F) ↦ (f : (a : E) → F) x

Tactic:
lipschitzWith_iff_norm_sub_le.2 fun f g => ((f - g).le_opNorm x).trans_eq (mul_comm _ _)

Premises used: Iff.mpr, Norm.norm, LE.le.trans_eq, ContinuousLinearMap.le_opNorm, HSub.hSub, lipschitzWith_iff_norm_sub_le, mul_comm
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ (x : E), r * ‖x‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simpa only [not_forall, not_le, Set.mem_setOf] using
    notMem_of_lt_csInf (nnnorm_def f ▸ hr : r < sInf { c : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ })
      (OrderBot.bddBelow _)

Premises used: not_le, ContinuousLinearMap.nnnorm_def, Eq.rec, Set.mem_setOf, notMem_of_lt_csInf, OrderBot.bddBelow, Classical.not_forall
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr₀ : 0 ≤ r
hr : r < ‖f‖
⊢ 0 ≤ r

Tactic:
hr₀
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr₀ : 0 ≤ r
hr : r < ‖f‖
lift : ∀ (r : ℝ≥0) (hr : (↑r : ℝ) < ‖f‖), ∃ (x : E), (↑r : ℝ) * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (x : E), r * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
lift r to ℝ≥0 using hr₀
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : (↑r : ℝ) < ‖f‖
⊢ ∃ (x : E), (↑r : ℝ) * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
f.exists_mul_lt_apply_of_lt_opNNNorm hr

Premises used: ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : (↑r : ℝ) < ‖f‖
⊢ ∃ (x : E), (↑r : ℝ) * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
exact f.exists_mul_lt_apply_of_lt_opNNNorm hr

Premises used: ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm
-- Module: Mathlib.Analysis.Normed.Operator.NNNorm
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_7 : RingHomInvPair σ₁₂ σ₂₁
inst_8 : RingHomInvPair σ₂₁ σ₁₂
e : E ≃SL[σ₁₂] F
⊢ LipschitzWith.{u_4, u_5} (α := E) (β := F) ‖(↑e : E →SL[σ₁₂] F)‖₊ (⇑e : (a : E) → F)

Tactic:
(e : E →SL[σ₁₂] F).lipschitz

Premises used: ContinuousLinearMap.lipschitz, ContinuousLinearEquiv.toContinuousLinearMap
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
obtain :
  ∀ (y : E) (hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)),
    ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_opNNNorm hr

Premises used: ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
heq : y = 0
⊢ False

Tactic:
simp [heq, nnnorm_zero, map_zero] at hy

Premises used: map_zero, nnnorm_zero
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
⊢ ‖y‖₊ ≠ 0

Tactic:
have hy' : ‖y‖₊ ≠ 0 :=
    nnnorm_ne_zero_iff.2 fun heq => by
      simp [heq, nnnorm_zero, map_zero] at hy
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
hy' : ‖y‖₊ ≠ 0
⊢ nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0

Tactic:
have hfy : ‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
⊢ r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹

Tactic:
rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ←
    mul_assoc, ← NNReal.lt_inv_iff_mul_lt hy'] at hy

Premises used: NNNorm.nnnorm, mul_assoc, NNReal.lt_inv_iff_mul_lt, inv_inv, mul_comm, inv_ne_zero, DFunLike.coe
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
hy₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
⊢ ‖y‖₊ ≠ 0

Tactic:
rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ←
    mul_assoc, ← NNReal.lt_inv_iff_mul_lt hy'] at hy

Premises used: NNNorm.nnnorm, mul_assoc, NNReal.lt_inv_iff_mul_lt, inv_inv, mul_comm, inv_ne_zero, DFunLike.coe
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
hy₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
hy'₁ : ‖y‖₊ ≠ 0
⊢ nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0

Tactic:
rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ←
    mul_assoc, ← NNReal.lt_inv_iff_mul_lt hy'] at hy

Premises used: NNNorm.nnnorm, mul_assoc, NNReal.lt_inv_iff_mul_lt, inv_inv, mul_comm, inv_ne_zero, DFunLike.coe
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
obtain :
  ∀ (k : 𝕜) (hk₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖k‖₊) (hk₂ : ‖k‖₊ < ‖y‖₊⁻¹),
    ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy

Premises used: NormedField.exists_lt_nnnorm_lt
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
k : 𝕜
hk₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩

Premises used: nnnorm_smul, Eq.rec, NNReal.lt_inv_iff_mul_lt, And.intro, Exists.intro, Iff.mp, HSMul.hSMul, Eq.symm
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
k : 𝕜
hk₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
refine : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
refine ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
k : 𝕜
hk₁ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
rwa : r < ‖HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) ((f : (a : E) → F) y : F)‖₊
rwa₁ : r < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) * nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
rwa₂ : r / nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
rwa₃ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
rwa₄ rwa₅ rwa₆ rwa₇ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < ‖k‖₊
⊢ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)

Tactic:
rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv,
    RingHomIsometric.nnnorm_map]

Premises used: nnnorm_smul, MulActionSemiHomClass.map_smulₛₗ, RingHomIsometric.nnnorm_map, div_lt_iff₀, div_eq_mul_inv, Ne.bot_lt
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
pos : ∀ (hr₀ : r < 0), ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
neg : ∀ (hr₀ : ¬r < 0), ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
by_cases hr₀ : r < 0
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : r < 0
⊢ Norm.norm.{u_4} (E := E) 0 < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)

Tactic:
simpa using hr₀
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : r < 0
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
exact ⟨0, by simpa using hr₀⟩
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : ¬r < 0
⊢ 0 ≤ r

Tactic:
not_lt.1 hr₀

Premises used: not_lt, Iff.mp
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : ¬r < 0
neg :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ) < ‖f‖) (hr₀ : ¬(↑r : ℝ) < 0),
    ∃ (x : E), ‖x‖ < 1 ∧ (↑r : ℝ) < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
lift r to ℝ≥0 using not_lt.1 hr₀

Premises used: not_lt, Iff.mp
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : (↑r : ℝ) < ‖f‖
hr₀ : ¬(↑r : ℝ) < 0
⊢ ∃ (x : E), ‖x‖ < 1 ∧ (↑r : ℝ) < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
f.exists_lt_apply_of_lt_opNNNorm hr

Premises used: ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm, NNReal.toReal
-- 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : (↑r : ℝ) < ‖f‖
hr₀ : ¬(↑r : ℝ) < 0
⊢ ∃ (x : E), ‖x‖ < 1 ∧ (↑r : ℝ) < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
exact f.exists_lt_apply_of_lt_opNNNorm hr

Premises used: ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm
-- 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 σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) = ‖f‖₊

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_
    fun ub hub => ?_

Premises used: Iff.mpr, Metric.nonempty_ball, zero_lt_one, Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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 σ₁₂
f : E →SL[σ₁₂] F
refine_1 :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) a →
      a ≤ ‖f‖₊
refine_2 :
  ∀ (ub : ℝ≥0) (hub : ub < ‖f‖₊),
    ∃ (a : ℝ≥0),
      Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) a ∧
        ub < a
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) = ‖f‖₊

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_
    fun ub hub => ?_

Premises used: Iff.mpr, Metric.nonempty_ball, zero_lt_one, Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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 σ₁₂
f : E →SL[σ₁₂] F
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ (fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) x ≤ ‖f‖₊

Tactic:
simpa only [mul_one] using f.le_opNorm_of_le (mem_ball_zero_iff.1 hx).le

Premises used: LT.lt.le, ContinuousLinearMap.le_opNorm_of_le, Iff.mp, mul_one, mem_ball_zero_iff
-- 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 σ₁₂
f : E →SL[σ₁₂] F
ub : ℝ≥0
hub : ub < ‖f‖₊
refine_2 :
  ∀ (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)) '' ball 0 1) a ∧
        ub < a
⊢ ∃ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) a ∧
      ub < a

Tactic:
obtain ⟨x, hx, hxf⟩ := f.exists_lt_apply_of_lt_opNNNorm hub

Premises used: ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm
-- 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 σ₁₂
f : E →SL[σ₁₂] F
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)) '' ball 0 1) a ∧
      ub < a

Tactic:
⟨_, ⟨x, mem_ball_zero_iff.2 hx, rfl⟩, hxf⟩

Premises used: Iff.mpr, And.intro, Exists.intro, rfl, mem_ball_zero_iff