Six circle theorem

Stream: Is there code for X?

[Ashvni Narayanan]

Does the Miquel's Six Circle theorem / Pivot theorem exist in mathlib?
It states that, given points X, A, B, C, D, E, F, M such that XABD, XBCE, XACF, ADFM and BDEM are concyclic, the points CEFM will be concyclic, too.

Any help is appreciated, thank you!

[Johan Commelin]

I'm pretty sure it isn't there. @Joseph Myers is the expert on euclidean geometry in mathlib

[Kevin Buzzard]

Presumably this is a question in 2D? Or not? The points are in a plane?

[Yaël Dillies]

Yes, there are higher dimensional generalisations, but Miquel is usually stated in the plane

[Ashvni Narayanan]

Kevin Buzzard said:

Presumably this is a question in 2D? Or not? The points are in a plane?

yes it is

[Joseph Myers]

Considering how many very basic things we don't yet have in geometry (someone needs to pick up getting the PRs defining congruence and similarity ready for inclusion in mathlib (#7478 and #7479), for example), you definitely shouldn't expect more advanced results to be present yet.

[Kevin Buzzard]

@Ashvni Narayanan if you are thinking about Euclidean geometry then please feel free to review Joseph's PRs!

[Joseph Myers]

They're not my PRs, one person wrote them in Lean 3, a different person picked them up for mathlib4, both haven't seen any activity lately (and need work to make them ready for inclusion).

[Ashvni Narayanan]

Thank you for the info! A student in my university is looking to use a theorem prover to formalize an advanced version of this result, and wanted to know what is already in mathlib, hence the question!