no goals
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
rcases mk_surjective x with ⟨x, rfl⟩
no goals
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖
simpa [h] using le_opNorm f x
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖↑(lift S (toAddMonoidHom f) hf) x‖ / ‖f‖
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ / ‖f‖
⊢ False
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖↑(lift S (toAddMonoidHom f) hf) x‖ / ‖f‖
rintro ⟨x, rfl, hx⟩
no goals
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ / ‖f‖
⊢ False
exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)