[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁴ : PseudoEMetricSpace X
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : IsometricSMul M X
c : Mᵐᵒᵖ
x y : X
⊢ edist ((fun x => c • x) x) ((fun x => c • x) y) = edist x y
[PROOFSTEP]
simpa only [← op_smul_eq_smul] using isometry_smul X c.unop x y
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁶ : PseudoEMetricSpace X
inst✝⁵ : Group G
inst✝⁴ : MulAction G X
inst✝³ : IsometricSMul G X
inst✝² : DivInvMonoid M
inst✝¹ : PseudoEMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a / c) (b / c) = edist a b
[PROOFSTEP]
simp only [div_eq_mul_inv, edist_mul_right]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁶ : PseudoEMetricSpace X
inst✝⁵ : Group G
inst✝⁴ : MulAction G X
inst✝³ : IsometricSMul G X
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist a⁻¹ b⁻¹ = edist a b
[PROOFSTEP]
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_right_inv, one_mul, inv_mul_cancel_right, edist_comm]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁶ : PseudoEMetricSpace X
inst✝⁵ : Group G
inst✝⁴ : MulAction G X
inst✝³ : IsometricSMul G X
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹ y = edist x y⁻¹
[PROOFSTEP]
rw [← edist_inv_inv, inv_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁶ : PseudoEMetricSpace X
inst✝⁵ : Group G
inst✝⁴ : MulAction G X
inst✝³ : IsometricSMul G X
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a / b) (a / c) = edist b c
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, edist_mul_left, edist_inv_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x x_1 => x • x_1) c ⁻¹' ball x r = ball (c⁻¹ • x) r
[PROOFSTEP]
rw [preimage_smul, smul_ball]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x x_1 => x • x_1) c ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
[PROOFSTEP]
rw [preimage_smul, smul_closedBall]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b / a) r
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
[PROOFSTEP]
exact preimage_smul_ball (MulOpposite.op a) b r
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoEMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
[PROOFSTEP]
exact preimage_smul_closedBall (MulOpposite.op a) b r
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a / c) (b / c) = dist a b
[PROOFSTEP]
simp only [div_eq_mul_inv, dist_mul_right]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ nndist (a / c) (b / c) = nndist a b
[PROOFSTEP]
simp only [div_eq_mul_inv, nndist_mul_right]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ dist (a / b) (a / c) = dist b c
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ nndist (a / b) (a / c) = nndist b c
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x x_1 => x • x_1) c ⁻¹' ball x r = ball (c⁻¹ • x) r
[PROOFSTEP]
rw [preimage_smul, smul_ball]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x x_1 => x • x_1) c ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
[PROOFSTEP]
rw [preimage_smul, smul_closedBall]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x x_1 => x • x_1) c ⁻¹' sphere x r = sphere (c⁻¹ • x) r
[PROOFSTEP]
rw [preimage_smul, smul_sphere]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b / a) r
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
[PROOFSTEP]
exact preimage_smul_ball (MulOpposite.op a) b r
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
M : Type u
G : Type v
X : Type w
inst✝⁵ : PseudoMetricSpace X
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : IsometricSMul G X
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
[PROOFSTEP]
exact preimage_smul_closedBall (MulOpposite.op a) b r
[GOAL]
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsometricSMul M X
c : M
x y : Xᵐᵒᵖ
⊢ edist ((fun x => c • x) x) ((fun x => c • x) y) = edist x y
[PROOFSTEP]
simpa only using edist_smul_left c x.unop y.unop
[GOAL]
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsometricSMul M X
c : ULift M
⊢ Isometry fun x => c • x
[PROOFSTEP]
simpa only using isometry_smul X c.down
[GOAL]
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsometricSMul M X
c : M
x y : ULift X
⊢ edist ((fun x => c • x) x) ((fun x => c • x) y) = edist x y
[PROOFSTEP]
simpa only using edist_smul_left c x.1 y.1
