-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem IsQuotient.norm_lift {f : NormedAddGroupHom M N} (hquot : IsQuotient f) {ε : ℝ} (hε : 0 < ε)
    (n : N) : ∃ m : M, f m = n ∧ ‖m‖ < ‖n‖ + ε

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑f.ker) + ε
⊢ ‖m + x‖ < ‖f m‖ + ε

Tactic:
rwa [hquot.norm]

Result:
no goals

Proof state:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Tactic:
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
  rw [Set.image_nonempty]
  exact ⟨0, f.ker.zero_mem⟩

Result:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑f.ker) + ε
⊢ f (m + x) = f m

Tactic:
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]

Result:
no goals

Proof state:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Tactic:
rcases Real.lt_sInf_add_pos nonemp hε
  with ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩

Result:
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 : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑f.ker) + ε
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty

Tactic:
rw [Set.image_nonempty]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty

Proof state:
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 : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' => ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑f.ker) + ε
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Tactic:
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by
  rwa [hquot.norm]⟩

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ m, f m = n ∧ ‖m‖ < ‖n‖ + ε

Tactic:
obtain ⟨m, rfl⟩ := hquot.surjective n

Result:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, f m_1 = f m ∧ ‖m_1‖ < ‖f m‖ + ε

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ (↑f.ker).Nonempty

Tactic:
exact ⟨0, f.ker.zero_mem⟩

Result:
no goals