M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker f)) ≤ ‖m‖
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖↑f m‖ ≤ ‖m‖
rw [hquot.norm]
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))

case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑(ker f)
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker f)) ≤ ‖m‖
apply csInf_le
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
use 0
case h₁.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
rintro _ ⟨m', -, rfl⟩
no goals
case h₁.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'
apply norm_nonneg
no goals
case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑(ker f)
exact ⟨0, f.ker.zero_mem, by simp⟩
no goals
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ (fun m_1 => ‖m + m_1‖) 0 = ‖m‖
simp