M : Type u_1
N : Type ?u.27150
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ infDist x (↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
M : Type u_1
N : Type ?u.27150
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ ‖↑x‖ = infDist x ↑S
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.subLeft x).isometry,
  IsometryEquiv.subLeft_apply, sub_zero, ← IsometryEquiv.preimage_symm]
case e_s.h
M : Type u_1
N : Type ?u.27150
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ y ∈ ↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S
M : Type u_1
N : Type ?u.27150
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ infDist x (↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
congr 1 with y
no goals
case e_s.h
M : Type u_1
N : Type ?u.27150
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ y ∈ ↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S
simp only [mem_preimage, IsometryEquiv.subLeft_symm_apply, mem_setOf_eq, QuotientAddGroup.eq,
  neg_add, neg_neg, neg_add_cancel_right, SetLike.mem_coe]