Compfiles/Usa1988P4.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1988, Problem 4

ABC is a triangle with incenter I. Show that the circumcenters of triangles IAB, IBC, and ICA lie on a circle whose center is the circumcenter of triangle ABC.

Imports (4)
Imported by 1 file
  1. abbrev Usa1988P4.I line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, AffineIndependent, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: Affine.Simplex.incenter, Affine.Simplex.mk

    21 instances, coercions and auxiliary constants left out.

  2. abbrev Usa1988P4.O line 40 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, AffineIndependent, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: Affine.Simplex.circumcenter, Affine.Simplex.mk

    20 instances, coercions and auxiliary constants left out.

  3. problem Usa1988P4.usa1988_p4 sorry line 44 source

    depends on sorry what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, AffineIndependent, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Usa1988P4.I, Exists, EuclideanGeometry.Sphere, And, LT.lt and 4 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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