Commit 2023-01-07 10:11 72b23bd4

View on Github →

chore: remove iff_self from simp only after lean4#1933 (#1406)

Estimated changes

Modified Mathlib/Algebra/Order/Field/Basic.lean

modified theorem inv_lt_zero

modified theorem inv_nonpos

Modified Mathlib/Algebra/Order/Group/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

Modified Mathlib/Algebra/Order/Ring/Abs.lean

Modified Mathlib/Algebra/Order/Ring/Canonical.lean

Modified Mathlib/Algebra/Order/Ring/Lemmas.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Forall2.lean

Modified Mathlib/Data/Nat/Order/Basic.lean

Modified Mathlib/Data/Option/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Set/Intervals/Basic.lean

Modified Mathlib/Data/Set/Intervals/UnorderedInterval.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

Modified Mathlib/Logic/IsEmpty.lean

Modified Mathlib/Logic/Nontrivial.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Bounded.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Directed.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Tactic/Zify.lean