awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
⊢ ∃ (x : E), (f : (a : E) → F) x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
exact ⟨x, feq, x_ineq⟩
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
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)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) '' s)

Tactic:
rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩

Premises used: ContinuousLinearMap.exists_preimage_norm_le
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)

Tactic:
isOpen_iff.2 fun y yfs => ?_

Premises used: Iff.mpr, Metric.isOpen_iff
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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‖
refine :
  ∀ (y : F) (yfs : Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) y), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) '' s)

Tactic:
refine isOpen_iff.2 fun y yfs => ?_

Premises used: Iff.mpr, Metric.isOpen_iff
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
rcases : ∀ (x : E) (xs : x ∈ s) (fxy : (f : (a : E) → F) x = y), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s

Tactic:
rcases yfs with ⟨x, xs, fxy⟩
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ s), ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s

Tactic:
rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩

Premises used: Metric.isOpen_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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

Tactic:
⟨ε / C, div_pos εpos Cpos, fun z hz => ?_⟩

Premises used: HDiv.hDiv, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
refine : ∀ (z : F) (hz : z ∈ ball y (ε / C)), Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z
⊢ ∃ ε > 0, ball y ε ⊆ (⇑f : (a : E) → F) '' s

Tactic:
refine ⟨ε / C, div_pos εpos Cpos, fun z hz => ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
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
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z

Tactic:
rcases hC (z - y) with ⟨w, wim, wnorm⟩

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
rw₃ rw₄ : z = z
⊢ (f : (a : E) → F) (x + w) = z

Tactic:
rw [f.map_add, wim, fxy, add_sub_cancel]

Premises used: ContinuousLinearMap.map_add, add_sub_cancel
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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

Tactic:
have : f (x + w) = z := by rw [f.map_add, wim, fxy, add_sub_cancel]
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
rw : Membership.mem.{u_4, u_4} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) (x + w) : F)
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) z

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
⊢ dist (x + w) x = ‖w‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
apply : ‖z - y‖ < ε / C
⊢ C * ‖z - y‖ < C * (ε / C)

Tactic:
apply mul_lt_mul_of_pos_left _ Cpos

Premises used: mul_lt_mul_of_pos_left
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
rwa₁ rwa₂ rwa₃ 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
⊢ ‖z - y‖ < ε / C

Tactic:
rwa [mem_ball, dist_eq_norm] at hz

Premises used: dist_eq_norm, Metric.mem_ball
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
⊢ 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)
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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_1 : (f : (a : E) → F) (x + w) = z
this : x + w ∈ ball x ε
⊢ Membership.mem.{u_4, u_4} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) (x + w) : F)

Tactic:
Set.mem_image_of_mem _ (hε this)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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_1 : (f : (a : E) → F) (x + w) = z
this : x + w ∈ ball x ε
⊢ Membership.mem.{u_4, u_4} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) (x + w) : F)

Tactic:
exact Set.mem_image_of_mem _ (hε this)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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)
⊢ IsQuotientMap.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)

Tactic:
(f.isOpenMap surj).isQuotientMap f.continuous surj

Premises used: IsOpenMap.isQuotientMap, ContinuousLinearMap.continuous, ContinuousLinearMap.isOpenMap
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
P : Type u_6
Q : Type u_7
inst_7 : MetricSpace P
inst_8 : NormedAddTorsor E P
inst_9 : MetricSpace Q
inst_10 : NormedAddTorsor F Q
f : P →ᵃ[𝕜] Q
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : P) → Q)
surj : Surjective.{u_6 + 1, u_7 + 1} (α := P) (β := Q) (⇑f : (a : P) → Q)
⊢ IsOpenMap.{u_6, u_7} (X := P) (Y := Q) (⇑f : (a : P) → Q)

Tactic:
AffineMap.isOpenMap_linear_iff.mp <|
    ContinuousLinearMap.isOpenMap { f.linear with cont := AffineMap.continuous_linear_iff.mpr hf }
      (f.linear_surjective_iff.mpr surj)

Premises used: Iff.mpr, ContinuousLinearMap.mk, AffineMap.linear_surjective_iff, AffineMap.isOpenMap_linear_iff, AffineMap.linear, Iff.mp, AffineMap.continuous_linear_iff, ContinuousLinearMap.isOpenMap
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
hsurj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set F
⊢ Eq.{u_3 + 1} (α := Set E) (interior ((⇑f : (a : E) → F) ⁻¹' s)) ((⇑f : (a : E) → F) ⁻¹' interior s)

Tactic:
((f.isOpenMap hsurj).preimage_interior_eq_interior_preimage f.continuous s).symm

Premises used: IsOpenMap.preimage_interior_eq_interior_preimage, ContinuousLinearMap.continuous, ContinuousLinearMap.isOpenMap, Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
hsurj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set F
⊢ Eq.{u_3 + 1} (α := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : E) → F) ⁻¹' s))
    ((⇑f : (a : E) → F) ⁻¹' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
((f.isOpenMap hsurj).preimage_closure_eq_closure_preimage f.continuous s).symm

Premises used: IsOpenMap.preimage_closure_eq_closure_preimage, ContinuousLinearMap.continuous, ContinuousLinearMap.isOpenMap, Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Banach
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
hsurj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
s : Set F
⊢ Eq.{u_3 + 1} (α := Set E) (frontier ((⇑f : (a : E) → F) ⁻¹' s)) ((⇑f : (a : E) → F) ⁻¹' frontier s)

Tactic:
((f.isOpenMap hsurj).preimage_frontier_eq_frontier_preimage f.continuous s).symm

Premises used: ContinuousLinearMap.continuous, ContinuousLinearMap.isOpenMap, Eq.symm, IsOpenMap.preimage_frontier_eq_frontier_preimage