Skip to content

chore: use tfae_* tactics #600

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fmontesi merged 1 commit into from
May 28, 2026
+6 −15
Merged

chore: use tfae_* tactics #600

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 6 additions & 15 deletions Cslib/Foundations/Data/Relation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module

public import Cslib.Init
public import Mathlib.Data.List.TFAE
public import Mathlib.Tactic.TFAE
public import Mathlib.Order.Comparable
public import Mathlib.Order.WellFounded
public import Mathlib.Order.BooleanAlgebra.Basic
Expand Down Expand Up @@ -141,22 +142,12 @@ section euclidean_symm

variable [Std.Symm r]

private theorem RightEuclidean.symm_leftEuclidean [RightEuclidean r] : LeftEuclidean r where
leftEuclidean ac bc := rightEuclidean (symm ac) (symm bc)

private theorem LeftEuclidean.symm_trans [LeftEuclidean r] : IsTrans α r where
trans _ _ _ ab bc := leftEuclidean ab (symm bc)

private theorem RightEuclidean.trans_symm [IsTrans α r] : RightEuclidean r where
rightEuclidean ab ac := _root_.trans (symm ab) ac

open RightEuclidean LeftEuclidean in
private theorem symm_equivalents : [RightEuclidean r, LeftEuclidean r, IsTrans α r].TFAE := by
apply List.tfae_of_cycle
· simp only [List.isChain_cons_cons, List.IsChain.singleton, and_true]
split_ands
· exact @RightEuclidean.symm_leftEuclidean _ _ _
· exact @LeftEuclidean.symm_trans _ _ _
· exact @RightEuclidean.trans_symm _ _ _
tfae_have 1 → 2 := fun _ => ⟨fun ac bc => rightEuclidean (symm ac) (symm bc)⟩
tfae_have 2 → 3 := fun _ => ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩
tfae_have 3 → 1 := fun _ => ⟨fun ab ac => _root_.trans (symm ab) ac⟩
tfae_finish

/-- For a symmetric relation, `LeftEuclidean` and `RightEuclidean` are equivalent. -/
theorem symm_leftEuclidean_iff_rightEuclidean : LeftEuclidean r ↔ RightEuclidean r :=
Expand Down
Loading