case intro.intro.intro
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
k₁ : ℝ
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
⊢ dist a p * dist b p = dist c p * dist d p
obtain ⟨-, k₁, -, hab₁⟩ := angle_eq_zero_iff.mp hapb
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
k₁ : ℝ
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p
case intro.intro.intro
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
k₁ : ℝ
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p
obtain ⟨-, k₂, -, hcd₁⟩ := angle_eq_zero_iff.mp hcpd
case intro.intro.intro.intro.intro.intro.refine'_1
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
k₁ k₂ : ℝ
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
hab₁ : b -ᵥ p = a -ᵥ p
hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)
hnot : k₁ = 1
⊢ False

case intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
k₁ k₂ : ℝ
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
hcd₁ : d -ᵥ p = c -ᵥ p
hnot : k₂ = 1
⊢ False
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
k₁ : ℝ
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
k₂ : ℝ
hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)
⊢ dist a p * dist b p = dist c p * dist d p
refine' mul_dist_eq_mul_dist_of_cospherical h ⟨k₁, _, hab₁⟩ ⟨k₂, _, hcd₁⟩ <;> by_contra hnot <;>
  simp_all only [Classical.not_not, one_smul]
no goals
case intro.intro.intro.intro.intro.intro.refine'_1
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
k₁ k₂ : ℝ
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
hab₁ : b -ᵥ p = a -ᵥ p
hcd₁ : d -ᵥ p = k₂ • (c -ᵥ p)
hnot : k₁ = 1
⊢ False

case intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_1
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
k₁ k₂ : ℝ
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hapb : ∠ a p b = 0
hcpd : ∠ c p d = 0
hab₁ : b -ᵥ p = k₁ • (a -ᵥ p)
hcd₁ : d -ᵥ p = c -ᵥ p
hnot : k₂ = 1
⊢ False
exacts [hab (vsub_left_cancel hab₁).symm, hcd (vsub_left_cancel hcd₁).symm]