Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2012P5

import Mathlib.Geometry.Euclidean.Altitude
import Mathlib.Geometry.Euclidean.Angle.Sphere
import Mathlib.Geometry.Euclidean.Sphere.Power
import Mathlib.Geometry.Euclidean.Sphere.SecondInter

/-!
# International Mathematical Olympiad 2012, Problem 5

Let `ABC` be a triangle with `∠BCA = 90°`, and let `D` be the foot of the altitude from `C`.
Let `X` be a point in the interior of the segment `CD`. Let `K` be the point on the segment `AX`
such that `BK = BC`. Similarly, let `L` be the point on the segment `BX` such that `AL = AC`.
Let `M` be the point of intersection of `AL` and `BK`.
Show that `MK = ML`.
-/

open Affine EuclideanGeometry Module

open scoped EuclideanGeometry Real

variable (V P : Type*) [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [MetricSpace P] [NormedAddTorsor V P]

namespace Imo2012P5

theorem imo2012_p5 [Fact (finrank ℝ V = 2)] {A B C D X K L M : P}
    (affineIndependent_ABC : AffineIndependent ℝ ![A, B, C])
    (angle_BCA : ∠ B C A = π / 2)
    (D_eq_altitudeFoot : D = Simplex.altitudeFoot ⟨_, affineIndependent_ABC⟩ 2)
    (sbtw_CXD : Sbtw ℝ C X D)
    (wbtw_AKX : Wbtw ℝ A K X) (BK_eq_BC : dist B K = dist B C)
    (wbtw_BLX : Wbtw ℝ B L X) (AL_eq_AC : dist A L = dist A C)
    (M_mem_inf_AL_BK : M ∈ line[ℝ, A, L] ⊓ line[ℝ, B, K]) :
    dist M K = dist M L := sorry

File author(s): tenthmascot

This problem has a complete formalized solution.