awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
C : ℝ
C0 : C ≥ 0
g : (y : F) → E
hg : ∀ (y : F), dist ((f : (a : E) → F) (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : (y : F) → F := fun (y : F) ↦ HSub.hSub (β := F) y ((f : (a : E) → F) (g y) : F)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : (n : ℕ) → E := fun (n : ℕ) ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), (f : (a : E) → F) (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto.{0, u_4} (β := F) (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 ((f : (a : E) → F) x) : Filter F)
L₂ : Tendsto (fun (n : ℕ) ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : (f : (a : E) → F) x = y - 0
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
have feq₁ : (f : (a : E) → F) x = y
Tactic: rw [sub_zero] at feq
Cleared hypotheses: feq
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) '' s)
have rcases : ∀ (C : ℝ) (Cpos : C > 0) (hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) '' s)
Tactic: rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) '' s)
have refine : ∀ (y : F) (yfs : Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) y), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
Tactic: refine isOpen_iff.2 fun y yfs => ?_
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
yfs : Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) y
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
have rcases : ∀ (x : E) (xs : x ∈ s) (fxy : (f : (a : E) → F) x = y), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
Tactic: rcases yfs with ⟨x, xs, fxy⟩
Cleared hypotheses: yfs
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
have rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ s), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
Tactic: rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
have refine : ∀ (z : F) (hz : z ∈ ball y (ε / C)), Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
Tactic: refine ⟨ε / C, div_pos εpos Cpos, fun z hz => ?_⟩
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
have rcases : ∀ (w : E) (wim : (f : (a : E) → F) w = z - y) (wnorm : ‖w‖ ≤ C * ‖z - y‖),
  Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
Tactic: rcases hC (z - y) with ⟨w, wim, wnorm⟩
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ (f : (a : E) → F) (x + w) = z
have rw : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) w : F) = z
Tactic: rw [f.map_add, wim, fxy, add_sub_cancel]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
rw : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) w : F) = z
⊢ (f : (a : E) → F) (x + w) = z
have rw₁ : HAdd.hAdd (α := F) ((f : (a : E) → F) x : F) (z - y) = z
Tactic: rw [f.map_add, wim, fxy, add_sub_cancel]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
rw : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) w : F) = z
rw₁ : HAdd.hAdd (α := F) ((f : (a : E) → F) x : F) (z - y) = z
⊢ (f : (a : E) → F) (x + w) = z
have rw₂ : y + (z - y) = z
Tactic: rw [f.map_add, wim, fxy, add_sub_cancel]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
rw : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) w : F) = z
rw₁ : HAdd.hAdd (α := F) ((f : (a : E) → F) x : F) (z - y) = z
rw₂ : y + (z - y) = z
⊢ (f : (a : E) → F) (x + w) = z
have rw₃ : z = z
Tactic: rw [f.map_add, wim, fxy, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
have this : (f : (a : E) → F) (x + w) = z
Tactic: have : f (x + w) = z := by rw [f.map_add, wim, fxy, add_sub_cancel]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : (f : (a : E) → F) (x + w) = z
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
have rw : Membership.mem.{u_4, u_4} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) (x + w) : F)
Tactic: rw [← this]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : (f : (a : E) → F) (x + w) = z
⊢ C * ‖z - y‖ < C * (ε / C)
have apply : ‖z - y‖ < ε / C
Tactic: apply mul_lt_mul_of_pos_left _ Cpos
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : (f : (a : E) → F) (x + w) = z
⊢ ‖z - y‖ < ε / C
have rwa : ∀ (hz : dist z y < ε / C) (w : E) (wim : (f : (a : E) → F) w = z - y) (wnorm : ‖w‖ ≤ C * ‖z - y‖)
  (this : (f : (a : E) → F) (x + w) = z), ‖z - y‖ < ε / C
Tactic: rwa [mem_ball, dist_eq_norm] at hz
Cleared hypotheses: hz, w, wim, wnorm, this
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : (f : (a : E) → F) (x + w) = z
rwa :
  ∀ (hz : dist z y < ε / C) (w : E) (wim : (f : (a : E) → F) w = z - y) (wnorm : ‖w‖ ≤ C * ‖z - y‖)
    (this : (f : (a : E) → F) (x + w) = z), ‖z - y‖ < ε / C
⊢ ‖z - y‖ < ε / C
have rwa₁ : ∀ (hz : ‖z - y‖ < ε / C) (w : E) (wim : (f : (a : E) → F) w = z - y) (wnorm : ‖w‖ ≤ C * ‖z - y‖)
  (this : (f : (a : E) → F) (x + w) = z), ‖z - y‖ < ε / C
Tactic: rwa [mem_ball, dist_eq_norm] at hz
Cleared hypotheses: hz, w, wim, wnorm, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : (f : (a : E) → F) x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : (f : (a : E) → F) w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : (f : (a : E) → F) (x + w) = z
⊢ Membership.mem.{u_4, u_4} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) (x + w) : F)
have this₁ : x + w ∈ ball x ε
Tactic: have : x + w ∈ ball x ε :=
    calc
      dist (x + w) x = ‖w‖ := by
        simp
      _ ≤ C * ‖z - y‖ := wnorm
      _ < C * (ε / C) := by
        apply mul_lt_mul_of_pos_left _ Cpos
        rwa [mem_ball, dist_eq_norm] at hz
      _ = ε := mul_div_cancel₀ _ (ne_of_gt Cpos)
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
have choose : ∀ (C : ℝ) (hC : C > 0) (fsymm : (y : F) → E) (h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖),
  ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
Tactic: choose C hC fsymm h using
    exists_preimage_norm_le _ (LinearMap.range_eq_top.1 hsurj)
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
C : ℝ
hC : C > 0
fsymm : (y : F) → E
h : ∀ (y : F), (f : (a : E) → F) (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ ∃ (fsymm : f.NonlinearRightInverse), 0 < fsymm.nnnorm
have h₁ : 0 <
  NonlinearRightInverse.nnnorm.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) (f := f)
    { toFun := fsymm, nnnorm := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C sorry, bound' := sorry, right_inv' := sorry :
      f.NonlinearRightInverse }
Tactic: use {
      toFun := fsymm
      nnnorm := ⟨C, hC.lt.le⟩
      bound' := fun y => (h y).2
      right_inv' := fun y => (h y).1 }
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f : E →ₛₗ[σ] F).range = ⊤
⊢ 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
have rw : 0 < (Classical.choose (p := fun (x : f.NonlinearRightInverse) ↦ 0 < x.nnnorm) sorry).nnnorm
Tactic: rw [nonlinearRightInverseOfSurjective]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e : (a : E) → F)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e.symm : (a : F) → E)
have rw : ∀ (s : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e.symm : (a : F) → E) ⁻¹' s)
Tactic: rw [continuous_def]
-- 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
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑e : (a : E) → F)
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e.symm : (a : F) → E) ⁻¹' s)
have rw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑e : (a : E) → F) '' s)
Tactic: rw [← e.image_eq_preimage_symm]