awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst_7 : DistribSMul 𝕜' F
inst_8 : SMulCommClass 𝕜₂ 𝕜' F
inst_9 : SeminormedAddCommGroup 𝕜'
inst_10 : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x : E
grw : ‖HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)‖ ≤ ‖c‖ * ‖f‖ * ‖x‖
grw₁ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
⊢ Norm.norm.{u_5} (E := F) ((c • f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
have grw₂ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * (‖f‖ * ‖x‖)
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst_7 : DistribSMul 𝕜' F
inst_8 : SMulCommClass 𝕜₂ 𝕜' F
inst_9 : SeminormedAddCommGroup 𝕜'
inst_10 : IsBoundedSMul 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x : E
grw : ‖HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)‖ ≤ ‖c‖ * ‖f‖ * ‖x‖
grw₁ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
grw₂ : ‖c‖ * Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * (‖f‖ * ‖x‖)
⊢ Norm.norm.{u_5} (E := F) ((c • f : (a : E) → F) x : F) ≤ ‖c‖ * ‖f‖ * ‖x‖
have grw₃ : ‖c‖ * (‖f‖ * ‖x‖) ≤ ‖c‖ * (‖f‖ * ‖x‖)
Tactic: grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
have rw₃ : ‖f.1 + -f.2‖ = ‖f.1 + -f.2‖
Tactic: rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖-f.1 + f.2‖ < r})
have A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
Tactic: have A (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)) : ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by
    rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖-f.1 + f.2‖ < r})
have simp : Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
  (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})
Tactic: simp only [A]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})
have refine_1 : ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
Tactic: refine ContinuousLinearMap.seminorm (σ₁₂ := σ₁₂) (E := E) (F := F) |>.uniformity_eq_of_hasBasis
    (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
⊢ Eq (α := Filter ((E →SL[σ₁₂] F) × (E →SL[σ₁₂] F))) (𝓤 (E →SL[σ₁₂] F))
    (⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F) | ‖f.1 - f.2‖ < r})
have refine_2 : ∀ (x : Set E × ℝ) (s : Set E) (r : ℝ),
  IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2 →
    ∀ (hs : IsVonNBounded 𝕜 (s, r).1) (hr : 0 < (s, r).2),
      ∃ r_1 > 0,
        Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
          {f : E →SL[σ₁₂] F |
            ∀ x ∈ (s, r).1,
              Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
Tactic: refine ContinuousLinearMap.seminorm (σ₁₂ := σ₁₂) (E := E) (F := F) |>.uniformity_eq_of_hasBasis
    (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
have refine_1 : ∀ (c : 𝕜) (hc : 1 < ‖c‖),
  ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
Tactic: rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (r : ℝ), Membership.mem (γ := Filter (E →SL[σ₁₂] F)) (𝓝 0) (Seminorm.closedBall ContinuousLinearMap.seminorm 0 r)
have refine_1 : (IsVonNBounded.{u_1, u_4} 𝕜 (E := E) (closedBall 0 1, closedBall 0 1).1 ∧
    Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1, closedBall 0 1).2) ∧
  Subset (α := Set (E →SL[σ₁₂] F))
    {f : E →SL[σ₁₂] F |
      ∀ (x : E),
        Membership.mem (γ := Set E) (closedBall 0 1, closedBall 0 1).1 x →
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 1, closedBall 0 1).2 ((f : (a : E) → F) x : F)}
    (Seminorm.closedBall ContinuousLinearMap.seminorm 0 ‖c‖)
Tactic: refine ⟨‖c‖, ContinuousLinearMap.hasBasis_nhds_zero.mem_iff.2
      ⟨(closedBall 0 1, closedBall 0 1), ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
⊢ (IsVonNBounded.{u_1, u_4} 𝕜 (E := E) (closedBall 0 1, closedBall 0 1).1 ∧
      Membership.mem (γ := Filter F) (𝓝 0) (closedBall 0 1, closedBall 0 1).2) ∧
    Subset (α := Set (E →SL[σ₁₂] F))
      {f : E →SL[σ₁₂] F |
        ∀ (x : E),
          Membership.mem (γ := Set E) (closedBall 0 1, closedBall 0 1).1 x →
            Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 1, closedBall 0 1).2
              ((f : (a : E) → F) x : F)}
      (Seminorm.closedBall ContinuousLinearMap.seminorm 0 ‖c‖)
have refine_1 : ∀ (f : E →SL[σ₁₂] F), (∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1) → ‖f‖ ≤ ‖c‖
Tactic: suffices ∀ f : E →SL[σ₁₂] F, (∀ x, ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) → ‖f‖ ≤ ‖c‖ by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, subset_def] using this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ 1
⊢ ‖f‖ ≤ ‖c‖
have refine_1 : ∀ (x : E) (hcx : 1 / ‖c‖ ≤ ‖x‖) (hx : ‖x‖ < 1), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖c‖ * ‖x‖
Tactic: refine opNorm_le_of_shell (f := f) one_pos (norm_nonneg c) hc fun x hcx hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
have refine_2 : ∀ (ε : ℝ) (hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε),
  ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
Tactic: rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
have refine_2 : ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hδ : ε * δ < (s, r).2),
  ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
Tactic: rcases exists_pos_mul_lt hr ε with ⟨δ, hδ₀, hδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 r_1)
      {f : E →SL[σ₁₂] F |
        ∀ x ∈ (s, r).1,
          Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)}
have refine_2 : ∀ (f : E →SL[σ₁₂] F) (hf : Membership.mem (γ := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 δ) f)
  (x : E) (hx : x ∈ (s, r).1),
  Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)
Tactic: refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
hf : Membership.mem (γ := Set (E →SL[σ₁₂] F)) (Seminorm.ball ContinuousLinearMap.seminorm 0 δ) f
x : E
hx : x ∈ (s, r).1
⊢ Membership.mem.{u_5, u_5} (α := F) (γ := Set F) (closedBall 0 (s, r).2) ((f : (a : E) → F) x : F)
have refine_2 : ∀ (hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ),
  Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r
Tactic: simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : Set E × ℝ
s : Set E
r : ℝ
h : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε * δ < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ
⊢ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r
have refine_2 : ∀ (hδ : δ * ε < (s, r).2) (f : E →SL[σ₁₂] F) (x : E) (hx : x ∈ (s, r).1)
  (hf : (ContinuousLinearMap.seminorm : (a : E →SL[σ₁₂] F) → ℝ) f < δ),
  Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ r
Tactic: rw [mul_comm] at hδ
Cleared hypotheses: hδ, f, x, hx, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : SeminormedAddCommGroup G
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NontriviallyNormedField 𝕜₃
inst_6 : NormedSpace 𝕜 E
inst_7 : NormedSpace 𝕜₂ F
inst_8 : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomIsometric σ₁₂
inst_11 : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * ‖f‖ * ‖x‖
have rw : Norm.norm.{u_7} (E := G) ((h ∘SL f : (a : E) → G) x : G) ≤ ‖h‖ * (‖f‖ * ‖x‖)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ enorm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ₑ * ‖x‖ₑ
have simp_rw : ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal ‖f‖ * ENNReal.ofReal ‖x‖
Tactic: simp_rw [← ofReal_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal ‖f‖ * ENNReal.ofReal ‖x‖
have rw : ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal (‖f‖ * ‖x‖)
Tactic: rw [← ENNReal.ofReal_mul (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
⊢ ENNReal.ofReal (Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)) ≤ ENNReal.ofReal (‖f‖ * ‖x‖)
have h : Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
⊢ ‖f‖ = a
have obtain : ∀ (x : E) (hx : ‖x‖ ≠ 0), ‖f‖ = a
Tactic: obtain ⟨x, hx⟩ := exists_norm_ne_zero E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : ‖x‖ ≠ 0
⊢ ‖f‖ = a
have hx₁ : 0 < ‖x‖
Tactic: replace hx : 0 < ‖x‖ := lt_of_le_of_ne' (norm_nonneg _) hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
⊢ ‖f‖ = a
have ha : 0 ≤ a
Tactic: have ha : 0 ≤ a := by simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ ‖f‖ = a
have apply : a ≤ ‖f‖
Tactic: apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
M : ι → Type u_10
inst_4 : (i : ι) → SeminormedAddCommGroup (M i)
inst_5 : (i : ι) → NormedSpace.{u_1, u_10} 𝕜 (M i)
C : ℝ
L : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_10} (RingHom.id 𝕜) E (M i)
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
⊢ ‖pi (φ := M) L‖ ≤ C
have refine : ∀ (x : E), norm (E := (i : ι) → M i) ((pi (φ := M) L : (a : E) → (i : ι) → M i) x : (i : ι) → M i) ≤ C * ‖x‖
Tactic: refine opNorm_le_bound _ hC (fun x ↦ ?_)