awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
F : Type u_5
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
g : E →ₗ[𝕜] F
hg :
  ∀ (u : ℕ → E) (x : E) (y : F),
    Tendsto u atTop (𝓝 x) → Tendsto ((⇑g : (a : E) → F) ∘ u) atTop (𝓝 y) → y = (g : (a : E) → F) x
⊢ (↑(ofSeqClosedGraph hg) : E →ₗ[𝕜] F) = g
have h : ∀ (x : E), Eq.{u_5 + 1} (α := F) (((↑(ofSeqClosedGraph hg) : E →ₗ[𝕜] F) : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
have refine : ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
Tactic: refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
refine :
  ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
have refine₁ : ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
  ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
Tactic: refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
refine :
  ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
refine₁ :
  ∀ (h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)),
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
⊢ Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
      ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
have refine₂ : ((↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)) →
  ∀ (hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤) (c : ℝ≥0)
    (hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)),
    Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
Tactic: refine ⟨fun h ↦ ⟨?eq_top, ?anti⟩, fun ⟨hd, c, hf⟩ ↦ ⟨hf.injective, ?surj⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
have refine_1 : (↑f : E →ₛₗ[σ] F).ker = ⊥
Tactic: refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h : Bijective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
refine_1 : (↑f : E →ₛₗ[σ] F).ker = ⊥
⊢ ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
have refine_2 : (↑f : E →ₛₗ[σ] F).range = ⊤
Tactic: refine ⟨_, ContinuousLinearEquiv.ofBijective f ?_ ?_ |>.antilipschitz⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have rwa : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
Tactic: rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
rwa : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have rwa₁ : (↑f : E →ₛₗ[σ] F).range = ⊤
Tactic: rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have case : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
Tactic: case surj => rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_4 : RingHomInvPair σ σ'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : CompleteSpace E
inst_8 : CompleteSpace F
inst_9 : RingHomInvPair σ' σ
inst_10 : RingHomIsometric σ
inst_11 : RingHomIsometric σ'
f : E →SL[σ] F
h :
  (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤ ∧
    ∃ (c : ℝ≥0), AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
hd : (↑f : E →ₛₗ[σ] F).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith.{u_3, u_4} (α := E) (β := F) c (⇑f : (a : E) → F)
case : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑(↑f : E →ₛₗ[σ] F) : (a : E) → F)
⊢ Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have case₁ : (↑f : E →ₛₗ[σ] F).range = ⊤
Tactic: case surj => rwa [← f.coe_coe, ← LinearMap.range_eq_top, ← closed_range_of_antilipschitz hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BanachSteinhaus (goal)
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
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_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
⊢ ∃ (C' : ℝ), ∀ (i : ι), ‖g i‖ ≤ C'
have rw : UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
Tactic: rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BanachSteinhaus (goal)
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
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_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), ∃ (C : ℝ), ∀ (i : ι), norm.{u_2} (E := F) ((g i : (a : E) → F) x : F) ≤ C
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
have refine : ∀ (x : Fin 1) (x : E),
  BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))
Tactic: refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BanachSteinhaus (goal)
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
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_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
⊢ LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑‖g i‖₊ : ℝ≥0∞)) ∞
have rw : UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
Tactic: rw [show ((⨆ i, ↑‖g i‖₊) < ∞) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 8 2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BanachSteinhaus (goal)
Goal:
E : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
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_5
inst_7 : CompleteSpace E
g : ι → E →SL[σ₁₂] F
h : ∀ (x : E), LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(nnnorm.{u_2} (E := F) ((g i : (a : E) → F) x : F)) : ℝ≥0∞)) ∞
⊢ UniformEquicontinuous.{u_5, u_2, u_1} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ g)
have refine : ∀ (x : Fin 1) (x : E),
  BddAbove (α := ℝ) (range fun (i : ι) ↦ (normSeminorm 𝕜₂ F : (a : F) → ℝ) ((g i : (a : E) → F) x : F))
Tactic: refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
⊢ ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F) ↔
    Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have refine : ∀ (h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)),
  Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
Tactic: refine ⟨fun h ↦ ?_, by simp_all⟩
-- 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
have rw : Subset.{u_5} (α := Set F) (ball 0 r)
  (Set.range.{u_5, u_4 + 1} (ι := E)
    (⇑(↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F) : (a : E) → F))
Tactic: rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe]
-- 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)
⊢ Subset.{u_5} (α := Set F) (ball 0 r)
    (Set.range.{u_5, u_4 + 1} (ι := E)
      (⇑(↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F) : (a : E) → F))
have simp_rw : ∀ (x : F),
  Membership.mem (γ := Set F) (ball 0 r) x →
    Membership.mem (γ := Submodule 𝕜₂ F)
      (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x
Tactic: simp_rw [← LinearMap.coe_range, Set.subset_def, SetLike.mem_coe] at 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
h_1 : Membership.mem (γ := Set F) (ball 0 r) x_1
⊢ Membership.mem (γ := Submodule 𝕜₂ F)
    (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) x_1
have rw : Membership.mem (γ := Submodule 𝕜₂ F)
  (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) (x_1 + x)
Tactic: rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
inst_8 : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_2 ∈ ball x r, Membership.mem (γ := Set F) (Set.range.{u_5, u_4 + 1} (ι := E) (⇑f : (a : E) → F)) x_2
x_1 : F
h_1 : Membership.mem (γ := Set F) (ball 0 r) x_1
⊢ Membership.mem (γ := Submodule 𝕜₂ F)
    (LinearMap.range (↑f : [inst_9 : FunLike 𝓕 E F] → [SemilinearMapClass 𝓕 σ₁₂ E F] → E →ₛₗ[σ₁₂] F)) (x_1 + x)
have a : x_1 + x ∈ ball x r
Tactic: apply h
-- 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
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
⊢ sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F') ↔
    Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')
have refine : ∀ (h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')),
  Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')
Tactic: refine ⟨fun h ↦ ?_, by simp_all⟩
-- 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
F' : Type u_9
𝓕' : Type u_10
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace ℝ F'
inst_5 : Nontrivial F'
τ : 𝕜 →+* ℝ
inst_6 : FunLike 𝓕' E F'
inst_7 : SemilinearMapClass 𝓕' τ E F'
inst_8 : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F')
⊢ Function.Surjective.{u_4 + 1, u_9 + 1} (α := E) (β := F') (⇑f : (a : E) → F')
have grw : Convex.{0, u_9} ℝ (E := F') (Set.range.{u_9, u_4 + 1} (ι := E) (⇑f : (a : E) → F'))
Tactic: grw [← (closedBall_subset_range_iff_surjective x hr), ← convexHull_sphere_eq_closedBall x hr.le,
    convexHull_mono h, (convexHull_eq_self (𝕜 := ℝ) (s := Set.range ↑f)).mpr]
-- 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
𝓕 : Type u_8
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜₂
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : FunLike 𝓕 E F
inst_7 : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)
x : E
hx : ‖x‖ = 0
⊢ norm.{u_5} (E := F) ((f : (a : E) → F) x : F) = 0
have rw : ∀ (hx : 0 ⤳ x), Specializes.{u_5} (X := F) ((f : (a : E) → F) 0 : F) ((f : (a : E) → F) x : F)
Tactic: rw [← mem_closure_zero_iff_norm, ← specializes_iff_mem_closure, ← map_zero f] at *
Cleared hypotheses: 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 σ₁₂
f : E →SL[σ₁₂] F
⊢ IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖} ‖f‖
have refine : IsClosed (X := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}
Tactic: refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow
-- 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
⊢ IsClosed (X := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : E), Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ c * ‖x‖}
have simp : IsClosed (X := ℝ) ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})
Tactic: simp only [setOf_and, setOf_forall]
-- 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
⊢ IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})
have refine_1 : ∀ (x : E), Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: refine isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_
-- 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
refine_1 : ∀ (x : E), Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ Norm.norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩ ⋂ (i : E), {x : ℝ | Norm.norm.{u_5} (E := F) ((f : (a : E) → F) i : F) ≤ x * ‖i‖})
have refine_2 : ∀ (x : E), Continuous (Y := ℝ) fun (x_1 : ℝ) ↦ x_1 * ‖x‖
Tactic: refine isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_
-- 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 y : E
⊢ dist.{u_5} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) ≤ ‖f‖ * dist x y
have simp_rw : ‖HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)‖ ≤ ‖f‖ * ‖x - y‖
Tactic: simp_rw [dist_eq_norm, ← map_sub, f.le_opNorm]