Loogle!

Result

Found 3171 declarations whose name contains "succ". Of these, only the first 200 are shown.

• Nat.succ 📋 Init.Prelude
  (n : ℕ) : ℕ
• Nat.le_succ 📋 Init.Prelude
  (n : ℕ) : n ≤ n.succ
• Nat.lt_succ_self 📋 Init.Prelude
  (n : ℕ) : n < n.succ
• Nat.not_succ_le_self 📋 Init.Prelude
  (n : ℕ) : ¬n.succ ≤ n
• Nat.ctorIdx_succ 📋 Init.Prelude
  {n : ℕ} : n.succ.ctorIdx = 1
• Nat.succ_pos 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.zero_lt_succ 📋 Init.Prelude
  (n : ℕ) : 0 < n.succ
• Nat.not_succ_le_zero 📋 Init.Prelude
  (n : ℕ) : n.succ ≤ 0 → False
• Nat.le_of_lt_succ 📋 Init.Prelude
  {m n : ℕ} : m < n.succ → m ≤ n
• Nat.le_succ_of_le 📋 Init.Prelude
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• Nat.lt_succ_of_le 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n < m.succ
• Nat.le_of_succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n.succ ≤ m.succ → n ≤ m
• Nat.succ_le_succ 📋 Init.Prelude
  {n m : ℕ} : n ≤ m → n.succ ≤ m.succ
• Nat.ble_succ_eq_true 📋 Init.Prelude
  {n m : ℕ} : n.ble m = true → n.ble m.succ = true
• Nat.succ_sub_succ_eq_sub 📋 Init.Prelude
  (n m : ℕ) : n.succ - m.succ = n - m
• Lean.Parser.Tactic.failIfSuccess 📋 Init.Tactics
  : Lean.ParserDescr
• Nat.succ.inj 📋 Init.Core
  {m n : ℕ} : m.succ = n.succ → m = n
• Nat.succ.injEq 📋 Init.Core
  (u v : ℕ) : (u.succ = v.succ) = (u = v)
• Lean.Parser.Tactic.Grind.failIfSuccess 📋 Init.Grind.Interactive
  : Lean.ParserDescr
• Nat.succ_ne_self 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ ≠ n
• Nat.pred_succ 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ.pred = n
• Nat.succ_ne_zero 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ ≠ 0
• Nat.succ_succ_ne_one 📋 Init.Data.Nat.Basic
  (a : ℕ) : a.succ.succ ≠ 1
• Nat.le_of_succ_le 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n.succ ≤ m) : n ≤ m
• Nat.lt_of_succ_le 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n.succ ≤ m) : n < m
• Nat.lt_of_succ_lt 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n.succ < m → n < m
• Nat.lt_succ_of_lt 📋 Init.Data.Nat.Basic
  {a b : ℕ} (h : a < b) : a < b.succ
• Nat.succ_inj 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a.succ = b.succ ↔ a = b
• Nat.succ_le_of_lt 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n < m) : n.succ ≤ m
• Nat.succ_ne_succ_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a.succ ≠ b.succ ↔ a ≠ b
• Nat.lt_of_succ_lt_succ 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n.succ < m.succ → n < m
• Nat.lt_pred_of_succ_lt 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n.succ < m → n < m.pred
• Nat.lt_succ 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m < n.succ ↔ m ≤ n
• Nat.lt_succ_iff 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m < n.succ ↔ m ≤ n
• Nat.pred_le_of_le_succ 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n ≤ m.succ → n.pred ≤ m
• Nat.succ_le_iff 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m.succ ≤ n ↔ m < n
• Nat.succ_lt_succ 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n < m → n.succ < m.succ
• Nat.succ_lt_of_lt_pred 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n < m.pred → n.succ < m
• Nat.le_succ_of_pred_le 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n.pred ≤ m → n ≤ m.succ
• Nat.succ_le_succ_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a.succ ≤ b.succ ↔ a ≤ b
• Nat.succ_lt_succ_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a.succ < b.succ ↔ a < b
• Nat.succ_pred 📋 Init.Data.Nat.Basic
  {a : ℕ} (h : a ≠ 0) : a.pred.succ = a
• Nat.lt_pred_iff_succ_lt 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n < m.pred ↔ n.succ < m
• Nat.pred_le_iff_le_succ 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n.pred ≤ m ↔ n ≤ m.succ
• Nat.succ_pred_eq_of_ne_zero 📋 Init.Data.Nat.Basic
  {n : ℕ} : n ≠ 0 → n.pred.succ = n
• Nat.exists_eq_succ_of_ne_zero 📋 Init.Data.Nat.Basic
  {n : ℕ} : n ≠ 0 → ∃ k, n = k.succ
• Nat.succ_pred_eq_of_pos 📋 Init.Data.Nat.Basic
  {n : ℕ} : 0 < n → n.pred.succ = n
• Nat.eq_zero_or_eq_succ_pred 📋 Init.Data.Nat.Basic
  (n : ℕ) : n = 0 ∨ n = n.pred.succ
• Nat.succ_eq_add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ = n + 1
• Nat.le_or_eq_of_le_succ 📋 Init.Data.Nat.Basic
  {m n : ℕ} (h : m ≤ n.succ) : m ≤ n ∨ m = n.succ
• Nat.lt_succ_iff_lt_or_eq 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m < n.succ ↔ m < n ∨ m = n
• Nat.instNeZeroSucc 📋 Init.Data.Nat.Basic
  {n : ℕ} : NeZero (n + 1)
• Nat.lt_of_sub_eq_succ 📋 Init.Data.Nat.Basic
  {m n l : ℕ} (h : m - n = l.succ) : n < m
• Nat.add_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n + m.succ = (n + m).succ
• Nat.sub_le_succ_sub 📋 Init.Data.Nat.Basic
  (a i : ℕ) : a - i ≤ a.succ - i
• Nat.sub_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n - m.succ = (n - m).pred
• Nat.succ_add 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.succ + m = (n + m).succ
• Nat.succ_sub_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.succ - m.succ = n - m
• Nat.eq_of_le_of_lt_succ 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n
• Nat.eq_of_lt_succ_of_not_lt 📋 Init.Data.Nat.Basic
  {m n : ℕ} (hmn : m < n + 1) (h : ¬m < n) : m = n
• Nat.succ_sub 📋 Init.Data.Nat.Basic
  {m n : ℕ} (h : n ≤ m) : m.succ - n = (m - n).succ
• Nat.mul_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * m.succ = n * m + n
• Nat.succ_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.succ * m = n * m + m
• Nat.pow_succ 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n ^ m.succ = n ^ m * n
• Nat.sub_succ_lt_self 📋 Init.Data.Nat.Basic
  (a i : ℕ) (h : i < a) : a - (i + 1) < a - i
• Int.negSucc 📋 Init.Data.Int.Basic
  : ℕ → ℤ
• List.modifyTailIdx_succ_nil 📋 Init.Data.List.Basic
  {α : Type u} {f : List α → List α} {i : ℕ} : [].modifyTailIdx (i + 1) f = []
• List.replicate_succ 📋 Init.Data.List.Basic
  {α : Type u} {a : α} {n : ℕ} : List.replicate (n + 1) a = a :: List.replicate n a
• List.drop_succ_cons 📋 Init.Data.List.Basic
  {α : Type u} {a : α} {l : List α} {i : ℕ} : List.drop (i + 1) (a :: l) = List.drop i l
• List.eraseIdx_cons_succ 📋 Init.Data.List.Basic
  {α✝ : Type u_1} {a : α✝} {as : List α✝} {i : ℕ} : (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i
• List.take_succ_cons 📋 Init.Data.List.Basic
  {α : Type u} {a : α} {as : List α} {i : ℕ} : List.take (i + 1) (a :: as) = a :: List.take i as
• List.range'_succ 📋 Init.Data.List.Basic
  {s n step : ℕ} : List.range' s (n + 1) step = s :: List.range' (s + step) n step
• List.modifyTailIdx_succ_cons 📋 Init.Data.List.Basic
  {α : Type u} {f : List α → List α} {i : ℕ} {a : α} {l : List α} : (a :: l).modifyTailIdx (i + 1) f = a :: l.modifyTailIdx i f
• Nat.shiftRight_succ 📋 Init.Data.Nat.Bitwise.Basic
  (m n : ℕ) : m >>> (n + 1) = m >>> n / 2
• Fin.castSucc 📋 Init.Data.Fin.Basic
  {n : ℕ} : Fin n → Fin (n + 1)
• Fin.succ 📋 Init.Data.Fin.Basic
  {n : ℕ} : Fin n → Fin (n + 1)
• List.getElem_cons_drop_succ_eq_drop 📋 Init.GetElem
  {α : Type u_1} {as : List α} {i : ℕ} (h : i < as.length) : as[i] :: List.drop (i + 1) as = List.drop i as
• List.getElem_cons_succ 📋 Init.GetElem
  {α : Type u_1} (a : α) (as : List α) (i : ℕ) (h : i + 1 < (a :: as).length) : (a :: as)[i + 1] = as[i]
• Lean.Parser.Tactic.Conv.failIfSuccess 📋 Init.Conv
  : Lean.ParserDescr
• Int.negSucc_emod_ofNat 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a % ↑b = Int.subNatNat b (a % b).succ
• Int.negSucc_ediv_ofNat_succ 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a / ↑(b + 1) = Int.negSucc (a / b.succ)
• Int.ofNat_ediv_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.ofNat a / Int.negSucc b = -↑(a / (b + 1))
• Int.negSucc_ediv_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a / Int.negSucc b = ↑(a / (b + 1) + 1)
• Int.negSucc_emod_negSucc 📋 Init.Data.Int.DivMod.Basic
  {a b : ℕ} : Int.negSucc a % Int.negSucc b = Int.subNatNat (b + 1) (a % (b + 1)).succ
• Int.negSucc_ne_zero 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n ≠ 0
• Int.zero_ne_negSucc 📋 Init.Data.Int.Lemmas
  (n : ℕ) : 0 ≠ Int.negSucc n
• Int.negSucc_inj 📋 Init.Data.Int.Lemmas
  {m n : ℕ} : Int.negSucc m = Int.negSucc n ↔ m = n
• Int.neg_ofNat_succ 📋 Init.Data.Int.Lemmas
  (n : ℕ) : -↑n.succ = Int.negSucc n
• Int.negSucc_add_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m + ↑n = Int.subNatNat n m.succ
• Int.ofNat_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m + Int.negSucc n = Int.subNatNat m n.succ
• Int.subNatNat_of_sub_eq_succ 📋 Init.Data.Int.Lemmas
  {m n k : ℕ} (h : n - m = k.succ) : Int.subNatNat m n = Int.negSucc k
• Int.natCast_succ 📋 Init.Data.Int.Lemmas
  (n : ℕ) : ↑n.succ = ↑n + 1
• Int.negSucc_eq 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n = -(↑n + 1)
• Int.neg_negSucc 📋 Init.Data.Int.Lemmas
  (n : ℕ) : -Int.negSucc n = ↑(n + 1)
• Int.negOfNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)
• Int.negSucc_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m + Int.negSucc n = Int.negSucc (m + n).succ
• Int.negSucc_mul_negOfNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negOfNat n = Int.ofNat (m.succ * n)
• Int.subNatNat_add_negSucc 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + k.succ)
• Int.negSucc_add_one_eq_neg_ofNat_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : Int.negSucc a + 1 = -↑b ↔ a = b
• Int.negSucc_eq_neg_ofNat_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : Int.negSucc a = -↑b ↔ a + 1 = b
• Int.neg_ofNat_eq_negSucc_add_one_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : -↑a = Int.negSucc b + 1 ↔ a = b
• Int.neg_ofNat_eq_negSucc_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : -↑a = Int.negSucc b ↔ a = b + 1
• Int.negSucc_sub_one 📋 Init.Data.Int.Lemmas
  (n : ℕ) : Int.negSucc n - 1 = Int.negSucc (n + 1)
• Int.ofNat_add_negSucc_of_lt 📋 Init.Data.Int.Lemmas
  {m n : ℕ} (h : m < n.succ) : Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)
• Int.negSucc_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * Int.negSucc n = ↑m.succ * ↑n.succ
• Int.negSucc_mul_ofNat 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : Int.negSucc m * ↑n = -↑(m.succ * n)
• Int.ofNat_mul_negSucc 📋 Init.Data.Int.Lemmas
  (m n : ℕ) : ↑m * Int.negSucc n = -↑(m * n.succ)
• Int.negSucc_mul_subNatNat 📋 Init.Data.Int.Lemmas
  (m n k : ℕ) : Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
• Int.natAbs_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : (Int.negSucc n).natAbs = n.succ
• Int.negSucc_le_zero 📋 Init.Data.Int.Order
  (n : ℕ) : Int.negSucc n ≤ 0
• Int.negSucc_lt_zero 📋 Init.Data.Int.Order
  (n : ℕ) : Int.negSucc n < 0
• Int.toNat_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : (Int.negSucc n).toNat = 0
• Int.negSucc_not_nonneg 📋 Init.Data.Int.Order
  (n : ℕ) : 0 ≤ Int.negSucc n ↔ False
• Int.negSucc_not_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < Int.negSucc n ↔ False
• Int.ofNat_succ_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < ↑n.succ
• Int.sign_negSucc 📋 Init.Data.Int.Order
  (x : ℕ) : (Int.negSucc x).sign = -1
• Int.eq_negSucc_of_lt_zero 📋 Init.Data.Int.Order
  {a : ℤ} : a < 0 → ∃ n, a = Int.negSucc n
• Int.lt_succ 📋 Init.Data.Int.Order
  (a : ℤ) : a < a + 1
• Int.negSucc_max_zero 📋 Init.Data.Int.Order
  (n : ℕ) : max (Int.negSucc n) 0 = 0
• Int.zero_max_negSucc 📋 Init.Data.Int.Order
  (n : ℕ) : max 0 (Int.negSucc n) = 0
• Int.succ_ofNat_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < ↑n + 1
• Int.lt_add_succ 📋 Init.Data.Int.Order
  (a : ℤ) (n : ℕ) : a < a + (↑n + 1)
• Int.eq_succ_of_zero_lt 📋 Init.Data.Int.Order
  {a : ℤ} (h : 0 < a) : ∃ n, a = ↑n + 1
• Nat.gcd_succ 📋 Init.Data.Nat.Gcd
  (x y : ℕ) : x.succ.gcd y = (y % x.succ).gcd x.succ
• Lean.Omega.IntList.get_cons_succ 📋 Init.Omega.IntList
  {x : ℤ} {xs : List ℤ} {i : ℕ} : Lean.Omega.IntList.get (x :: xs) (i + 1) = Lean.Omega.IntList.get xs i
• Lean.Omega.IntList.set_cons_succ 📋 Init.Omega.IntList
  {x : ℤ} {xs : List ℤ} {i : ℕ} {y : ℤ} : Lean.Omega.IntList.set (x :: xs) (i + 1) y = x :: Lean.Omega.IntList.set xs i y
• Lean.Omega.IntList.set_nil_succ 📋 Init.Omega.IntList
  {i : ℕ} {y : ℤ} : Lean.Omega.IntList.set [] (i + 1) y = 0 :: Lean.Omega.IntList.set [] i y
• Nat.mod_pow_succ 📋 Init.Data.Nat.Mod
  {x b k : ℕ} : x % b ^ (k + 1) = x % b ^ k + b ^ k * (x / b ^ k % b)
• Nat.not_succ_lt_self 📋 Init.Data.Nat.Lemmas
  {n : ℕ} : ¬n.succ < n
• Nat.one_lt_succ_succ 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : 1 < n.succ.succ
• Nat.pred_eq_of_eq_succ 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} (H : m = n.succ) : m.pred = n
• Nat.succ_ne_succ 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m.succ ≠ n.succ ↔ m ≠ n
• Nat.mod_succ 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : n % n.succ = n
• Nat.succ_le 📋 Init.Data.Nat.Lemmas
  {n m : ℕ} : n.succ ≤ m ↔ n < m
• Nat.sub_lt_succ 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : a - b < a.succ
• Nat.succ_max_succ 📋 Init.Data.Nat.Lemmas
  (x y : ℕ) : max x.succ y.succ = (max x y).succ
• Nat.succ_min_succ 📋 Init.Data.Nat.Lemmas
  (x y : ℕ) : min x.succ y.succ = (min x y).succ
• Nat.succ_eq_one_add 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : n.succ = 1 + n
• Nat.succ_sub_one 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : n.succ - 1 = n
• Nat.le_succ_iff 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ
• Nat.mod_succ_eq_iff_lt 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m % n.succ = m ↔ m < n.succ
• Nat.succ_add_eq_add_succ 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : a.succ + b = a + b.succ
• Nat.succ_mul_pos 📋 Init.Data.Nat.Lemmas
  {n : ℕ} (m : ℕ) (hn : 0 < n) : 0 < m.succ * n
• Nat.add_succ_sub_one 📋 Init.Data.Nat.Lemmas
  (m n : ℕ) : m + n.succ - 1 = m + n
• Nat.forall_lt_succ_right 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : ℕ → Prop} : (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n
• Nat.sub_succ' 📋 Init.Data.Nat.Lemmas
  (m n : ℕ) : m - n.succ = m - n - 1
• Nat.succ_add_sub_one 📋 Init.Data.Nat.Lemmas
  (n m : ℕ) : m.succ + n - 1 = m + n
• Nat.pow_succ' 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m ^ n.succ = m * m ^ n
• Nat.exists_lt_succ_right 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : ℕ → Prop} : (∃ m < n + 1, p m) ↔ (∃ m < n, p m) ∨ p n
• Nat.succ_sub_sub_succ 📋 Init.Data.Nat.Lemmas
  (n m k : ℕ) : n.succ - m - k.succ = n - m - k
• Nat.lt_mul_div_succ 📋 Init.Data.Nat.Lemmas
  {b : ℕ} (a : ℕ) (hb : 0 < b) : a < b * (a / b + 1)
• Nat.shiftLeft_succ 📋 Init.Data.Nat.Lemmas
  (m n : ℕ) : m <<< (n + 1) = 2 * m <<< n
• Nat.shiftLeft_succ_inside 📋 Init.Data.Nat.Lemmas
  (m n : ℕ) : m <<< (n + 1) = (2 * m) <<< n
• Nat.shiftRight_succ_inside 📋 Init.Data.Nat.Lemmas
  (m n : ℕ) : m >>> (n + 1) = (m / 2) >>> n
• Nat.add_succ_lt_add 📋 Init.Data.Nat.Lemmas
  {a b c d : ℕ} (hab : a < b) (hcd : c < d) : a + c + 1 < b + d
• Nat.not_dvd_of_lt_of_lt_mul_succ 📋 Init.Data.Nat.Lemmas
  {n k m : ℕ} (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m
• Nat.pred_eq_succ_iff 📋 Init.Data.Nat.Lemmas
  {n m : ℕ} : n - 1 = m + 1 ↔ n = m + 2
• Nat.pow_lt_pow_succ 📋 Init.Data.Nat.Lemmas
  {a n : ℕ} (h : 1 < a) : a ^ n < a ^ (n + 1)
• Nat.forall_lt_succ_left 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : ℕ → Prop} : (∀ m < n + 1, p m) ↔ p 0 ∧ ∀ m < n, p (m + 1)
• Nat.succ_mul_succ 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : a.succ * b.succ = a * b + a + b + 1
• Nat.succ_mul_succ_eq 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : a.succ * b.succ = a * b + a + b + 1
• Nat.exists_lt_succ_left 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : ℕ → Prop} : (∃ m < n + 1, p m) ↔ p 0 ∨ ∃ m < n, p (m + 1)
• Nat.forall_lt_succ_right' 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop} : (∀ (m : ℕ) (h : m < n + 1), p m h) ↔ (∀ (m : ℕ) (h : m < n), p m ⋯) ∧ p n ⋯
• Nat.not_dvd_iff_lt_mul_succ 📋 Init.Data.Nat.Lemmas
  (n : ℕ) {a : ℕ} (ha : 0 < a) : ¬a ∣ n ↔ ∃ k, a * k < n ∧ n < a * (k + 1)
• Nat.mul_lt_mul_pow_succ 📋 Init.Data.Nat.Lemmas
  {a b n : ℕ} (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)
• Nat.succ_mod_succ_eq_zero_iff 📋 Init.Data.Nat.Lemmas
  {a b : ℕ} : (a + 1) % (b + 1) = 0 ↔ a % (b + 1) = b
• Nat.two_pow_succ 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n
• Nat.forall_lt_succ_left' 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop} : (∀ (m : ℕ) (h : m < n + 1), p m h) ↔ p 0 ⋯ ∧ ∀ (m : ℕ) (h : m < n), p (m + 1) ⋯
• Nat.exists_lt_succ_right' 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop} : (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m ⋯) ∨ p n ⋯
• Nat.exists_lt_succ_left' 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop} : (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 ⋯ ∨ ∃ m, ∃ (h : m < n), p (m + 1) ⋯
• Nat.succ_div_of_not_dvd 📋 Init.Data.Nat.Div.Lemmas
  {a b : ℕ} (h : ¬b ∣ a + 1) : (a + 1) / b = a / b
• Nat.succ_div_of_mod_ne_zero 📋 Init.Data.Nat.Div.Lemmas
  {a b : ℕ} (h : (a + 1) % b ≠ 0) : (a + 1) / b = a / b
• Nat.succ_div_of_dvd 📋 Init.Data.Nat.Div.Lemmas
  {a b : ℕ} (h : b ∣ a + 1) : (a + 1) / b = a / b + 1
• Nat.succ_div_of_mod_eq_zero 📋 Init.Data.Nat.Div.Lemmas
  {a b : ℕ} (h : (a + 1) % b = 0) : (a + 1) / b = a / b + 1
• Nat.succ_div 📋 Init.Data.Nat.Div.Lemmas
  {a b : ℕ} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
• Int.pow_succ 📋 Init.Data.Int.Pow
  (m : ℤ) (n : ℕ) : m ^ n.succ = m ^ n * m
• Int.pow_succ' 📋 Init.Data.Int.Pow
  (b : ℤ) (e : ℕ) : b ^ (e + 1) = b * b ^ e
• Int.negSucc_pow 📋 Init.Data.Int.Pow
  (m n : ℕ) : Int.negSucc m ^ n = if n % 2 = 0 then Int.ofNat (m.succ ^ n) else Int.negOfNat (m.succ ^ n)
• Nat.testBit_succ 📋 Init.Data.Nat.Bitwise.Lemmas
  (x i : ℕ) : x.testBit i.succ = (x / 2).testBit i
• Nat.testBit_two_pow_sub_succ 📋 Init.Data.Nat.Bitwise.Lemmas
  {x n : ℕ} (h₂ : x < 2 ^ n) (i : ℕ) : (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
• Fin.coe_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) : ↑i.castSucc = ↑i
• Fin.val_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) : ↑i.castSucc = ↑i
• Fin.castSucc_inj 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b
• Fin.succ_inj 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a.succ = b.succ ↔ a = b
• Fin.castLT_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a : Fin n) (h : ↑a < n) : a.castSucc.castLT h = a
• Fin.cast_succ_eq 📋 Init.Data.Fin.Lemmas
  {n n' : ℕ} (i : Fin n) (h : n.succ = n'.succ) : Fin.cast h i.succ = (Fin.cast ⋯ i).succ
• Fin.castSucc_lt_last 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a : Fin n) : a.castSucc < Fin.last n
• Fin.val_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (j : Fin n) : ↑j.succ = ↑j + 1
• Fin.castSucc_lt_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin n} : i.castSucc < i.succ
• Fin.lt_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a : Fin n} : a.castSucc < a.succ
• Fin.rev_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (k : Fin n) : k.castSucc.rev = k.rev.succ
• Fin.rev_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (k : Fin n) : k.succ.rev = k.rev.castSucc
• Fin.succ_eq_last_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin n.succ} : i.succ = Fin.last (n + 1) ↔ i = Fin.last n
• Fin.castSucc_mk 📋 Init.Data.Fin.Lemmas
  (n i : ℕ) (h : i < n) : ⟨i, h⟩.castSucc = ⟨i, ⋯⟩
• Fin.succ_last 📋 Init.Data.Fin.Lemmas
  (n : ℕ) : (Fin.last n).succ = Fin.last n.succ
• Fin.castSucc_lt_castSucc_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a.castSucc < b.castSucc ↔ a < b
• Fin.succ_le_succ_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b
• Fin.succ_lt_succ_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n} : a.succ < b.succ ↔ a < b
• Fin.castSucc_castLE 📋 Init.Data.Fin.Lemmas
  {n m : ℕ} (h : n ≤ m) (i : Fin n) : (Fin.castLE h i).castSucc = Fin.castLE ⋯ i
• Fin.lastCases_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {last : motive (Fin.last n)} {cast : (i : Fin n) → motive i.castSucc} (i : Fin n) : Fin.lastCases last cast i.castSucc = cast i

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 401c76f serving mathlib revision b87935d