V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
conv_lhs =>
  rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero,
    add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) := by
  rw [discrim]
  ring
case hc
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ 2 ≠ 0
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + 0 = 0 ↔ r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v
rw [quadratic_eq_zero_iff hvi hd, add_left_neg, zero_div, neg_mul_eq_neg_mul, ←
  mul_sub_right_distrib, sub_eq_add_neg, ← mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left,
  mul_div_assoc]
no goals
case hc
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
⊢ 2 ≠ 0
norm_num
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ inner v v ≠ 0
simpa using hv
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ (2 * inner v (p₁ -ᵥ p₂)) ^ 2 - 4 * inner v v * 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
rw [discrim]
no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : inner v v ≠ 0
⊢ (2 * inner v (p₁ -ᵥ p₂)) ^ 2 - 4 * inner v v * 0 = 2 * inner v (p₁ -ᵥ p₂) * (2 * inner v (p₁ -ᵥ p₂))
ring