case inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
R : ℝ
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d

case inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
R : ℝ
a b c d : P
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
rcases eq_or_ne b a with (rfl | hb)
case inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
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

case inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
case inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
rcases eq_or_ne c a with (rfl | hc)
case inr.inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
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

case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
case inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
rcases eq_or_ne d a with (rfl | hd)
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
have H := dist_triangle (inversion a 1 b) (inversion a 1 c) (inversion a 1 d)
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
rw [dist_inversion_inversion hb hd, dist_inversion_inversion hb hc,
  dist_inversion_inversion hc hd, one_pow] at H
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
rw [← dist_pos] at hb hc hd
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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))
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
rw [← div_le_div_right (mul_pos hb (mul_pos hc hd))]
no goals
case inr.inr.inr
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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))
convert H using 1 <;> (field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]; ring)
no goals
case inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
R : ℝ
b c d : P
⊢ dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
rw [dist_self, MulZeroClass.zero_mul, zero_add]
case inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
R : ℝ
b c d : P
hb : b ≠ c
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d
case inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
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
rw [dist_self, MulZeroClass.zero_mul]
no goals
case inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
R : ℝ
b c d : P
hb : b ≠ c
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d
apply_rules [add_nonneg, mul_nonneg, dist_nonneg]
no goals
case inr.inr.inl
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b✝ c✝ d✝ x y z : P
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
rw [dist_self, MulZeroClass.mul_zero, add_zero, dist_comm d, dist_comm d, mul_comm]
case h.e'_4
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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))
case h.e'_4
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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
field_simp [hb.ne', hc.ne', hd.ne', dist_comm a]
no goals
case h.e'_4
V : Type ?u.37918
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a✝ b✝ c✝ d✝ x y z : P
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))
ring