Theorem: Imo2001P1.lemma1 (Compfiles/Imo2001P1.lean)

State before:
t : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))
⊢ ∡ (Affine.Simplex.circumcenter t) (t.points 2) (t.points 1) = ↑Real.pi - ∡ (t.points 1) (t.points 0) (t.points 2)
Tactic:
sorry
State after:
no goals