Commit 2024-02-20 12:29 85db972f

View on Github →

chore: Remove Init.IteSimp (#10708) These lemmas can easily go in Logic.Basic. Also rename and restate them to better match the convention.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

modified theorem SimpleGraph.replaceVertex_self

Modified Mathlib/Init/Data/Ordering/Lemmas.lean

modified theorem cmpUsing_eq_eq

modified theorem cmpUsing_eq_gt

Deleted Mathlib/Init/IteSimp.lean

deleted theorem if_false_left_eq_and

deleted theorem if_false_right_eq_and

deleted theorem if_true_left_eq_or

deleted theorem if_true_right_eq_or

Modified Mathlib/Logic/Basic.lean

added theorem if_false_left

added theorem if_false_right

added theorem if_true_left

added theorem if_true_right

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean