awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) = ‖f‖₊
have 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
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_
    fun ub hub => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, hx, hxf⟩ := f.exists_lt_apply_of_lt_opNNNorm hub
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (hypothesis)
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)) '' closedBall 0 1) = ‖f‖₊
have 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‖₊
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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
have refine : ‖f‖₊ ≤ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
Tactic: refine le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ‖f‖₊ ≤ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
have 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))
Tactic: rw [← sSup_unit_ball_eq_nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ 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))
have h₁ : BddAbove (α := ℝ≥0) ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' closedBall 0 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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)
⊢ 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))
have h₂ : Subset.{u_4} (α := Set E) (ball 0 1) (closedBall 0 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: obtain ⟨x, hlt, hr⟩ := exists_lt_apply_of_lt_opNNNorm f hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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)
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: obtain rfl | hx0 := eq_zero_or_nnnorm_pos x
Cleared hypotheses: x, hlt, hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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)
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have inr : ∀ (hx0 : 0 < ‖x‖₊), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ∃ (x : E), ‖x‖₊ = 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: use algebraMap ℝ 𝕜 ‖x‖⁻¹ • x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ‖HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x‖₊ = 1 ∧
    r <
      nnnorm.{u_5} (E := F) ((f : (a : E) → F) (HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖x‖⁻¹ : 𝕜) x) : F)
have h : r < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: suffices r < ‖x‖₊⁻¹ * ‖f x‖₊ by simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ 1⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have ha : 0 < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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 < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have r₁ : r < 1⁻¹ * 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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 < ‖x‖₊⁻¹ * nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: calc
    r < 1⁻¹ * ‖f x‖₊ := by simpa
    _ < ‖x‖₊⁻¹ * ‖f x‖₊ := by gcongr; exact hr.pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
have inl : Subsingleton E → 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
have inr : Nontrivial E → 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
have inr : ∀ (this : NormedSpace ℝ E), 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
have 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‖₊
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
      ((NormedSpace.sphere_nonempty.mpr zero_le_one).image _) ?_ fun ub hub => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' sphere 0 1) = ‖f‖₊
have 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
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt
      ((NormedSpace.sphere_nonempty.mpr zero_le_one).image _) ?_ fun ub hub => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NNNorm (goal)
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‖₊
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, hx, hxf⟩ := f.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm hub
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have pos : ∀ (hx : x = 0), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
have neg : ∀ (hx : ¬x = 0), norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖
have obtain : ∀ (k : 𝕜) (hk : 1 < ‖k‖), ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖
Tactic: obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial 𝕜 _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
⊢ ∃ (C : ℝ), ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ C * ‖z‖
have h₁ : ∀ (z : E), norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) z : Fₗ) ≤ c * (‖k‖ / r) * ‖z‖
Tactic: use c * (‖k‖ / r)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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‖
have 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‖
Tactic: refine bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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 * (‖k‖ / r) * ‖x‖
have h₁ : 0 ≤ c
Tactic: calc
    ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
    _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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
⊢ norm.{u_6} (E := Fₗ) ((f : (a : E) → Fₗ) x : Fₗ) ≤ c * (‖k‖ / r) * ‖x‖
have h₂ : 1 ≤ ‖x‖ * ‖k‖ / r
Tactic: calc
    ‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
    _ ≤ c * (‖x‖ * ‖k‖ / r) := le_mul_of_one_le_right ?_ ?_
    _ = _ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
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
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
have hko₁ : r ≤ ‖x‖ * ‖k‖
Tactic: rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko
Cleared hypotheses: hko, hxo
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
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)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_4, u_5} (α := E) (β := F) K (⇑f : (a : E) → F)
have 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)
Tactic: rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩