Normalization theorems for the grind tactic.

theorem Lean.Grind.iff_eq (p q : Prop) : (p ↔ q) = (p = q)

theorem Lean.Grind.eq_true_eq (p : Prop) : (p = True) = p

theorem Lean.Grind.eq_false_eq (p : Prop) : (p = False) = ¬p

theorem Lean.Grind.not_eq_prop (p q : Prop) : (¬p = q) = (p = ¬q)

theorem Lean.Grind.imp_eq (p q : Prop) : (p → q) = (¬p ∨ q)

theorem Lean.Grind.true_imp_eq (p : Prop) : (True → p) = p

theorem Lean.Grind.false_imp_eq (p : Prop) : (False → p) = True

theorem Lean.Grind.imp_true_eq (p : Prop) : (p → True) = True

theorem Lean.Grind.imp_false_eq (p : Prop) : (p → False) = ¬p

theorem Lean.Grind.imp_self_eq (p : Prop) : (p → p) = True

theorem Lean.Grind.not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q)

theorem Lean.Grind.not_ite {p : Prop} {x✝ : Decidable p} (q r : Prop) : (¬if p then q else r) = if p then ¬q else ¬r

theorem Lean.Grind.ite_true_false {p : Prop} {x✝ : Decidable p} : (if p then True else False) = p

theorem Lean.Grind.ite_false_true {p : Prop} {x✝ : Decidable p} : (if p then False else True) = ¬p

theorem Lean.Grind.not_forall {α : Sort u_1} (p : α → Prop) : (¬∀ (x : α), p x) = ∃ (x : α), ¬p x

theorem Lean.Grind.not_exists {α : Sort u_1} (p : α → Prop) : (¬∃ (x : α), p x) = ∀ (x : α), ¬p x

theorem Lean.Grind.cond_eq_ite {α : Type u_1} (c : Bool) (a b : α) : (bif c then a else b) = if c = true then a else b

theorem Lean.Grind.Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b)

theorem Lean.Grind.Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b)

theorem Lean.Grind.ge_eq {α : Type u_1} [LE α] (a b : α) : (a ≥ b) = (b ≤ a)

theorem Lean.Grind.gt_eq {α : Type u_1} [LT α] (a b : α) : (a > b) = (b < a)

theorem Lean.Grind.beq_eq_decide_eq {α : Type u_1} {x✝ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a == b) = decide (a = b)

theorem Lean.Grind.bne_eq_decide_not_eq {α : Type u_1} {x✝ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = decide ¬a = b