case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ m, ↑f m = n ∧ ‖m‖ < ‖n‖ + ε
obtain ⟨m, rfl⟩ := hquot.surjective n
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
  rw [Set.nonempty_image_iff]
  exact ⟨0, f.ker.zero_mem⟩
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
rcases Real.lt_sInf_add_pos nonemp hε
  with ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
no goals
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by
  rwa [hquot.norm]⟩
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ↑(ker f)
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
rw [Set.nonempty_image_iff]
no goals
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ↑(ker f)
exact ⟨0, f.ker.zero_mem⟩
no goals
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ↑f (m + x) = ↑f m
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
no goals
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ‖m + x‖ < ‖↑f m‖ + ε
rwa [hquot.norm]