-
Notifications
You must be signed in to change notification settings - Fork 8
/
Bulgaria1998P2.lean
39 lines (31 loc) · 1.13 KB
/
Bulgaria1998P2.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
/-
Copyright (c) 2023 David Renshaw. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Renshaw
-/
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.AffineSpace.Midpoint
import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Geometry.Euclidean.Triangle
import ProblemExtraction
problem_file { tags := [.Geometry] }
/-!
# 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°.)
-/
namespace Bulgaria1998P2
open EuclideanGeometry
problem bulgaria1998_p2
(A B C D E M : EuclideanSpace ℝ (Fin 2))
(H1 : dist D A = dist D C)
(H2 : ∠ D A B = ∠ A B C)
(H3 : M = midpoint ℝ B C) :
∠ B E C = ∠ D A C := by
let x := ∠ D A C
have : ∠ D A C = ∠ D C A := EuclideanGeometry.angle_eq_angle_of_dist_eq H1
let y := ∠ C A B
have : ∠ A B C = x + y := by rw [←H2]; sorry -- need to switch to oangles?
sorry