The Butterfly Theorem

Textbook formulation:

A, B, C and D are four points on circle (O). E is the intersection of AC and BD. Through E draw a line perpendicular to OE, meeting AD at F and BC at G. Show that (OverBar[FE]) = (OverBar[GE]).

Remark:

Using the default coordinate system the algebraic methods are very slow.

Input to the system:

Proposition["Butterfly", any[O, A, B, C, D, EE, F, G], 
      point[O, A] ∧ 
pon[C, 
            circle[O, A]] ∧ 
pon[B, 
            circle[O, A]] ∧ 
pon[D, 
            circle[O, A]] ∧ 
inter[EE, line[A, C], 
            line[B, D]] ∧ inter[F, line[D, A], tline[EE, EE, O]] ∧ 
          inter[G, line[B, C], line[EE, F]]
 \[Implies] 
        distequal[EE, F, G, EE]]

Input to the system:

Simplify[Proposition["Butterfly"], 
      by -> GraphicSimplifier]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Butterfly_g", 
      any[O, A, B, C, 
        D], {{ O, {100, 100}}, {A, {0, 100}}, {B, {55, 
            190}}, {C, {171, 170}}, {D, {60, 10}}}]

Input to the system:

Simplify[Proposition["Butterfly"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Butterfly_g"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Wu", 
          Iterate -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Input to the system:

Prove[Proposition["Butterfly"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Area"}]

Inserted notebook generated automatically by the system

End of inserted notebook