Compfiles/Bulgaria1998P2.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Bulgarian Mathematical Olympiad 1998, Problem 2

A convex quadrilateral ABCD has AD = CD and ∠DAB = ∠ABC < 90°. The line through D and the midpoint of BC intersects line AB in point E. Prove that ∠BEC = ∠DAC. (Note: The problem is valid without the assumption ∠ABC < 90°.)

Imports (5)
Imported by 1 file
  1. problem Bulgaria1998P2.bulgaria1998_p2 sorry line 33 source

    depends on sorry what this means

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Not, Collinear, ENNReal, Insert.insert, Set, Singleton.singleton, Exists, And, Sbtw, Eq, Dist.dist, EuclideanGeometry.angle, midpoint

    Proof uses: EuclideanGeometry.angle_eq_angle_of_dist_eq, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    102 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.