case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑(mk' S) n = ↑(mk' S) m
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
obtain ⟨n : M, hn : mk' S n = mk' S m, hn' : ‖n‖ < ‖mk' S m‖ + ε⟩ :=
  norm_mk_lt (QuotientAddGroup.mk' S m) hε
case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑(mk' S) n = ↑(mk' S) m
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
erw [eq_comm, QuotientAddGroup.eq] at hn
case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖↑(mk' S) m‖ + ε
case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
use -m + n, hn
no goals
case intro.intro
M : Type u_1
N : Type ?u.220188
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖↑(mk' S) m‖ + ε
rwa [add_neg_cancel_left]