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_true : (¬True) = False

theorem Lean.Grind.not_false : (¬False) = True

theorem Lean.Grind.not_not (p : Prop) : (¬¬p) = p

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

theorem Lean.Grind.not_or (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.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.not_implies (p q : Prop) : (¬(p → q)) = (p ∧ ¬q)

theorem Lean.Grind.or_assoc (p q r : Prop) : ((p ∨ q) ∨ r) = (p ∨ q ∨ r)

theorem Lean.Grind.or_swap12 (p q r : Prop) : (p ∨ q ∨ r) = (q ∨ p ∨ r)

theorem Lean.Grind.or_swap13 (p q r : Prop) : (p ∨ q ∨ r) = (r ∨ q ∨ p)

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.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.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.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.natCast_pow (a b : Nat) : ↑(a ^ b) = ↑a ^ b

theorem Lean.Grind.natCast_id (a : Nat) : ↑a = a

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))

theorem Lean.Grind.forall_or_forall {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop) : (∀ (a : α), p a ∨ ∀ (b : β a), q a b) = ∀ (a : α) (b : β a), p a ∨ q a b

theorem Lean.Grind.forall_forall_or {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop) : (∀ (a : α), (∀ (b : β a), q a b) ∨ p a) = ∀ (a : α) (b : β a), q a b ∨ p a

theorem Lean.Grind.forall_and {α : Sort u_1} {p q : α → Prop} : (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x)

theorem Lean.Grind.exists_const (α : Sort u) [i : Nonempty α] {b : Prop} : (∃ (x : α), b) = b

theorem Lean.Grind.exists_or {α : Sort u} {p q : α → Prop} : (∃ (x : α), p x ∨ q x) = ((∃ (x : α), p x) ∨ ∃ (x : α), q x)

theorem Lean.Grind.exists_prop {a b : Prop} : (∃ (_h : a), b) = (a ∧ b)

theorem Lean.Grind.exists_and_left {α : Sort u} {p : α → Prop} {b : Prop} : (∃ (x : α), b ∧ p x) = (b ∧ ∃ (x : α), p x)

theorem Lean.Grind.exists_and_right {α : Sort u} {p : α → Prop} {b : Prop} : (∃ (x : α), p x ∧ b) = ((∃ (x : α), p x) ∧ b)

theorem Lean.Grind.zero_sub (a : Nat) : 0 - a = 0

Helper theorems for the simproc Sym.Simp.simpNatRel.

theorem Lean.Grind.Nat.add_succ_eq_zero_eq_false (a k : Nat) : (a + (k + 1) = 0) = False

theorem Lean.Grind.Nat.zero_eq_add_succ_eq_false (a k : Nat) : (0 = a + (k + 1)) = False

theorem Lean.Grind.Nat.add_succ_le_zero_eq_false (a k : Nat) : (a + (k + 1) ≤ 0) = False

theorem Lean.Grind.Nat.zero_le_eq_true (a : Nat) : (0 ≤ a) = True

theorem Lean.Grind.smul_nat_eq_mul {α : Type u_1} [Semiring α] (n : Nat) (a : α) : n • a = ↑n * a

theorem Lean.Grind.smul_int_eq_mul {α : Type u_1} [Ring α] (i : Int) (a : α) : i • a = ↑i * a

theorem Lean.Grind.Int.subNatNat_eq (a b : Nat) : Int.subNatNat a b = ↑a - ↑b

theorem Lean.Grind.Int.sign_eq (x : Int) : x.sign = if x > 0 then 1 else if x < 0 then -1 else 0