-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_left_midpoint_eq_pi_div_two_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₃ p₁ = dist p₃ p₂) :
    ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
let m : P := midpoint ℝ p₁ p₂

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
have h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m) := by
  rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
m : P := midpoint ℝ p₁ p₂
h : ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
exact (norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p₃ -ᵥ m) (p₁ -ᵥ m)).mp h.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
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
have h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m) := (vsub_sub_vsub_cancel_right p₃ p₁ m).symm

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Tactic:
rw [dist_eq_norm_vsub V p₃ p₁, dist_eq_norm_vsub V p₃ p₂, h1, h2] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
m : P := midpoint ℝ p₁ p₂
h : ‖p₃ -ᵥ m - (p₁ -ᵥ m)‖ = ‖p₃ -ᵥ m + (p₁ -ᵥ m)‖
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
h2 : p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)
⊢ ∠ p₃ (midpoint ℝ p₁ p₂) p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (p₁ -ᵥ m)

Tactic:
rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel]

Result:
no goals