Lean.Grind.CommRing.Poly.concat.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (p₁ : Grind.CommRing.Poly), motive p₁
Lean.Grind.CommRing.Poly.addConst.go.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (a : Grind.CommRing.Poly), motive a

Int.neg_neg_iff_pos : ∀ {a : Int}, -a < 0 ↔ 0 < a
Int.neg_lt_zero_iff : ∀ {a : Int}, -a < 0 ↔ 0 < a

Classical.not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
Classical.not_imp_iff_and_not : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b

forall_congr : ∀ {α : Sort u} {p q : α → Prop}, (∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a
pi_congr : ∀ {α : Sort u} {β β' : α → Sort v}, (∀ (a : α), β a = β' a) → ((a : α) → β a) = ((a : α) → β' a)

Lean.Omega.Int.natCast_ofNat : ∀ {x : Nat}, ↑(OfNat.ofNat x) = OfNat.ofNat x
Int.cast_ofNat_Int : ∀ {n : Nat}, ↑(OfNat.ofNat n) = OfNat.ofNat n

List.not_lt_iff_ge : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁
Array.not_lt_iff_ge : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁

Vector.contains_iff : ∀ {α : Type u_1} {n : Nat} [inst : BEq α] [LawfulBEq α] {a : α} {as : Vector α n},
  as.contains a = true ↔ a ∈ as
Vector.contains_iff_mem : ∀ {α : Type u_1} {n : Nat} [inst : BEq α] [LawfulBEq α] {xs : Vector α n} {a : α},
  xs.contains a = true ↔ a ∈ xs

List.not_le_iff_gt : ∀ {α : Type u_1} [DecidableEq α] [inst : LT α] [DecidableLT α] {l₁ l₂ : List α}, ¬l₁ ≤ l₂ ↔ l₂ < l₁
Array.not_le_iff_gt : ∀ {α : Type u_1} [DecidableEq α] [inst : LT α] [DecidableLT α] {l₁ l₂ : List α},
  ¬l₁ ≤ l₂ ↔ l₂ < l₁

UInt8.toFin_mod : ∀ (a b : UInt8), (a % b).toFin = a.toFin % b.toFin
UInt16.toFin_mod : ∀ (a b : UInt8), (a % b).toFin = a.toFin % b.toFin

Array.unzip_snd : ∀ {α : Type u_1} {β : Type u_2} {l : Array (α × β)}, l.unzip.snd = Array.map Prod.snd l
Array.snd_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.snd = Array.map Prod.snd xs

Int.ediv_nonneg_of_nonneg_of_nonneg : ∀ {x y : Int}, 0 ≤ x → 0 ≤ y → 0 ≤ x / y
Int.ediv_nonneg : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → 0 ≤ a / b

List.flatten_toArray : ∀ {α : Type u_1} {L : List (List α)},
  (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
Array.flatten_map_toArray : ∀ {α : Type u_1} {L : List (List α)},
  (Array.map List.toArray L.toArray).flatten = L.flatten.toArray

Int.ofNat_zero_le : ∀ (n : Nat), 0 ≤ ↑n
Int.ofNat_nonneg : ∀ (n : Nat), 0 ≤ ↑n

Option.ext : ∀ {α : Type u_1} {o₁ o₂ : Option α}, (∀ (a : α), o₁ = some a ↔ o₂ = some a) → o₁ = o₂
Option.eq_of_eq_some : ∀ {α : Type u} {x y : Option α}, (∀ (z : α), x = some z ↔ y = some z) → x = y

Lean.Grind.CommRing.Expr.toPoly.induct : ∀ (motive : Grind.CommRing.Expr → Prop),
  (∀ (n : Int), motive (Grind.CommRing.Expr.num n)) →
    (∀ (x : Grind.CommRing.Var), motive (Grind.CommRing.Expr.var x)) →
      (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.add b)) →
        (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.mul b)) →
          (∀ (a : Grind.CommRing.Expr), motive a → motive a.neg) →
            (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.sub b)) →
              (∀ (k : Nat) (n : Int), motive ((Grind.CommRing.Expr.num n).pow k)) →
                (∀ (k : Nat) (x : Grind.CommRing.Var), motive ((Grind.CommRing.Expr.var x).pow k)) →
                  (∀ (a : Grind.CommRing.Expr) (k : Nat),
                      (∀ (n : Int), a = Grind.CommRing.Expr.num n → False) →
                        (∀ (x : Grind.CommRing.Var), a = Grind.CommRing.Expr.var x → False) →
                          motive a → motive (a.pow k)) →
                    ∀ (a : Grind.CommRing.Expr), motive a
Lean.Grind.CommRing.Expr.toPolyC.go.induct : ∀ (motive : Grind.CommRing.Expr → Prop),
  (∀ (n : Int), motive (Grind.CommRing.Expr.num n)) →
    (∀ (x : Grind.CommRing.Var), motive (Grind.CommRing.Expr.var x)) →
      (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.add b)) →
        (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.mul b)) →
          (∀ (a : Grind.CommRing.Expr), motive a → motive a.neg) →
            (∀ (a b : Grind.CommRing.Expr), motive a → motive b → motive (a.sub b)) →
              (∀ (k : Nat) (n : Int), motive ((Grind.CommRing.Expr.num n).pow k)) →
                (∀ (k : Nat) (x : Grind.CommRing.Var), motive ((Grind.CommRing.Expr.var x).pow k)) →
                  (∀ (a : Grind.CommRing.Expr) (k : Nat),
                      (∀ (n : Int), a = Grind.CommRing.Expr.num n → False) →
                        (∀ (x : Grind.CommRing.Var), a = Grind.CommRing.Expr.var x → False) →
                          motive a → motive (a.pow k)) →
                    ∀ (a : Grind.CommRing.Expr), motive a

Int.add_le_iff_le_sub : ∀ {a b c : Int}, a + b ≤ c ↔ a ≤ c - b
Lean.Omega.Int.add_le_iff_le_sub : ∀ {a b c : Int}, a + b ≤ c ↔ a ≤ c - b

Nat.mul_div_cancel_left : ∀ (m : Nat) {n : Nat}, 0 < n → n * m / n = m
Nat.mul_div_right : ∀ (n : Nat) {m : Nat}, 0 < m → m * n / m = n

Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg : ∀ {a b c d : Int}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
Int.mul_le_mul : ∀ {a b c d : Int}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d

Vector.back_append_right : ∀ {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} [inst : NeZero m],
  (xs ++ ys).back = ys.back
Vector.back_append_of_neZero : ∀ {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} [inst : NeZero m],
  (xs ++ ys).back = ys.back

Std.DTreeMap.Internal.Impl.insertMin!.fun_cases : ∀
  (motive : {α : Type u} → {β : α → Type v} → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ {α : Type u} {β : α → Type v} (k : α) (v : β k), motive k v Std.DTreeMap.Internal.Impl.leaf) →
    (∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (size : Nat) (k' : α) (v' : β k')
        (l' r' : Std.DTreeMap.Internal.Impl α β), motive k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')) →
      ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β), motive k v t
Std.DTreeMap.Internal.Impl.insertMax!.fun_cases : ∀
  (motive : {α : Type u} → {β : α → Type v} → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ {α : Type u} {β : α → Type v} (k : α) (v : β k), motive k v Std.DTreeMap.Internal.Impl.leaf) →
    (∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (size : Nat) (k' : α) (v' : β k')
        (l' r' : Std.DTreeMap.Internal.Impl α β), motive k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')) →
      ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β), motive k v t

Nat.mul_lt_mul'' : ∀ {a b c d : Nat}, a < c → b < d → a * b < c * d
Nat.mul_lt_mul_of_lt_of_lt : ∀ {a b c d : Nat}, a < c → b < d → a * b < c * d

Lean.Grind.CommRing.Poly.addConstC.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (p : Grind.CommRing.Poly), motive p
Lean.Grind.CommRing.Poly.addConst.go.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (a : Grind.CommRing.Poly), motive a

Bool.of_not_eq_false : ∀ {b : Bool}, ¬b = false → b = true
eq_true_of_ne_false : ∀ {b : Bool}, ¬b = false → b = true

Char.lt_iff_val_lt_val : ∀ {a b : Char}, a < b ↔ a.val < b.val
Char.lt_def : ∀ {a b : Char}, a < b ↔ a.val < b.val

Std.TreeSet.mem_of_mem_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp]
  {k a : α}, (t.erase k).contains a = true → t.contains a = true
Std.TreeSet.contains_of_contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}
  [Std.TransCmp cmp] {k a : α}, (t.erase k).contains a = true → t.contains a = true

Int32.not_eq_neg_add : ∀ (a : Int32), ~~~a = -a - 1
Int32.not_eq_neg_sub : ∀ (a : Int32), ~~~a = -a - 1

id_eq : ∀ {α : Sort u_1} (a : α), id a = a
id_def : ∀ {α : Sort u} (a : α), id a = a

false_implies : ∀ (p : Prop), (False → p) = True
Lean.Grind.false_imp_eq : ∀ (p : Prop), (False → p) = True

Array.all_eq_true' : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.all p = true ↔ ∀ (x : α), x ∈ as → p x = true
Array.all_eq_true_iff_forall_mem : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α},
  xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

Nat.succ_ne_succ_iff : ∀ {a b : Nat}, a.succ ≠ b.succ ↔ a ≠ b
Nat.succ_ne_succ : ∀ {m n : Nat}, m.succ ≠ n.succ ↔ m ≠ n

Array.toArray_eq : ∀ {α : Type u_1} {as : List α} {xs : Array α}, as.toArray = xs ↔ as = xs.toList
List.toArray_eq_iff : ∀ {α : Type u_1} {as : List α} {bs : Array α}, as.toArray = bs ↔ as = bs.toList

Int64.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int8}, (-1) <<< b ||| a <<< b = (-1) <<< b
Int8.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int8}, (-1) <<< b ||| a <<< b = (-1) <<< b

BitVec.not_lt_iff_le : ∀ {w : Nat} {x y : BitVec w}, ¬x < y ↔ y ≤ x
BitVec.not_lt : ∀ {n : Nat} {x y : BitVec n}, ¬x < y ↔ y ≤ x

Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey! l ↔
          (k == Std.Internal.List.maxKey! l) = false)
Std.Internal.List.maxKey!_eraseKey_eq_iff_beq_maxKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.maxKey! l ↔
          (k == Std.Internal.List.maxKey! l) = false)

Char.eq_of_val_eq : ∀ {c d : Char}, c.val = d.val → c = d
Char.ext : ∀ {a b : Char}, a.val = b.val → a = b

Lean.Omega.Int.not_le_of_lt : ∀ {x y : Int}, y < x → ¬x ≤ y
Int.not_le_of_gt : ∀ {a b : Int}, b < a → ¬a ≤ b

Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm
      (Std.Internal.List.insertEntryIfNew k v t.toListModel)
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm
      (Std.Internal.List.insertEntryIfNew k v t.toListModel)

Nat.add_sub_cancel_left : ∀ (n m : Nat), n + m - n = m
Nat.add_sub_self_left : ∀ (a b : Nat), a + b - a = b

List.not_lt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁
Array.not_lt_iff_ge : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁

Lean.Omega.Int.lt_of_not_le : ∀ {x y : Int}, ¬x ≤ y → y < x
Lean.Omega.Int.lt_of_not_ge : ∀ {x y : Int}, ¬x ≤ y → y < x

Int8.not_eq_neg_sub : ∀ (a : Int8), ~~~a = -a - 1
Int8.not_eq_neg_add : ∀ (a : Int8), ~~~a = -a - 1

Int.lt_of_not_ge : ∀ {a b : Int}, ¬a ≤ b → b < a
Lean.Omega.Int.lt_of_not_ge : ∀ {x y : Int}, ¬x ≤ y → y < x

Int.lt_add_of_neg_add_lt_left : ∀ {a b c : Int}, -b + a < c → a < b + c
Int.lt_add_of_neg_add_lt : ∀ {a b c : Int}, -b + a < c → a < b + c

Std.TransCmp.gt_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → cmp b c = Ordering.gt → cmp a c = Ordering.gt
Std.TransCmp.gt_of_gt_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → cmp b c = Ordering.gt → cmp a c = Ordering.gt

Lean.Grind.CommRing.Poly.mulConst.go.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (a : Grind.CommRing.Poly), motive a
Lean.Grind.CommRing.Poly.addConst.go.induct : ∀ (motive : Grind.CommRing.Poly → Prop),
  (∀ (a : Int), motive (Grind.CommRing.Poly.num a)) →
    (∀ (a : Int) (a_1 : Grind.CommRing.Mon) (a_2 : Grind.CommRing.Poly),
        motive a_2 → motive (Grind.CommRing.Poly.add a a_1 a_2)) →
      ∀ (a : Grind.CommRing.Poly), motive a

true_implies : ∀ (p : Prop), (True → p) = p
Lean.Grind.true_imp_eq : ∀ (p : Prop), (True → p) = p

propext_iff : ∀ {a b : Prop}, a = b ↔ (a ↔ b)
eq_iff_iff : ∀ {a b : Prop}, a = b ↔ (a ↔ b)

Quotient.inductionOn : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s),
  (∀ (a : α), motive (Quotient.mk s a)) → motive q
Quotient.ind : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop},
  (∀ (a : α), motive (Quotient.mk s a)) → ∀ (q : Quotient s), motive q

List.Perm.pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {l l' : List α},
  l.Perm l' → List.Pairwise R l → (∀ {x y : α}, R x y → R y x) → List.Pairwise R l'
List.Pairwise.perm : ∀ {α : Type u_1} {R : α → α → Prop} {l l' : List α},
  List.Pairwise R l → l.Perm l' → (∀ {x y : α}, R x y → R y x) → List.Pairwise R l'

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

Nat.succ_mul_succ : ∀ (a b : Nat), a.succ * b.succ = a * b + a + b + 1
Nat.succ_mul_succ_eq : ∀ (a b : Nat), a.succ * b.succ = a * b + a + b + 1

Int.ediv_mul_cancel_of_dvd : ∀ {a b : Int}, b ∣ a → a / b * b = a
Int.ediv_mul_cancel : ∀ {a b : Int}, b ∣ a → a / b * b = a

Array.getElem?_push_size : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x)[xs.size]? = some x
Array.getElem?_push_eq : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x)[xs.size]? = some x

Int.eq_iff_le_and_ge : ∀ {x y : Int}, x = y ↔ x ≤ y ∧ y ≤ x
Int.le_antisymm_iff : ∀ {a b : Int}, a = b ↔ a ≤ b ∧ b ≤ a

Int.add_le_zero_iff_le_neg : ∀ {a b : Int}, a + b ≤ 0 ↔ a ≤ -b
Lean.Omega.Int.add_le_zero_iff_le_neg : ∀ {a b : Int}, a + b ≤ 0 ↔ a ≤ -b

Vector.any_iff_exists : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.any p = true ↔ ∃ i x, p xs[i] = true
Vector.any_eq_true : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.any p = true ↔ ∃ i x, p xs[i] = true

Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {instOrd : Ord α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF) {l : List α} {k : α}
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯).val = true}
  (contains : k ∈ t), (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯).val.getKey k h' = t.getKey k contains
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF) {l : List α} {k : α} (contains : k ∈ t)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯).val = true},
  (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯).val.getKey k h' = t.getKey k contains

Int.add_nonnneg_iff_neg_le : ∀ {a b : Int}, 0 ≤ a + b ↔ -b ≤ a
Lean.Omega.Int.add_nonnneg_iff_neg_le : ∀ {a b : Int}, 0 ≤ a + b ↔ -b ≤ a

Nat.add_sub_cancel : ∀ (n m : Nat), n + m - m = n
Nat.add_sub_self_right : ∀ (a b : Nat), a + b - b = a

Int.zero_le_neg_iff : ∀ {a : Int}, 0 ≤ -a ↔ a ≤ 0
Int.neg_nonneg : ∀ {a : Int}, 0 ≤ -a ↔ a ≤ 0

UInt64.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt8}, (-1) <<< b ||| a <<< b = (-1) <<< b
UInt8.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt8}, (-1) <<< b ||| a <<< b = (-1) <<< b

Nat.zero_lt_two : 0 < 2
Nat.two_pos : 0 < 2

Int.fdiv_mul_cancel_of_dvd : ∀ {a b : Int}, b ∣ a → a.fdiv b * b = a
Int.fdiv_mul_cancel : ∀ {a b : Int}, b ∣ a → a.fdiv b * b = a

Int.natCast_eq_zero : ∀ {n : Nat}, ↑n = 0 ↔ n = 0
Int.ofNat_eq_zero : ∀ {n : Nat}, ↑n = 0 ↔ n = 0

Std.DTreeMap.Internal.Impl.minKey!.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (size : Nat) (k : α) (v : β k) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a
Std.DTreeMap.Internal.Impl.minKey?.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (size : Nat) (k : α) (v : β k) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a

Std.DTreeMap.Internal.Impl.maxKey!.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
      (∀ (size : Nat) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l_1 r : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a
Std.DTreeMap.Internal.Impl.maxKey?.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
      (∀ (size : Nat) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l_1 r : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a

Nat.zero_lt_sub_of_lt : ∀ {i a : Nat}, i < a → 0 < a - i
Nat.sub_pos_of_lt : ∀ {m n : Nat}, m < n → 0 < n - m

Lean.Grind.CommRing.Poly.pow.induct : ∀ (motive : Nat → Prop),
  motive 0 → motive 1 → (∀ (k : Nat), (k = 0 → False) → motive k → motive k.succ) → ∀ (k : Nat), motive k
Lean.Grind.CommRing.Poly.powC.induct : ∀ (motive : Nat → Prop),
  motive 0 → motive 1 → (∀ (k : Nat), (k = 0 → False) → motive k → motive k.succ) → ∀ (k : Nat), motive k

Lean.Grind.imp_true_eq : ∀ (p : Prop), (p → True) = True
implies_true : ∀ (α : Sort u), (∀ (a : α), True) = True

Array.mem_toList : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs.toList ↔ a ∈ xs
Array.mem_toList_iff : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs.toList ↔ a ∈ xs

List.eq_toArray_iff : ∀ {α : Type u_1} {as : Array α} {bs : List α}, as = bs.toArray ↔ as.toList = bs
Array.eq_toArray : ∀ {α : Type u_1} {xs : Array α} {as : List α}, xs = as.toArray ↔ xs.toList = as

Int.ofNat_mul_ofNat : ∀ (m n : Nat), ↑m * ↑n = ↑(m * n)
Int.ofNat_mul_out : ∀ (m n : Nat), ↑m * ↑n = ↑(m * n)

Bool.of_not_eq_true : ∀ {b : Bool}, ¬b = true → b = false
eq_false_of_ne_true : ∀ {b : Bool}, ¬b = true → b = false

Nat.succ_le_iff : ∀ {m n : Nat}, m.succ ≤ n ↔ m < n
Nat.succ_le : ∀ {n m : Nat}, n.succ ≤ m ↔ n < m

Std.DTreeMap.Internal.Impl.minEntry?.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (size : Nat) (k : α) (v : β k) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a
Std.DTreeMap.Internal.Impl.minKey?.induct : ∀ {α : Type u} {β : α → Type v}
  (motive : Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (size : Nat) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
      (∀ (size : Nat) (k : α) (v : β k) (size_1 : Nat) (k_1 : α) (v_1 : β k_1)
          (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) →
            motive
              (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a

Lean.Omega.Int.add_le_zero_iff_le_neg' : ∀ {a b : Int}, a + b ≤ 0 ↔ b ≤ -a
Int.add_le_zero_iff_le_neg' : ∀ {a b : Int}, a + b ≤ 0 ↔ b ≤ -a

Nat.lt_succ_iff : ∀ {m n : Nat}, m < n.succ ↔ m ≤ n
Nat.lt_succ : ∀ {m n : Nat}, m < n.succ ↔ m ≤ n

Int.ofNat_add_out : ∀ (m n : Nat), ↑m + ↑n = ↑(m + n)
Int.ofNat_add_ofNat : ∀ (m n : Nat), ↑m + ↑n = ↑(m + n)

Vector.map_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : Nat} {f g : α → β} {xs : Vector α n},
  Vector.map f xs = Vector.map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a
Vector.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {n : Nat} {xs : Vector α n} {f g : α → β},
  Vector.map f xs = Vector.map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

Nat.zero_eq : Nat.zero = 0
Nat.ctor_eq_zero : Nat.zero = 0

Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey! l ↔
          (k == Std.Internal.List.minKey! l) = false)
Std.Internal.List.minKey!_eraseKey_eq_iff_beq_minKey!_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKey! (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey! l ↔
          (k == Std.Internal.List.minKey! l) = false)

Int.ofNat_pos : ∀ {n : Nat}, 0 < ↑n ↔ 0 < n
Lean.Omega.Int.ofNat_pos : ∀ {a : Nat}, 0 < ↑a ↔ 0 < a

Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k : α}
      {h' :
        Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l).val = true}
      (contains : k ∈ t),
      (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l).val.getKey k h' = t.getKey k contains
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α}
  {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k : α} (contains : k ∈ t)
      {h' :
        Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l).val = true},
      (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l).val.getKey k h' = t.getKey k contains

Array.flatten_toArray_map : ∀ {α : Type u_1} {L : List (List α)},
  (List.map List.toArray L).toArray.flatten = L.flatten.toArray
Array.flatten_toArray_map_toArray : ∀ {α : Type u_1} {xss : List (List α)},
  (List.map List.toArray xss).toArray.flatten = xss.flatten.toArray

Int.ofNat_one : ↑1 = 1
Int.natCast_one : ↑1 = 1

Int.natCast_nonneg : ∀ (n : Nat), 0 ≤ ↑n
Int.ofNat_nonneg : ∀ (n : Nat), 0 ≤ ↑n

List.getElem_cons_drop : ∀ {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length),
  l[i] :: List.drop (i + 1) l = List.drop i l
List.getElem_cons_drop_succ_eq_drop : ∀ {α : Type u_1} {as : List α} {i : Nat} (h : i < as.length),
  as[i] :: List.drop (i + 1) as = List.drop i as

Fin.val_mul : ∀ {n : Nat} (a b : Fin n), ↑(a * b) = ↑a * ↑b % n
Fin.coe_mul : ∀ {n : Nat} (a b : Fin n), ↑(a * b) = ↑a * ↑b % n

Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_mem_of_contains : ∀ {α : Type u} [inst : BEq α]
  [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α],
  m.val.WF →
    ∀ {l : List α} {k : α} (contains : m.contains k = true)
      {h' : (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l).val.contains k = true},
      (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains : ∀ {α : Type u} [inst : BEq α]
  [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α],
  m.val.WF →
    ∀ {l : List α} {k : α} {h' : (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l).val.contains k = true}
      (contains : m.contains k = true),
      (Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains

Lean.Omega.Int.ofNat_pow : ∀ (a b : Nat), ↑(a ^ b) = ↑a ^ b
Int.natCast_pow : ∀ (b n : Nat), ↑(b ^ n) = ↑b ^ n

Fin.val_congr : ∀ {n : Nat} {a b : Fin n}, a = b → ↑a = ↑b
Fin.val_eq_of_eq : ∀ {n : Nat} {i j : Fin n}, i = j → ↑i = ↑j

Nat.pred_le_iff : ∀ {m : Nat} {n : Nat}, m.pred ≤ n ↔ m ≤ n.succ
Nat.pred_le_iff_le_succ : ∀ {n : Nat} {m : Nat}, n.pred ≤ m ↔ n ≤ m.succ

Bool.cond_eq_ite : ∀ {α : Sort u_1} (b : Bool) (t e : α), (bif b then t else e) = if b = true then t else e
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

Lean.Grind.Bool.eq_true_of_not_eq_false' : ∀ {a : Bool}, ¬a = false → a = true
eq_true_of_ne_false : ∀ {b : Bool}, ¬b = false → b = true

Int.sign_of_add_one : ∀ (x : Nat), (↑x + 1).sign = 1
Int.sign_natCast_add_one : ∀ (n : Nat), (↑n + 1).sign = 1

Int.neg_pos : ∀ {a : Int}, 0 < -a ↔ a < 0
Int.zero_lt_neg_iff : ∀ {a : Int}, 0 < -a ↔ a < 0

Int16.not_eq_neg_sub : ∀ (a : Int16), ~~~a = -a - 1
Int16.not_eq_neg_add : ∀ (a : Int16), ~~~a = -a - 1

Int.neg_add_lt_left_of_lt_add : ∀ {a b c : Int}, a < b + c → -b + a < c
Int.neg_add_lt_of_lt_add : ∀ {a b c : Int}, a < b + c → -b + a < c

Fin.lt_iff_val_lt_val : ∀ {n : Nat} {a b : Fin n}, a < b ↔ ↑a < ↑b
Fin.lt_def : ∀ {n : Nat} {a b : Fin n}, a < b ↔ ↑a < ↑b

Nat.mul_add_mod' : ∀ (a b c : Nat), (a * b + c) % b = c % b
Nat.mul_add_mod_self_right : ∀ (a b c : Nat), (a * b + c) % b = c % b

BitVec.ne_intMin_of_msb_eq_false : ∀ {w : Nat}, 0 < w → ∀ {n : BitVec w}, n.msb = false → n ≠ BitVec.intMin w
BitVec.ne_intMin_of_lt_of_msb_false : ∀ {w : Nat} {x : BitVec w}, 0 < w → x.msb = false → x ≠ BitVec.intMin w

Vector.getElem_push_last : ∀ {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α}, (xs.push x)[n] = x
Vector.getElem_push_eq : ∀ {α : Type u_1} {n : Nat} {xs : Vector α n} {x : α}, (xs.push x)[n] = x

Nat.mul_div_cancel : ∀ (m : Nat) {n : Nat}, 0 < n → m * n / n = m
Nat.mul_div_left : ∀ (m : Nat) {n : Nat}, 0 < n → m * n / n = m

List.getLast?_eq_getLast : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
List.getLast?_eq_some_getLast : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)

Nat.lt_pred_iff : ∀ {a : Nat} {b : Nat}, a < b.pred ↔ a.succ < b
Nat.lt_pred_iff_succ_lt : ∀ {n : Nat} {m : Nat}, n < m.pred ↔ n.succ < m

Nat.zero_lt_of_ne_zero : ∀ {a : Nat}, a ≠ 0 → 0 < a
Nat.pos_of_ne_zero : ∀ {n : Nat}, n ≠ 0 → 0 < n

Int64.not_eq_neg_sub : ∀ (a : Int64), ~~~a = -a - 1
Int64.not_eq_neg_add : ∀ (a : Int64), ~~~a = -a - 1

Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.maxKeyD l fallback ↔
          (k == Std.Internal.List.maxKeyD l fallback) = false)
Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.maxKeyD l fallback ↔
          (k == Std.Internal.List.maxKeyD l fallback) = false)

seq_eq_bind_map : ∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α),
  f <*> x = do
    let x_1 ← f
    x_1 <$> x
seq_eq_bind : ∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α),
  mf <*> x = do
    let f ← mf
    f <$> x

BitVec.toInt_one : ∀ {w : Nat}, 1 < w → (1#w).toInt = 1
BitVec.toInt_one_of_lt : ∀ {w : Nat}, 1 < w → (1#w).toInt = 1

Std.Internal.List.getValue?_insertEntry_of_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α]
  {l : List ((_ : α) × β)} {k : α} {v : β}, Std.Internal.List.getValue? k (Std.Internal.List.insertEntry k v l) = some v
Std.Internal.List.getValue?_insertEntry_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α]
  {l : List ((_ : α) × β)} {k : α} {v : β}, Std.Internal.List.getValue? k (Std.Internal.List.insertEntry k v l) = some v

Lean.Grind.of_decide_eq_false : ∀ {p : Prop} {x : Decidable p}, decide p = false → p = False
eq_false_of_decide : ∀ {p : Prop} {x : Decidable p}, decide p = false → p = False

List.take_succ : ∀ {α : Type u_1} {l : List α} {i : Nat}, List.take (i + 1) l = List.take i l ++ l[i]?.toList
List.take_add_one : ∀ {α : Type u_1} {l : List α} {i : Nat}, List.take (i + 1) l = List.take i l ++ l[i]?.toList

Nat.lt_succ_of_lt : ∀ {a b : Nat}, a < b → a < b.succ
Nat.lt.step : ∀ {n m : Nat}, n < m → n < m.succ

Nat.mul_right_cancel : ∀ {n m k : Nat}, 0 < m → n * m = k * m → n = k
Nat.eq_of_mul_eq_mul_right : ∀ {n m k : Nat}, 0 < m → n * m = k * m → n = k

Vector.not_lt_iff_ge : ∀ {α : Type u_1} {n : Nat} [inst : LT α] {xs ys : Vector α n}, ¬xs < ys ↔ ys ≤ xs
Vector.not_lt : ∀ {α : Type u_1} {n : Nat} [inst : LT α] {xs ys : Vector α n}, ¬xs < ys ↔ ys ≤ xs

Array.findFinIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool},
  Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none
Vector.findFinIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool},
  Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none

Nat.mul_add_mod : ∀ (m x y : Nat), (m * x + y) % m = y % m
Nat.mul_add_mod_self_left : ∀ (a b c : Nat), (a * b + c) % a = c % a

Nat.mod_def : ∀ (m k : Nat), m % k = m - k * (m / k)
Nat.mod_eq_sub : ∀ (x w : Nat), x % w = x - w * (x / w)

Nat.add_eq_zero_iff : ∀ {n m : Nat}, n + m = 0 ↔ n = 0 ∧ m = 0
Nat.add_eq_zero : ∀ {m n : Nat}, m + n = 0 ↔ m = 0 ∧ n = 0

Lean.Grind.Bool.eq_false_of_not_eq_true' : ∀ {a : Bool}, ¬a = true → a = false
eq_false_of_ne_true : ∀ {b : Bool}, ¬b = true → b = false

List.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → β},
  List.map f l = List.map g l ↔ ∀ (a : α), a ∈ l → f a = g a
List.map_eq_map_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {l : List α} {g : α → α_1},
  List.map f l = List.map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Int.mul_le_mul_right : ∀ {a b c : Int}, 0 < a → (b * a ≤ c * a ↔ b ≤ c)
Int.mul_le_mul_iff_of_pos_right : ∀ {a b c : Int}, 0 < a → (b * a ≤ c * a ↔ b ≤ c)

Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero : ∀ {xs ys : Omega.IntList},
  (∀ (x : Int), x ∈ xs → x = 0) → xs.dot ys = 0
Lean.Omega.IntList.dot_of_left_zero : ∀ {xs ys : Omega.IntList}, (∀ (x : Int), x ∈ xs → x = 0) → xs.dot ys = 0

Nat.pow_lt_pow_right : ∀ {a m n : Nat}, 1 < a → m < n → a ^ m < a ^ n
Nat.pow_lt_pow_of_lt : ∀ {a n m : Nat}, 1 < a → n < m → a ^ n < a ^ m

Int.neg_add_le_of_le_add : ∀ {a b c : Int}, a ≤ b + c → -b + a ≤ c
Int.neg_add_le_left_of_le_add : ∀ {a b c : Int}, a ≤ b + c → -b + a ≤ c

Int.ofNat_succ_pos : ∀ (n : Nat), 0 < ↑n.succ
Int.natCast_succ_pos : ∀ (n : Nat), 0 < ↑n.succ

Option.map_id_fun : ∀ {α : Type u}, Option.map id = id
Option.map_id : ∀ {α : Type u_1}, Option.map id = id

Int.natCast_pos : ∀ {n : Nat}, 0 < ↑n ↔ 0 < n
Lean.Omega.Int.ofNat_pos : ∀ {a : Nat}, 0 < ↑a ↔ 0 < a

Array.find?_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool}
  {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach
Vector.find?_subtype : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool}
  {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map Subtype.val (Array.find? f xs) = Array.find? g xs.unattach

Vector.all_iff_forall : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true
Vector.all_eq_true : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true

Vector.all_eq_true' : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true
Vector.all_eq_true_iff_forall_mem : ∀ {α : Type u_1} {n : Nat} {p : α → Bool} {xs : Vector α n},
  xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

Nat.sub_one_sub_lt : ∀ {i n : Nat}, i < n → n - 1 - i < n
Nat.sub_one_sub_lt_of_lt : ∀ {a b : Nat}, a < b → b - 1 - a < b

String.Pos.addChar_byteIdx : ∀ (p : String.Pos) (c : Char), (p + c).byteIdx = p.byteIdx + c.utf8Size
String.pos_add_char : ∀ (p : String.Pos) (c : Char), (p + c).byteIdx = p.byteIdx + c.utf8Size

Nat.not_lt_of_le : ∀ {a b : Nat}, a ≤ b → ¬b < a
Nat.le_lt_asymm : ∀ {a b : Nat}, a ≤ b → ¬b < a

Int.natCast_ne_zero : ∀ {n : Nat}, ↑n ≠ 0 ↔ n ≠ 0
Int.ofNat_ne_zero : ∀ {n : Nat}, ↑n ≠ 0 ↔ n ≠ 0

Nat.add_one_ne : ∀ (n : Nat), n + 1 ≠ n
Nat.add_one_ne_self : ∀ (n : Nat), n + 1 ≠ n

Lean.Omega.Int.add_nonnneg_iff_neg_le' : ∀ {a b : Int}, 0 ≤ a + b ↔ -a ≤ b
Int.add_nonnneg_iff_neg_le' : ∀ {a b : Int}, 0 ≤ a + b ↔ -a ≤ b

Array.unzip_fst : ∀ {α : Type u_1} {β : Type u_2} {l : Array (α × β)}, l.unzip.fst = Array.map Prod.fst l
Array.fst_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.fst = Array.map Prod.fst xs

Int.natCast_zero : ↑0 = 0
Int.ofNat_zero : ↑0 = 0

Array.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : α → β},
  Array.map f xs = Array.map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a
Array.map_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {xs : Array α},
  Array.map f xs = Array.map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

Int.le_add_iff_sub_le : ∀ {a b c : Int}, a ≤ b + c ↔ a - c ≤ b
Lean.Omega.Int.le_add_iff_sub_le : ∀ {a b c : Int}, a ≤ b + c ↔ a - c ≤ b

Std.Internal.List.key_getValueCast_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α]
  {l : List ((a : α) × β a)} {a : α} (h : Std.Internal.List.containsKey a l = true),
  ⟨a, Std.Internal.List.getValueCast a l h⟩ ∈ l
Std.Internal.List.getValueCast_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α]
  {l : List ((a : α) × β a)} {a : α} (h : Std.Internal.List.containsKey a l = true),
  ⟨a, Std.Internal.List.getValueCast a l h⟩ ∈ l

List.contains_iff_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, l.contains a = true ↔ a ∈ l
List.contains_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {as : List α}, as.contains a = true ↔ a ∈ as

Int.natAbs_cast : ∀ (n : Nat), (↑n).natAbs = n
Int.natAbs_natCast : ∀ (n : Nat), (↑n).natAbs = n

ISize.not_eq_neg_add : ∀ (a : ISize), ~~~a = -a - 1
ISize.not_eq_neg_sub : ∀ (a : ISize), ~~~a = -a - 1

Array.getElem?_eq_none : ∀ {α : Type u_1} {i : Nat} {xs : Array α}, xs.size ≤ i → xs[i]? = none
Array.getElem?_size_le : ∀ {α : Type u_1} {xs : Array α} {i : Nat}, xs.size ≤ i → xs[i]? = none

List.min?_eq_some_iff' : ∀ {a : Nat} {xs : List Nat}, xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b
List.min?_eq_some_iff'' : ∀ {a : Nat} {xs : List Nat}, xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → a ≤ b

Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.minKeyD l fallback ↔
          (k == Std.Internal.List.minKeyD l fallback) = false)
Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α]
  [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.minKeyD l fallback ↔
          (k == Std.Internal.List.minKeyD l fallback) = false)

Int.toNat_eq_max : ∀ (a : Int), ↑a.toNat = max a 0
Int.ofNat_toNat : ∀ (a : Int), ↑a.toNat = max a 0

List.head?_eq_some_head : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head? = some (l.head h)
List.head?_eq_head : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head? = some (l.head h)

Lean.Omega.Fin.not_le : ∀ {n : Nat} {i j : Fin n}, ¬i ≤ j ↔ j < i
Fin.not_le : ∀ {n : Nat} {a b : Fin n}, ¬a ≤ b ↔ b < a

Int.tdiv_mul_cancel : ∀ {a b : Int}, b ∣ a → a.tdiv b * b = a
Int.tdiv_mul_cancel_of_dvd : ∀ {a b : Int}, b ∣ a → a.tdiv b * b = a

Int.le_add_of_neg_add_le : ∀ {a b c : Int}, -b + a ≤ c → a ≤ b + c
Int.le_add_of_neg_add_le_left : ∀ {a b c : Int}, -b + a ≤ c → a ≤ b + c

Int.eq_fdiv_of_mul_eq_right : ∀ {a b c : Int}, a ≠ 0 → a * b = c → b = c.tdiv a
Int.eq_tdiv_of_mul_eq_right : ∀ {a b c : Int}, a ≠ 0 → a * b = c → b = c.tdiv a

Nat.mul_div_cancel_left' : ∀ {a b : Nat}, a ∣ b → a * (b / a) = b
Nat.mul_div_cancel' : ∀ {n m : Nat}, n ∣ m → n * (m / n) = m

Fin.not_lt : ∀ {n : Nat} {a b : Fin n}, ¬a < b ↔ b ≤ a
Lean.Omega.Fin.not_lt : ∀ {n : Nat} {i j : Fin n}, ¬i < j ↔ j ≤ i

Array.contains_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, xs.contains a = true ↔ a ∈ xs
Array.contains_iff_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α},
  xs.contains a = true ↔ a ∈ xs

PUnit.ext : ∀ (x y : PUnit), x = y
PUnit.subsingleton : ∀ (a b : PUnit), a = b

Int.natCast_nonpos_iff : ∀ {n : Nat}, ↑n ≤ 0 ↔ n = 0
Int.natCast_le_zero : ∀ {n : Nat}, ↑n ≤ 0 ↔ n = 0

Array.push_eq_append : ∀ {α : Type u_1} {a : α} {as : Array α}, as.push a = as ++ #[a]
Array.push_eq_append_singleton : ∀ {α : Type u_1} {as : Array α} {x : α}, as.push x = as ++ #[x]

List.drop_of_length_le : ∀ {α : Type u_1} {i : Nat} {l : List α}, l.length ≤ i → List.drop i l = []
List.drop_eq_nil_of_le : ∀ {α : Type u} {as : List α} {i : Nat}, as.length ≤ i → List.drop i as = []

Quotient.inductionOn₂ : ∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β}
  {motive : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂),
  (∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) → motive q₁ q₂
Quotient.ind₂ : ∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β}
  {motive : Quotient s₁ → Quotient s₂ → Prop},
  (∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) →
    ∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), motive q₁ q₂