theorem Lean.Sym.ne_self {α : Sort u_1} (a : α) : (a ≠ a) = False

theorem Lean.Sym.not_true_eq : (¬True) = False

theorem Lean.Sym.not_false_eq : (¬False) = True

theorem Lean.Sym.ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) {inst' : Decidable c'} (h : c = c') : (if c then a else b) = if c' then a else b

theorem Lean.Sym.dite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬c → α) (c' : Prop) {inst' : Decidable c'} (h : c = c') : dite c a b = if h' : c' then a ⋯ else b ⋯

theorem Lean.Sym.cond_cond_eq_true {α : Sort u} (c : Bool) (a b : α) (h : c = true) : (bif c then a else b) = a

theorem Lean.Sym.cond_cond_eq_false {α : Sort u} (c : Bool) (a b : α) (h : c = false) : (bif c then a else b) = b

theorem Lean.Sym.cond_cond_congr {α : Sort u} (c : Bool) (a b : α) (c' : Bool) (h : c = c') : (bif c then a else b) = bif c' then a else b

theorem Lean.Sym.Nat.lt_eq_true (a b : Nat) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Int.lt_eq_true (a b : Int) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Rat.lt_eq_true (a b : Rat) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Int8.lt_eq_true (a b : Int8) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Int16.lt_eq_true (a b : Int16) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Int32.lt_eq_true (a b : Int32) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Int64.lt_eq_true (a b : Int64) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.UInt8.lt_eq_true (a b : UInt8) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.UInt16.lt_eq_true (a b : UInt16) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.UInt32.lt_eq_true (a b : UInt32) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.UInt64.lt_eq_true (a b : UInt64) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Fin.lt_eq_true {n : Nat} (a b : Fin n) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.BitVec.lt_eq_true {n : Nat} (a b : BitVec n) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.String.lt_eq_true (a b : String) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Char.lt_eq_true (a b : Char) (h : decide (a < b) = true) : (a < b) = True

theorem Lean.Sym.Nat.lt_eq_false (a b : Nat) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Int.lt_eq_false (a b : Int) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Rat.lt_eq_false (a b : Rat) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Int8.lt_eq_false (a b : Int8) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Int16.lt_eq_false (a b : Int16) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Int32.lt_eq_false (a b : Int32) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Int64.lt_eq_false (a b : Int64) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.UInt8.lt_eq_false (a b : UInt8) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.UInt16.lt_eq_false (a b : UInt16) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.UInt32.lt_eq_false (a b : UInt32) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.UInt64.lt_eq_false (a b : UInt64) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Fin.lt_eq_false {n : Nat} (a b : Fin n) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.BitVec.lt_eq_false {n : Nat} (a b : BitVec n) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.String.lt_eq_false (a b : String) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Char.lt_eq_false (a b : Char) (h : decide (a < b) = false) : (a < b) = False

theorem Lean.Sym.Nat.le_eq_true (a b : Nat) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Int.le_eq_true (a b : Int) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Rat.le_eq_true (a b : Rat) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Int8.le_eq_true (a b : Int8) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Int16.le_eq_true (a b : Int16) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Int32.le_eq_true (a b : Int32) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Int64.le_eq_true (a b : Int64) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.UInt8.le_eq_true (a b : UInt8) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.UInt16.le_eq_true (a b : UInt16) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.UInt32.le_eq_true (a b : UInt32) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.UInt64.le_eq_true (a b : UInt64) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Fin.le_eq_true {n : Nat} (a b : Fin n) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.BitVec.le_eq_true {n : Nat} (a b : BitVec n) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.String.le_eq_true (a b : String) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Char.le_eq_true (a b : Char) (h : decide (a ≤ b) = true) : (a ≤ b) = True

theorem Lean.Sym.Nat.le_eq_false (a b : Nat) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Int.le_eq_false (a b : Int) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Rat.le_eq_false (a b : Rat) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Int8.le_eq_false (a b : Int8) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Int16.le_eq_false (a b : Int16) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Int32.le_eq_false (a b : Int32) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Int64.le_eq_false (a b : Int64) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.UInt8.le_eq_false (a b : UInt8) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.UInt16.le_eq_false (a b : UInt16) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.UInt32.le_eq_false (a b : UInt32) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.UInt64.le_eq_false (a b : UInt64) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Fin.le_eq_false {n : Nat} (a b : Fin n) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.BitVec.le_eq_false {n : Nat} (a b : BitVec n) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.String.le_eq_false (a b : String) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Char.le_eq_false (a b : Char) (h : decide (a ≤ b) = false) : (a ≤ b) = False

theorem Lean.Sym.Nat.eq_eq_true (a b : Nat) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Int.eq_eq_true (a b : Int) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Rat.eq_eq_true (a b : Rat) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Int8.eq_eq_true (a b : Int8) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Int16.eq_eq_true (a b : Int16) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Int32.eq_eq_true (a b : Int32) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Int64.eq_eq_true (a b : Int64) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.UInt8.eq_eq_true (a b : UInt8) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.UInt16.eq_eq_true (a b : UInt16) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.UInt32.eq_eq_true (a b : UInt32) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.UInt64.eq_eq_true (a b : UInt64) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Fin.eq_eq_true {n : Nat} (a b : Fin n) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.BitVec.eq_eq_true {n : Nat} (a b : BitVec n) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.String.eq_eq_true (a b : String) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Char.eq_eq_true (a b : Char) (h : decide (a = b) = true) : (a = b) = True

theorem Lean.Sym.Nat.eq_eq_false (a b : Nat) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Int.eq_eq_false (a b : Int) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Rat.eq_eq_false (a b : Rat) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Int8.eq_eq_false (a b : Int8) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Int16.eq_eq_false (a b : Int16) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Int32.eq_eq_false (a b : Int32) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Int64.eq_eq_false (a b : Int64) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.UInt8.eq_eq_false (a b : UInt8) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.UInt16.eq_eq_false (a b : UInt16) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.UInt32.eq_eq_false (a b : UInt32) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.UInt64.eq_eq_false (a b : UInt64) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Fin.eq_eq_false {n : Nat} (a b : Fin n) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.BitVec.eq_eq_false {n : Nat} (a b : BitVec n) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.String.eq_eq_false (a b : String) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Char.eq_eq_false (a b : Char) (h : decide (a = b) = false) : (a = b) = False

theorem Lean.Sym.Nat.dvd_eq_true (a b : Nat) (h : decide (a ∣ b) = true) : (a ∣ b) = True

theorem Lean.Sym.Int.dvd_eq_true (a b : Int) (h : decide (a ∣ b) = true) : (a ∣ b) = True

theorem Lean.Sym.Nat.dvd_eq_false (a b : Nat) (h : decide (a ∣ b) = false) : (a ∣ b) = False

theorem Lean.Sym.Int.dvd_eq_false (a b : Int) (h : decide (a ∣ b) = false) : (a ∣ b) = False