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 σ₁₂
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:
exact ⟨_, ⟨x, mem_ball_zero_iff.2 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 σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun (x : E) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) = ‖f‖

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

Premises used: Iff.mpr, Set.image_image, NNReal.coe_sSup, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, NNReal.coe_inj
-- 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) (closedBall 0 1) x
⊢ (fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) x ≤ ‖f‖₊

Tactic:
f.unit_le_opNorm x (mem_closedBall_zero_iff.1 hx)

Premises used: Iff.mp, ContinuousLinearMap.unit_le_opNorm, mem_closedBall_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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 1) x
⊢ (fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) x ≤ ‖f‖₊

Tactic:
exact f.unit_le_opNorm x (mem_closedBall_zero_iff.1 hx)

Premises used: Iff.mp, ContinuousLinearMap.unit_le_opNorm, mem_closedBall_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
⊢ ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊

Tactic:
have hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊ := by
    rintro - ⟨x, hx, rfl⟩
    exact f.unit_le_opNorm x (mem_closedBall_zero_iff.1 hx)
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1) = ‖f‖₊

Tactic:
le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, le_antisymm, Set.Nonempty.image, csSup_le
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
refine : ‖f‖₊ ≤ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1) = ‖f‖₊

Tactic:
refine le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, le_antisymm, Set.Nonempty.image, csSup_le
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
rw :
  LE.le (α := ℝ≥0) (sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1))
    (sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1))
⊢ ‖f‖₊ ≤ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)

Tactic:
rw [← sSup_unit_ball_eq_nnnorm]

Premises used: ContinuousLinearMap.sSup_unit_ball_eq_nnnorm
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
h₁ : BddAbove (α := ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
h₂ : Subset.{u_4} (α := Set E) (ball 0 1) (closedBall 0 1)
⊢ LE.le (α := ℝ≥0) (sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1))
    (sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1))

Tactic:
gcongr
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
⊢ BddAbove (α := ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)

Tactic:
⟨‖f‖₊, hbdd⟩

Premises used: NNNorm.nnnorm, BddAbove, Set.Nonempty, Exists.intro
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
⊢ Subset.{u_4} (α := Set E) (ball 0 1) (closedBall 0 1)

Tactic:
ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall
-- 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
hbdd :
  ∀ (y : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
        y →
      y ≤ ‖f‖₊
⊢ BddAbove (α := ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)

Tactic:
exacts [⟨‖f‖₊, hbdd⟩, ball_subset_closedBall]

Premises used: Metric.ball_subset_closedBall
-- 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) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1) = ‖f‖

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

Premises used: Iff.mpr, Set.image_image, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, NNReal.coe_sSup, NNReal.coe_inj
-- 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
r : ℝ≥0
hr : r < ‖f‖₊
obtain :
  ∀ (x : E) (hlt : ‖x‖₊ < 1) (hr : 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)
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
obtain ⟨x, hlt, hr⟩ := exists_lt_apply_of_lt_opNNNorm f 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 σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
inl :
  ∀ (hlt : nnnorm.{u_4} (E := E) 0 < 1) (hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)),
    ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
inr : ∀ (hx0 : 0 < ‖x‖₊), ∃ (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 rfl | hx0 := eq_zero_or_nnnorm_pos x

Premises used: eq_zero_or_nnnorm_pos, rfl
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
hlt : nnnorm.{u_4} (E := E) 0 < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simp at 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 σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
h :
  ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖₊ = 1 ∧
    r <
      nnnorm.{u_5} (E := F) ((f : (a : E) → F) (HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x) : F)
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
use algebraMap ℝ 𝕜 ‖x‖⁻¹ • x

Premises used: Norm.norm, Real, Algebra.algebraMap, Inv.inv, 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 σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
this : r < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖₊ = 1 ∧
    r <
      nnnorm.{u_5} (E := F) ((f : (a : E) → F) (HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x) : F)

Tactic:
simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this

Premises used: nnnorm_smul, LT.lt.ne', inv_mul_cancel₀
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
h : r < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖₊ = 1 ∧
    r <
      nnnorm.{u_5} (E := F) ((f : (a : E) → F) (HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x) : F)

Tactic:
suffices r < ‖x‖₊⁻¹ * ‖f x‖₊ by simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
⊢ r < 1⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simpa
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
ha : 0 < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ 1⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
gcongr
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
⊢ 0 < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
hr.pos

Premises used: LT.lt.pos
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
⊢ 0 < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
exact hr.pos

Premises used: LT.lt.pos
-- 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
r : ℝ≥0
hr_1 : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
hx0 : 0 < ‖x‖₊
r₁ : r < 1⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
r₂ : 1⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ r < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
calc
    r < 1⁻¹ * ‖f x‖₊ := by simpa
    _ < ‖x‖₊⁻¹ * ‖f x‖₊ := by gcongr; exact hr.pos

Premises used: 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 σ₁₂
inst_7 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
inl : Subsingleton E → sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
inr : Nontrivial E → sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊

Tactic:
cases subsingleton_or_nontrivial E

Premises used: subsingleton_or_nontrivial
-- 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 : Subsingleton E
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊

Tactic:
simp [sphere_eq_empty_of_subsingleton one_ne_zero]

Premises used: one_ne_zero, Metric.sphere_eq_empty_of_subsingleton
-- 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
inr :
  ∀ (this : NormedSpace ℝ E),
    sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊

Tactic:
have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
-- 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
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt
      ((NormedSpace.sphere_nonempty.mpr zero_le_one).image _) ?_ fun ub hub => ?_

Premises used: Iff.mpr, zero_le_one, Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt, NormedSpace.sphere_nonempty
-- 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
inr :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) a →
      a ≤ ‖f‖₊
inr₁ :
  ∀ (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)) '' sphere 0 1) a ∧
        ub < a
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
      ((NormedSpace.sphere_nonempty.mpr zero_le_one).image _) ?_ fun ub hub => ?_

Premises used: Iff.mpr, zero_le_one, Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt, NormedSpace.sphere_nonempty
-- 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
x : E
hx : Membership.mem (γ := Set E) (sphere 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_sphere_zero_iff_norm.1 hx).le

Premises used: Eq.le, ContinuousLinearMap.le_opNorm_of_le, mem_sphere_zero_iff_norm, Iff.mp, mul_one
-- 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‖₊
inr :
  ∀ (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
⊢ ∃ (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:
obtain ⟨x, hx, hxf⟩ := f.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm hub

Premises used: ContinuousLinearMap.exists_nnnorm_eq_one_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 σ₁₂
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)
⊢ Membership.mem (γ := Set E) (sphere 0 1) x

Tactic:
simpa using congrArg NNReal.toReal hx

Premises used: congrArg, NNReal.toReal