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 : 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
⊢ ‖f‖₊ = sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}
have a : (↑‖f‖₊ : ℝ) = (↑(sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}) : ℝ)
Tactic: ext
-- 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 : 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
⊢ (↑‖f‖₊ : ℝ) = (↑(sInf {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}) : ℝ)
have a : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf
    {x : ℝ |
      ∃ (h : 0 ≤ x),
        Membership.mem (γ := Set ℝ≥0) {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊}
          (NNReal.mk x h)})
Tactic: rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]
-- 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 : 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
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
have a : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf
    {x : ℝ |
      ∃ (h : 0 ≤ x),
        Membership.mem (γ := Set ℝ≥0)
          {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
          (NNReal.mk x sorry)})
Tactic: simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
-- 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 : 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
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
            (NNReal.mk x ⋯)})
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
have a₁ : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf
    {x : ℝ |
      ∃ (h : 0 ≤ x),
        Membership.mem (γ := Set ℝ≥0)
          {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑c : ℝ) * (↑‖x‖₊ : ℝ)}
          (NNReal.mk x sorry)})
Tactic: simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
-- 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 : 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
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
            (NNReal.mk x ⋯)})
a₁ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑c : ℝ) * (↑‖x‖₊ : ℝ)}
            (NNReal.mk x ⋯)})
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
have a₂ : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf
    {x : ℝ |
      ∃ (h : 0 ≤ x),
        Membership.mem (γ := Set ℝ≥0)
          {c : ℝ≥0 | ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑c : ℝ) * ‖x‖} (NNReal.mk x sorry)})
Tactic: simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
-- 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 : 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
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
            (NNReal.mk x ⋯)})
a₁ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑c : ℝ) * (↑‖x‖₊ : ℝ)}
            (NNReal.mk x ⋯)})
a₂ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑c : ℝ) * ‖x‖} (NNReal.mk x ⋯)})
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
have a₃ : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf
    {x : ℝ |
      ∃ (h : 0 ≤ x),
        ∀ (x_1 : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x_1 : F) ≤ (↑(NNReal.mk x sorry) : ℝ) * ‖x_1‖})
Tactic: simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
-- 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 : 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
a :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑(c * ‖x‖₊) : ℝ)}
            (NNReal.mk x ⋯)})
a₁ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), (↑(nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) : ℝ) ≤ (↑c : ℝ) * (↑‖x‖₊ : ℝ)}
            (NNReal.mk x ⋯)})
a₂ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑c : ℝ) * ‖x‖} (NNReal.mk x ⋯)})
a₃ :
  Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          ∀ (x_1 : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x_1 : F) ≤ (↑(NNReal.mk x ⋯) : ℝ) * ‖x_1‖})
⊢ Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
    (sInf
      {x : ℝ |
        ∃ (h : 0 ≤ x),
          Membership.mem (γ := Set ℝ≥0)
            {c : ℝ≥0 | ∀ (x : E), nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖₊} (NNReal.mk x h)})
have a₄ : Eq (α := ℝ) (sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖})
  (sInf {x : ℝ | ∃ (_ : 0 ≤ x), ∀ (x_1 : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x_1 : F) ≤ x * ‖x_1‖})
Tactic: simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
    exists_prop]
-- 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 : 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
M : ℝ≥0
hM : ∀ (x : E), ‖x‖₊ ≠ 0 → nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ M * ‖x‖₊
x : E
hx : ‖x‖ ≠ 0
⊢ ‖x‖₊ ≠ 0
have rwa : (↑‖x‖₊ : ℝ) ≠ 0
Tactic: rwa [← NNReal.coe_ne_zero]
-- 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 : 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 : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ C
x : E
hx : ‖x‖ = 1
⊢ ‖x‖₊ = 1
have rwa : (↑‖x‖₊ : ℝ) = 1
Tactic: rwa [← NNReal.coe_eq_one]
-- 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 : 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‖
⊢ ∃ (x : E), r * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have lift : ∀ (r : ℝ≥0) (hr : (↑r : ℝ) < ‖f‖), ∃ (x : E), (↑r : ℝ) * ‖x‖ < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: lift r to ℝ≥0 using hr₀
Cleared hypotheses: r, hr₀, 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 σ₁₂
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 : ∀ (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)
Tactic: obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_opNNNorm hr
-- 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
r : ℝ≥0
hr : r < ‖f‖₊
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)
have hy' : ‖y‖₊ ≠ 0
Tactic: have hy' : ‖y‖₊ ≠ 0 :=
    nnnorm_ne_zero_iff.2 fun heq => by
      simp [heq, nnnorm_zero, map_zero] at hy
-- 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
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
hy' : ‖y‖₊ ≠ 0
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hfy : nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) ≠ 0
Tactic: have hfy : ‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'
-- 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
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
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have hy₁ : 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
Cleared hypotheses: hy, hy', hfy
-- 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
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
⊢ ∃ (x : E), ‖x‖₊ < 1 ∧ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy
-- 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
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)
have refine : r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
Tactic: refine ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, ?_⟩
-- 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
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‖₊⁻¹
⊢ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
have rwa : r < ‖HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) ((f : (a : E) → F) y : F)‖₊
Tactic: rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv,
    RingHomIsometric.nnnorm_map]
-- 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
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)‖₊
⊢ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
have rwa₁ : r < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) * nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F)
Tactic: rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv,
    RingHomIsometric.nnnorm_map]
-- 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
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)
⊢ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
have rwa₂ : r / nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F) < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
Tactic: rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv,
    RingHomIsometric.nnnorm_map]
-- 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
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 : 𝕜₂)
⊢ r < nnnorm.{u_5} (E := F) ((f : (a : E) → F) (k • y) : F)
have rwa₃ : r * (nnnorm.{u_5} (E := F) ((f : (a : E) → F) y : F))⁻¹ < nnnorm.{u_2} (E := 𝕜₂) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
Tactic: rwa [map_smulₛₗ f, nnnorm_smul, ← div_lt_iff₀ hfy.bot_lt, div_eq_mul_inv,
    RingHomIsometric.nnnorm_map]
-- 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
r : ℝ
hr : r < ‖f‖
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have pos : ∀ (hr₀ : r < 0), ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: by_cases hr₀ : r < 0
-- 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
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)
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have neg : ∀ (hr₀ : ¬r < 0), ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: by_cases hr₀ : r < 0
-- 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
r : ℝ
hr : r < ‖f‖
hr₀ : ¬r < 0
⊢ ∃ (x : E), ‖x‖ < 1 ∧ r < Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have 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)
Tactic: lift r to ℝ≥0 using not_lt.1 hr₀
Cleared hypotheses: r, hr, 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 σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun (x : E) ↦ nnnorm.{u_5} (E := F) ((f : (a : E) → F) x : F)) '' ball 0 1) = ‖f‖₊
have 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‖₊
Tactic: refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ((nonempty_ball.mpr zero_lt_one).image _) ?_
    fun ub hub => ?_