case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}

M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
have : ∀ ε : ℝ, mk '' ball (0 : M) ε = { x : M ⧸ S | ‖x‖ < ε }
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (Filter.map mk (𝓝 0)) (fun ε => 0 < ε) fun x => mk '' ball 0 x
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
rw [← mk_zero, nhds_eq, ← funext this]
no goals
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (Filter.map mk (𝓝 0)) (fun ε => 0 < ε) fun x => mk '' ball 0 x
exact .map _ Metric.nhds_basis_ball
case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}
case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1, x_1 ∈ {x | ‖x‖ < ε} ∧ ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}
rw [ball_zero_eq, mem_setOf_eq, norm_lt_iff, mem_image]
no goals
case this
M : Type u_1
N : Type ?u.386793
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1, x_1 ∈ {x | ‖x‖ < ε} ∧ ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
exact exists_congr fun _ ↦ and_comm