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.forall_imp_eq_or {α : Sort u_1} (p : α → Prop) (q : Prop) : ((∀ (a : α), p a) → q) = ((∃ (a : α), ¬p a) ∨ 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 {α : Sort 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

theorem Lean.Grind.xor_eq (a b : Bool) : (a ^^ b) = (a != b)

theorem Lean.Grind.natCast_eq {α : Type u_1} [NatCast α] (a : Nat) : ↑a = ↑a

theorem Lean.Grind.natCast_div (a b : Nat) : ↑(a / b) = ↑a / ↑b

theorem Lean.Grind.natCast_mod (a b : Nat) : ↑(a % b) = ↑a % ↑b

theorem Lean.Grind.natCast_add (a b : Nat) : ↑(a + b) = ↑a + ↑b

theorem Lean.Grind.natCast_mul (a b : Nat) : ↑(a * b) = ↑a * ↑b

theorem Lean.Grind.Nat.pow_one (a : Nat) : a ^ 1 = a

theorem Lean.Grind.Int.pow_one (a : Int) : a ^ 1 = a

theorem Lean.Grind.forall_true (p : True → Prop) : (∀ (h : True), p h) = p True.intro

theorem Lean.Grind.flip_bool_eq (a b : Bool) : (a = b) = (b = a)

theorem Lean.Grind.bool_eq_to_prop (a b : Bool) : (a = b) = ((a = true) = (b = true))