feat(logic/lemmas): Aliases for =-≠ transitivity lemmas (#16959)

leanprover-community · Oct 15, 2022 · 4a4d740 · 4a4d740
1 parent 0a37590
commit 4a4d740
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/logic/lemmas.lean b/src/logic/lemmas.lean
@@ -22,6 +22,9 @@ alias heq_iff_eq ↔ heq.eq eq.heq
 
 attribute [protected] heq.eq eq.heq
 
+alias ne_of_eq_of_ne ← eq.trans_ne
+alias ne_of_ne_of_eq ← ne.trans_eq
+
 variables {α : Sort*} {p q r : Prop} [decidable p] [decidable q] {a b c : α}
 
 lemma dite_dite_distrib_left {a : p → α} {b : ¬ p → q → α} {c : ¬ p → ¬ q → α} :