chore: rename Classical.and_not (#612)

Std/Data/Nat/Lemmas.lean

@@ -171,7 +171,7 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
 protected alias eq_iff_le_and_ge := Nat.le_antisymm_iff
 
 protected theorem lt_or_gt_of_ne {a b : Nat} : a ≠ b → a < b ∨ b < a := by
-  rw [← Nat.not_le, ← Nat.not_le, ← Decidable.not_and, and_comm]
+  rw [← Nat.not_le, ← Nat.not_le, ← Decidable.not_and_iff_or_not_not, and_comm]
   exact mt Nat.le_antisymm_iff.2
 protected alias lt_or_lt_of_ne := Nat.lt_or_gt_of_ne
 @[deprecated] protected alias lt_connex := Nat.lt_or_gt_of_ne

Std/Logic.lean

@@ -594,7 +594,7 @@ theorem Decidable.imp_or' [Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a 
   if h : b then by simp [h] else by
     rw [eq_false h, false_or]; exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm
 
-theorem Decidable.not_imp [Decidable a] : ¬(a → b) ↔ a ∧ ¬b :=
+theorem Decidable.not_imp_iff_and_not [Decidable a] : ¬(a → b) ↔ a ∧ ¬b :=
   ⟨fun h => ⟨of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩
 
 theorem Decidable.peirce (a b : Prop) [Decidable a] : ((a → b) → a) → a :=
@@ -626,17 +626,17 @@ theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] :
 theorem Decidable.not_and_not_right [Decidable b] : ¬(a ∧ ¬b) ↔ (a → b) :=
   ⟨fun h ha => not_imp_symm (And.intro ha) h, fun h ⟨ha, hb⟩ => hb <| h ha⟩
 
-theorem Decidable.not_and [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
+theorem Decidable.not_and_iff_or_not_not [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
   ⟨fun h => if ha : a then .inr (h ⟨ha, ·⟩) else .inl ha, not_and_of_not_or_not⟩
 
-theorem Decidable.not_and' [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
+theorem Decidable.not_and_iff_or_not_not' [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
   ⟨fun h => if hb : b then .inl (h ⟨·, hb⟩) else .inr hb, not_and_of_not_or_not⟩
 
 theorem Decidable.or_iff_not_and_not [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b) := by
   rw [← not_or, not_not]
 
 theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b) := by
-  rw [← not_and, not_not]
+  rw [← not_and_iff_or_not_not, not_not]
 
 theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
   ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
@@ -718,11 +718,11 @@ theorem or_iff_not_imp_left : a ∨ b ↔ (¬a → b) :=
 theorem or_iff_not_imp_right : a ∨ b ↔ (¬b → a) :=
   Decidable.or_iff_not_imp_right
 
-theorem not_imp : ¬(a → b) ↔ a ∧ ¬b :=
-  Decidable.not_imp
+theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b :=
+  Decidable.not_imp_iff_and_not
 
-theorem not_and : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
-  Decidable.not_and
+theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
+  Decidable.not_and_iff_or_not_not
 
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) :=
   Decidable.not_iff

Std/Tactic/Omega/Int.lean

@@ -134,7 +134,7 @@ theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.
 theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop}
     {p q : α × β} (w : ¬ Prod.Lex r s p q) :
     ¬ r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬ s p.snd q.snd) := by
-  rw [Prod.lex_def, not_or, Decidable.not_and] at w
+  rw [Prod.lex_def, not_or, Decidable.not_and_iff_or_not_not] at w
   exact w
 
 theorem fst_mk : (Prod.mk x y).fst = x := rfl

Std/Tactic/Omega/Logic.lean

@@ -29,4 +29,4 @@ theorem Decidable.not_iff_iff_and_not_or_not_and [Decidable a] [Decidable b] :
 
 alias ⟨Decidable.and_not_or_not_and_of_not_iff, _⟩ := Decidable.not_iff_iff_and_not_or_not_and
 
-alias ⟨Decidable.and_not_of_not_imp, _⟩ := Decidable.not_imp
+alias ⟨Decidable.and_not_of_not_imp, _⟩ := Decidable.not_imp_iff_and_not