M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ 1 ≤ ‖normedMk S‖
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ‖normedMk S‖ = 1
refine le_antisymm (norm_normedMk_le S) ?_
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ∃ x, 0 < ‖↑x‖

case intro
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖normedMk S‖
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ 1 ≤ ‖normedMk S‖
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖
case intro
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖normedMk S‖ * ‖↑x‖
case intro
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖normedMk S‖
refine (le_mul_iff_one_le_left hx).1 ?_
no goals
case intro
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖normedMk S‖ * ‖↑x‖
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : x ∈ ↑(topologicalClosure S)ᶜ
⊢ 0 < ‖↑x‖
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ∃ x, 0 < ‖↑x‖
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
no goals
M : Type u_1
N : Type ?u.454552
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : x ∈ ↑(topologicalClosure S)ᶜ
⊢ 0 < ‖↑x‖
exact (norm_nonneg _).lt_of_ne' <| mt (quotient_norm_eq_zero_iff S x).1 hx