[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x y z : P
r R✝ : ℝ
c : P
R : ℝ
⊢ inversion c R c = c
[PROOFSTEP]
simp [inversion]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R : ℝ
c x : P
⊢ inversion c 0 x = c
[PROOFSTEP]
simp [inversion]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b c✝ d x✝ y z : P
r R✝ : ℝ
c : P
a R : ℝ
x : P
⊢ inversion c (a * R) x = ↑(homothety c (a ^ 2)) (inversion c R x)
[PROOFSTEP]
simp only [inversion_eq_lineMap, ← homothety_eq_lineMap, ← homothety_mul_apply, mul_div_assoc, mul_pow]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R : ℝ
c x : P
⊢ inversion c (dist x c) x = x
[PROOFSTEP]
rcases eq_or_ne x c with (rfl | hne)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x✝ y z : P
r R : ℝ
x : P
⊢ inversion x (dist x x) x = x
[PROOFSTEP]
apply inversion_self
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R : ℝ
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x
[PROOFSTEP]
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R : ℝ
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0
[PROOFSTEP]
rwa [dist_ne_zero]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R : ℝ
c x : P
⊢ inversion c (dist c x) x = x
[PROOFSTEP]
rw [dist_comm, inversion_dist_center]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
[PROOFSTEP]
rcases eq_or_ne x c with (rfl | hx)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x✝ y z : P
r R✝ : ℝ
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x
[PROOFSTEP]
simp
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
[PROOFSTEP]
have : dist x c ≠ 0 := dist_ne_zero.2 hx
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
[PROOFSTEP]
field_simp [inversion, norm_smul, abs_div, ← dist_eq_norm_vsub, sq, mul_assoc]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c x : P
R : ℝ
⊢ dist c (inversion c R x) = R ^ 2 / dist c x
[PROOFSTEP]
rw [dist_comm c, dist_comm c, dist_inversion_center]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c : P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion c R (inversion c R x) = x
[PROOFSTEP]
rcases eq_or_ne x c with (rfl | hne)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x✝ y z : P
r R✝ R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x
[PROOFSTEP]
rw [inversion_self, inversion_self]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ inversion c R (inversion c R x) = x
[PROOFSTEP]
rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow, div_mul_div_comm,
  div_mul_cancel _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul, vsub_vadd]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
r R✝ : ℝ
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ R ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ hR
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0
[PROOFSTEP]
by_cases hR : R = 0
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hR : R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0
[PROOFSTEP]
simp [inversion_eq_center, hR]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hR : ¬R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0
[PROOFSTEP]
simp [inversion_eq_center, hR]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R✝ : ℝ
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist (inversion c R x) (inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y
[PROOFSTEP]
dsimp only [inversion]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R✝ : ℝ
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ((R / dist y c) ^ 2 • (y -ᵥ c) +ᵥ c) =
    R ^ 2 / (dist x c * dist y c) * dist x y
[PROOFSTEP]
simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R✝ : ℝ
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y
[PROOFSTEP]
simpa only [dist_vsub_cancel_right] using dist_div_norm_sq_smul (vsub_ne_zero.2 hx) (vsub_ne_zero.2 hy) R
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
rcases eq_or_ne R 0 with rfl | hR
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r : ℝ
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c
[PROOFSTEP]
simp [dist_comm, mul_comm]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
have hy' : inversion c R y ≠ c := by simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ inversion c R y ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
conv in dist _ y => rw [← inversion_inversion c hR y]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
| dist (inversion c R x) y
[PROOFSTEP]
rw [← inversion_inversion c hR y]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
| dist (inversion c R x) y
[PROOFSTEP]
rw [← inversion_inversion c hR y]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
| dist (inversion c R x) y
[PROOFSTEP]
rw [← inversion_inversion c hR y]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ dist (inversion c R x) (inversion c R (inversion c R y)) * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
rw [dist_inversion_inversion hx hy', dist_inversion_center]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
have : dist x c ≠ 0 := dist_ne_zero.2 hx
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
this : dist x c ≠ 0
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
[PROOFSTEP]
field_simp
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x y z : P
r R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
this : dist x c ≠ 0
⊢ R ^ 2 * dist y c * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c * (dist x c * R ^ 2)
[PROOFSTEP]
ring
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rcases eq_or_ne b a with (rfl | hb)
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
r R : ℝ
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
[PROOFSTEP]
rw [dist_self, zero_mul, zero_add]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb : b ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rcases eq_or_ne c a with (rfl | hc)
[GOAL]
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
r R : ℝ
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d
[PROOFSTEP]
rw [dist_self, zero_mul]
[GOAL]
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
r R : ℝ
b c d : P
hb : b ≠ c
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d
[PROOFSTEP]
apply_rules [add_nonneg, mul_nonneg, dist_nonneg]
[GOAL]
case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rcases eq_or_ne d a with (rfl | hd)
[GOAL]
case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
r R : ℝ
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
[PROOFSTEP]
rw [dist_self, mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
  /- Otherwise, we apply the triangle inequality to `EuclideanGeometry.inversion a 1 b`,
      `EuclideanGeometry.inversion a 1 c`, and `EuclideanGeometry.inversion a 1 d`. -/
[GOAL]
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
have H := dist_triangle (inversion a 1 b) (inversion a 1 c) (inversion a 1 d)
[GOAL]
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  dist (inversion a 1 b) (inversion a 1 d) ≤
    dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rw [dist_inversion_inversion hb hd, dist_inversion_inversion hb hc, dist_inversion_inversion hc hd, one_pow] at H 
[GOAL]
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rw [← dist_pos] at hb hc hd 
[GOAL]
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
[PROOFSTEP]
rw [← div_le_div_right (mul_pos hb (mul_pos hc hd))]
[GOAL]
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
[PROOFSTEP]
convert H using 1
[GOAL]
case h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d
[PROOFSTEP]
field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]
[GOAL]
case h.e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist c a * dist b d * (dist b a * dist d a) = dist b d * (dist b a * (dist c a * dist d a))
[PROOFSTEP]
ring
[GOAL]
case h.e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
[PROOFSTEP]
field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]
[GOAL]
case h.e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
r R : ℝ
a b c d : P
hb✝ : b ≠ a
hb : 0 < dist b a
hc✝ : c ≠ a
hc : 0 < dist c a
hd✝ : d ≠ a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ (dist b a * dist c d + dist b c * dist d a) * (dist b a * dist c a * (dist c a * dist d a)) =
    (dist b c * (dist c a * dist d a) + dist c d * (dist b a * dist c a)) * (dist b a * (dist c a * dist d a))
[PROOFSTEP]
ring
