-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :
    dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Proof state:
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

Tactic:
rw [quadratic_eq_zero_iff hvi hd, neg_add_cancel, 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]

Result:
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

Proof state:
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

Tactic:
have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) := by
  rw [discrim]
  ring

Result:
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

Proof state:
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₂))

Tactic:
ring

Result:
no goals

Proof state:
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

Tactic:
norm_num

Result:
no goals

Proof state:
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₂))

Tactic:
rw [discrim]

Result:
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₂))

Proof state:
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

Tactic:
conv_lhs =>
  rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
    ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
    sub_self]

Result:
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

Proof state:
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

Tactic:
simpa using hv

Result:
no goals

Proof state:
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

Tactic:
have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv

Result:
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