-- Mathlib/Geometry/Euclidean/Basic.lean
theorem eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {s : AffineSubspace ℝ P}
    [FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = 2) {c₁ c₂ p₁ p₂ p : P}
    (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) {r₁ r₂ : ℝ}
    (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁)
    (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂)
    (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Tactic:
rw [hp₂.symm] at hpc₁

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = 1
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * inner (p₂ -ᵥ p₁) (p₁ -ᵥ c₁) / inner (p₂ -ᵥ p₁) (p₂ -ᵥ p₁)
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hpt : p = t₂ • (p₂ -ᵥ p₁) +ᵥ p₁
hop : t₁ = 0
⊢ p = p₁ ∨ p = p₂

Tactic:
subst hpt

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Proof state:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ Pairwise fun i j => inner (b i) (b j) = 0

Tactic:
intro i j hij

Result:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i j : Fin 2
hij : i ≠ j
⊢ inner (b i) (b j) = 0

Proof state:
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : v' ∈ Submodule.span ℝ {p₂ -ᵥ p₁}
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)

Tactic:
rw [Submodule.mem_span_singleton] at hv'

Result:
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : ∃ a, a • (p₂ -ᵥ p₁) = v'
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)