feat: =, ≠, <, and ≤ functionality for norm_num (#1568)

This PR gives `norm_num` basic inequality (and equality) functionality (towards #1567), including the following:
```
example {α} [DivisionRing α] [CharZero α] : (-1:α) ≠ 2 := by norm_num
```
We implement basic logical extensions to handle `=` and `≠` together, namely `¬`, `True`, and `False`. `≠` is not given an extension, as it is handled by `=` and `¬`.

For now we only can prove `≠` for numbers given a `CharZero α` instance.

- [x] depends on: #1578 

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Algebra/Invertible.lean

@@ -257,6 +257,30 @@ theorem invOf_mul [Monoid α] (a b : α) [Invertible a] [Invertible b] [Invertib
   invOf_eq_right_inv (by simp [← mul_assoc])
 #align inv_of_mul invOf_mul
 
+theorem mul_right_inj_of_invertible [Monoid α] (c : α) [Invertible c] :
+    a * c = b * c ↔ a = b :=
+  ⟨fun h => by simpa using congr_arg (· * ⅟c) h, congr_arg (· * _)⟩
+
+theorem mul_left_inj_of_invertible [Monoid α] (c : α) [Invertible c] :
+    c * a = c * b ↔ a = b :=
+  ⟨fun h => by simpa using congr_arg (⅟c * ·) h, congr_arg (_ * ·)⟩
+
+theorem invOf_mul_eq_iff_eq_mul_left [Monoid α] [Invertible (c : α)] :
+    ⅟c * a = b ↔ a = c * b := by
+  rw [← mul_left_inj_of_invertible (c := c), mul_invOf_self_assoc]
+
+theorem mul_left_eq_iff_eq_invOf_mul [Monoid α] [Invertible (c : α)] :
+    c * a = b ↔ a = ⅟c * b := by
+  rw [← mul_left_inj_of_invertible (c := ⅟c), invOf_mul_self_assoc]
+
+theorem mul_invOf_eq_iff_eq_mul_right [Monoid α] [Invertible (c : α)] :
+    a * ⅟c = b ↔ a = b * c := by
+  rw [← mul_right_inj_of_invertible (c := c), mul_invOf_mul_self_cancel]
+
+theorem mul_right_eq_iff_eq_mul_invOf [Monoid α] [Invertible (c : α)] :
+    a * c = b ↔ a = b * ⅟c := by
+  rw [← mul_right_inj_of_invertible (c := ⅟c), mul_mul_invOf_self_cancel]
+
 theorem Commute.invOf_right [Monoid α] {a b : α} [Invertible b] (h : Commute a b) :
     Commute a (⅟ b) :=
   calc

Mathlib/Data/Nat/Cast/Basic.lean

@@ -164,6 +164,9 @@ alias coe_nat_dvd ← _root_.Dvd.dvd.natCast
 
 end Nat
 
+instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where exists_pair_ne :=
+  ⟨1, 0, (Nat.cast_one (R := α) ▸ Nat.cast_ne_zero.2 (by decide))⟩
+
 section AddMonoidHomClass
 
 variable {A B F : Type _} [AddMonoidWithOne B]

Mathlib/Logic/Nontrivial.lean

@@ -108,18 +108,16 @@ theorem not_nontrivial_iff_subsingleton : ¬Nontrivial α ↔ Subsingleton α :=
 theorem not_nontrivial (α) [Subsingleton α] : ¬Nontrivial α :=
   fun ⟨⟨x, y, h⟩⟩ ↦ h <| Subsingleton.elim x y
 
-theorem not_subsingleton (α) [h : Nontrivial α] : ¬Subsingleton α :=
-  let ⟨⟨x, y, hxy⟩⟩ := h
-  fun ⟨h'⟩ ↦ hxy <| h' x y
+theorem not_subsingleton (α) [Nontrivial α] : ¬Subsingleton α :=
+  fun _ => not_nontrivial _ ‹_›
 
 /-- A type is either a subsingleton or nontrivial. -/
 theorem subsingleton_or_nontrivial (α : Type _) : Subsingleton α ∨ Nontrivial α := by
   rw [← not_nontrivial_iff_subsingleton, or_comm]
   exact Classical.em _
 
 theorem false_of_nontrivial_of_subsingleton (α : Type _) [Nontrivial α] [Subsingleton α] : False :=
-  let ⟨x, y, h⟩ := exists_pair_ne α
-  h <| Subsingleton.elim x y
+  not_nontrivial _ ‹_›
 
 instance Option.nontrivial [Nonempty α] : Nontrivial (Option α) := by
   inhabit α