opposite angles of quadrilateral are equal

Stream: new members

[Attila Vajda]

Hi! I'm trying to prove, and understand this statement:
"1. Let ABCD be a quadrilateral. If the opposite sides of ABCD are pairwise equal, then the opposite angles are pairwise equal."
Can LEAN be used to reason about this? Or to gain insight into this problem?
Thanks

[Daniel Weber]

What you need is basically the SSS congruence rule. I don't think it's in Mathlib, but it shouldn't be hard to conclude from the law of cosines, which is docs#InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle . Or maybe it's easier to reflect across AC and BD, I'm not sure

[Joseph Myers]

For congruence, first we need to get #7478 into mathlib (the PR requires further work). Then, the original !3#18214 included additional congruence material specific to the Euclidean context, which would need to be ported (or rewritten) for Lean 4 and also got ready for mathlib.