-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint {p₁ p₂ p : P} (h : p₁ ≠ p₂) :
    dist p₁ p = dist p₂ p ↔
      ∃ r : ℝ, r • o.rotation (π / 2 : ℝ) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Proof state:
case refine_1.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr : p = r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Tactic:
exact ⟨r, hr.symm⟩

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : inner (p -ᵥ p₁) (p -ᵥ p₁) = inner (p -ᵥ p₂) (p -ᵥ p₂)
⊢ inner (p₂ -ᵥ p₁) (p -ᵥ midpoint ℝ p₁ p₂) = 0

Tactic:
simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right,
  inner_smul_right, hd, real_inner_comm (p -ᵥ p₁)]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : inner (p -ᵥ p₁) (p -ᵥ p₁) = inner (p -ᵥ p₂) (p -ᵥ p₂)
⊢ ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) -
      (⅟2 * inner (p -ᵥ p₁) (p -ᵥ p₂) + ⅟2 * inner (p -ᵥ p₂) (p -ᵥ p₂)) =
    0

Proof state:
case refine_2.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ inner (2⁻¹ • -(p₂ -ᵥ p₁)) (2⁻¹ • -(p₂ -ᵥ p₁)) - inner (2⁻¹ • -(p₂ -ᵥ p₁)) (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) -
        inner (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) (2⁻¹ • -(p₂ -ᵥ p₁)) +
      inner (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) =
    inner (2⁻¹ • (p₂ -ᵥ p₁)) (2⁻¹ • (p₂ -ᵥ p₁)) - inner (2⁻¹ • (p₂ -ᵥ p₁)) (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) -
        inner (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) (2⁻¹ • (p₂ -ᵥ p₁)) +
      inner (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)) (r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁))

Tactic:
simp [-neg_vsub_eq_vsub_rev]

Result:
no goals

Proof state:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
hi : inner (p₂ -ᵥ p₁) (p -ᵥ midpoint ℝ p₁ p₂) = 0
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Tactic:
rw [@Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ _ o,
  or_iff_right (vsub_ne_zero.2 h.symm)] at hi

Result:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
hi : ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) = p -ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p