Loogle!

Result

Found 1208 declarations mentioning Nat.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.le.step 📋 Init.Prelude
  {n m : ℕ} : n.le m → n.le m.succ
• 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
• 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)
• 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.lt.base 📋 Init.Data.Nat.Basic
  (n : ℕ) : n < n.succ
• 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.le_step 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n ≤ m) : n ≤ m.succ
• 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.recCompiled 📋 Init.Data.Nat.Basic
  {motive : ℕ → Sort u} (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) (t : ℕ) : motive t
• 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.step 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n < m → n < m.succ
• 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 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n < m.pred ↔ n.succ < m
• Nat.lt_pred_iff_succ_lt 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n < m.pred ↔ n.succ < m
• Nat.pred_le_iff 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n.pred ≤ m ↔ n ≤ m.succ
• Nat.pred_le_iff_le_succ 📋 Init.Data.Nat.Basic
  {n : ℕ} {m : ℕ} : n.pred ≤ m ↔ n ≤ m.succ
• Nat.rec_eq_recCompiled 📋 Init.Data.Nat.Basic
  : @Nat.rec = @Nat.recCompiled
• 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.add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 = n.succ
• 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.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.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.caseStrongRecOn 📋 Init.WF
  {motive : ℕ → Sort u} (a : ℕ) (zero : motive 0) (ind : (n : ℕ) → ((m : ℕ) → m ≤ n → motive m) → motive n.succ) : motive a
• 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.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.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.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.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.ofNat_succ_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < ↑n.succ
• Int.lt.dest 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a < b) : ∃ n, a + ↑n.succ = b
• Nat.gcd_succ 📋 Init.Data.Nat.Gcd
  (x y : ℕ) : x.succ.gcd y = (y % x.succ).gcd x.succ
• 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.one_add 📋 Init.Data.Nat.Lemmas
  (n : ℕ) : 1 + n = n.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.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.succ_sub_sub_succ 📋 Init.Data.Nat.Lemmas
  (n m k : ℕ) : n.succ - m - k.succ = n - m - k
• 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
• Int.pow_succ 📋 Init.Data.Int.Pow
  (m : ℤ) (n : ℕ) : m ^ n.succ = m ^ n * m
• 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
• 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.castLE_zero 📋 Init.Data.Fin.Lemmas
  {n m : ℕ} (h : n.succ ≤ m.succ) : Fin.castLE h 0 = 0
• 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.succ_last 📋 Init.Data.Fin.Lemmas
  (n : ℕ) : (Fin.last n).succ = Fin.last n.succ
• Fin.pred_le_pred_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} : a.pred ha ≤ b.pred hb ↔ a ≤ b
• Fin.pred_lt_pred_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} : a.pred ha < b.pred hb ↔ a < b
• Fin.val_add_one_of_lt 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin n.succ} (h : i < Fin.last n) : ↑(i + 1) = ↑i + 1
• Fin.succRec 📋 Init.Data.Fin.Lemmas
  {motive : (n : ℕ) → Fin n → Sort u_1} (zero : (n : ℕ) → motive n.succ 0) (succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ) {n : ℕ} (i : Fin n) : motive n i
• Fin.succRecOn 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) {motive : (n : ℕ) → Fin n → Sort u_1} (zero : (n : ℕ) → motive (n + 1) 0) (succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ) : motive n i
• Fin.castLE_succ 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} (h : m + 1 ≤ n + 1) (i : Fin m) : Fin.castLE h i.succ = (Fin.castLE ⋯ i).succ
• Fin.mk_succ_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : ℕ) (h : i < n) : 0 < ⟨i.succ, ⋯⟩
• Fin.succRecOn_succ 📋 Init.Data.Fin.Lemmas
  {motive : (n : ℕ) → Fin n → Sort u_1} {zero : (n : ℕ) → motive (n + 1) 0} {succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ} {n : ℕ} (i : Fin n) : i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)
• Fin.cases_succ' 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} {i : ℕ} (h : i + 1 < n + 1) : Fin.cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩
• Fin.succRecOn_zero 📋 Init.Data.Fin.Lemmas
  {motive : (n : ℕ) → Fin n → Sort u_1} {zero : (n : ℕ) → motive (n + 1) 0} {succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ} (n : ℕ) : Fin.succRecOn 0 zero succ = zero n
• List.getElem_cons 📋 Init.Data.List.Lemmas
  {α : Type u_1} {i : ℕ} {a : α} {l : List α} (w : i < (a :: l).length) : (a :: l)[i] = if h : i = 0 then a else l[i - 1]
• List.IsPrefix.getElem 📋 Init.Data.List.Sublist
  {α : Type u_1} {xs ys : List α} (h : xs <+: ys) {i : ℕ} (hi : i < xs.length) : xs[i] = ys[i]
• Int.emod_negSucc 📋 Init.Data.Int.DivMod.Lemmas
  (m : ℕ) (n : ℤ) : Int.negSucc m % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
• Int.natCast_succ_pos 📋 Init.Data.Int.LemmasAux
  (n : ℕ) : 0 < ↑n.succ
• Int.ofNat_add_one_out 📋 Init.Data.Int.LemmasAux
  (n : ℕ) : ↑n + 1 = ↑n.succ
• List.range_succ 📋 Init.Data.List.Range
  {n : ℕ} : List.range n.succ = List.range n ++ [n]
• List.range_succ_eq_map 📋 Init.Data.List.Range
  {n : ℕ} : List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
• List.not_of_lt_findIdx 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} (h : i < List.findIdx p xs) : p xs[i] = false
• Std.Iter.atIdxSlow?.induct_unfolding 📋 Init.Data.Iterators.Consumers.Access
  {α β : Type u} [Std.Iterator α Id β] [Std.Iterators.Productive α Id] (motive : ℕ → Std.Iter β → Option β → Prop) (yield_zero : ∀ (it it' : Std.Iter β) (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out)), it.step = ⟨Std.IterStep.yield it' out, property⟩ → motive 0 it (some out)) (yield_succ : ∀ (it it' : Std.Iter β) (out : β) (property : it.IsPlausibleStep (Std.IterStep.yield it' out)), it.step = ⟨Std.IterStep.yield it' out, property⟩ → ∀ (k : ℕ), motive k it' (Std.Iter.atIdxSlow? k it') → motive k.succ it (Std.Iter.atIdxSlow? k it')) (skip_case : ∀ (n : ℕ) (it it' : Std.Iter β) (property : it.IsPlausibleStep (Std.IterStep.skip it')), it.step = ⟨Std.IterStep.skip it', property⟩ → motive n it' (Std.Iter.atIdxSlow? n it') → motive n it (Std.Iter.atIdxSlow? n it')) (done_case : ∀ (n : ℕ) (it : Std.Iter β) (property : it.IsPlausibleStep Std.IterStep.done), it.step = ⟨Std.IterStep.done, property⟩ → motive n it none) (n : ℕ) (it : Std.Iter β) : motive n it (Std.Iter.atIdxSlow? n it)
• Array.not_of_lt_findIdx 📋 Init.Data.Array.Find
  {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < Array.findIdx p xs) : p xs[i] = false
• Array.range_succ 📋 Init.Data.Array.Range
  {n : ℕ} : Array.range n.succ = Array.range n ++ #[n]
• Array.range_succ_eq_map 📋 Init.Data.Array.Range
  {n : ℕ} : Array.range (n + 1) = #[0] ++ Array.map Nat.succ (Array.range n)
• Subarray.split 📋 Init.Data.Array.Subarray.Split
  {α : Type u_1} (s : Subarray α) (i : Fin (Std.Slice.size s).succ) : Subarray α × Subarray α
• Vector.range_succ 📋 Init.Data.Vector.Range
  {n : ℕ} : Vector.range n.succ = Vector.range n ++ #v[n]
• Vector.range_succ_eq_map 📋 Init.Data.Vector.Range
  {n : ℕ} : Vector.range (n + 1) = Vector.cast ⋯ (#v[0] ++ Vector.map Nat.succ (Vector.range n))
• Std.IterM.step_drop 📋 Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
  {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Std.Iterator α m β] {n : ℕ} {it : Std.IterM m β} : (Std.IterM.drop n it).step = do let __do_lift ← it.step match __do_lift.inflate with | ⟨Std.IterStep.yield it' out, h⟩ => match h' : n with | 0 => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.drop 0 it') out ⋯)) | k.succ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.drop k it') ⋯)) | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.drop n it') ⋯)) | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
• Std.Time.Internal.Bounded.LE.ofFin 📋 Std.Time.Internal.Bounded
  {hi : ℕ} (fin : Fin hi.succ) : Std.Time.Internal.Bounded.LE 0 ↑hi
• Std.Time.Internal.Bounded.LE.ofFin' 📋 Std.Time.Internal.Bounded
  {hi lo : ℕ} (fin : Fin hi.succ) (h : lo ≤ hi) : Std.Time.Internal.Bounded.LE ↑lo ↑hi
• Fin.dfoldlM_loop_eq 📋 Batteries.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} [Monad m] (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (x : α ⟨n, ⋯⟩) : Fin.dfoldlM.loop n α f n ⋯ x = pure x
• Nat.log2_eq_succ_log2_shiftRight 📋 Mathlib.Data.Nat.BinaryRec
  {n : ℕ} (hn : n >>> 1 ≠ 0) : n.log2 = (n >>> 1).log2.succ
• DivInvMonoid.zpow_neg' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• SubNegMonoid.zsmul_neg' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : SubNegMonoid G] (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• DivInvMonoid.zpow_succ' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• SubNegMonoid.zsmul_succ' 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [self : SubNegMonoid G] (n : ℕ) (a : G) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• DivInvMonoid.mk 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [toMonoid : Monoid G] [toInv : Inv G] [toDiv : Div G] (div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G → G) (zpow_zero' : ∀ (a : G), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) : DivInvMonoid G
• SubNegMonoid.mk 📋 Mathlib.Algebra.Group.Defs
  {G : Type u} [toAddMonoid : AddMonoid G] [toNeg : Neg G] [toSub : Sub G] (sub_eq_add_neg : ∀ (a b : G), a - b = a + -b := by intros; rfl) (zsmul : ℤ → G → G) (zsmul_zero' : ∀ (a : G), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : G), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : G), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) : SubNegMonoid G
• Function.iterate_succ_apply 📋 Mathlib.Logic.Function.Iterate
  {α : Type u} (f : α → α) (n : ℕ) (x : α) : f^[n.succ] x = f^[n] (f x)
• Function.iterate_succ_apply' 📋 Mathlib.Logic.Function.Iterate
  {α : Type u} (f : α → α) (n : ℕ) (x : α) : f^[n.succ] x = f (f^[n] x)
• Function.iterate_succ 📋 Mathlib.Logic.Function.Iterate
  {α : Type u} (f : α → α) (n : ℕ) : f^[n.succ] = f^[n] ∘ f
• Function.iterate_succ' 📋 Mathlib.Logic.Function.Iterate
  {α : Type u} (f : α → α) (n : ℕ) : f^[n.succ] = f ∘ f^[n]
• pairwise_fin_succ_iff_of_isSymm 📋 Mathlib.Logic.Pairwise
  {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} [Std.Symm R] : Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j => R i.succ j.succ
• pairwise_fin_succ_iff 📋 Mathlib.Logic.Pairwise
  {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} : Pairwise R ↔ (∀ (i : Fin n), R i.succ 0) ∧ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j => R i.succ j.succ
• Nat.succ_pos' 📋 Mathlib.Data.Nat.Init
  {n : ℕ} : 0 < n.succ
• LT.lt.nat_succ_le 📋 Mathlib.Data.Nat.Init
  {n m : ℕ} (h : n < m) : n.succ ≤ m
• Nat.of_le_succ 📋 Mathlib.Data.Nat.Init
  {m n : ℕ} : m ≤ n.succ → m ≤ n ∨ m = n.succ
• Nat.pincerRecursion 📋 Mathlib.Data.Nat.Init
  {P : ℕ → ℕ → Sort u_1} (Ha0 : (m : ℕ) → P m 0) (H0b : (n : ℕ) → P 0 n) (H : (x y : ℕ) → P x y.succ → P x.succ y → P x.succ y.succ) (n m : ℕ) : P n m
• Nat.leRec_succ' 📋 Mathlib.Data.Nat.Init
  {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) : Nat.leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
• Nat.succ_injective 📋 Mathlib.Data.Nat.Basic
  : Function.Injective Nat.succ
• Int.lt.elim 📋 Mathlib.Data.Int.Order.Basic
  {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ (n : ℕ), a + ↑n.succ = b → P) : P
• Nat.mem_range_succ 📋 Mathlib.Data.Set.Image
  (i : ℕ) : i ∈ Set.range Nat.succ ↔ 0 < i
• Int.pred_nat_succ 📋 Mathlib.Data.Int.Init
  (n : ℕ) : (↑n.succ).pred = ↑n
• Int.neg_nat_succ 📋 Mathlib.Data.Int.Init
  (n : ℕ) : -↑n.succ = (-↑n).pred
• Int.succ_neg_natCast_succ 📋 Mathlib.Data.Int.Init
  (n : ℕ) : (-↑n.succ).succ = -↑n
• Int.ofNat_add_negSucc_of_ge 📋 Mathlib.Data.Int.Init
  {m n : ℕ} (h : n.succ ≤ m) : Int.ofNat m + Int.negSucc n = Int.ofNat (m - n.succ)
• Plausible.Random.instFinSucc 📋 Plausible.Random
  {m : Type → Type u_1} [Monad m] {n : ℕ} : Plausible.Random m (Fin n.succ)
• Plausible.Random.randFin 📋 Plausible.Random
  {m : Type → Type u_1} [Monad m] {g : Type} {n : ℕ} [RandomGen g] : Plausible.RandGT g m (Fin n.succ)
• Plausible.Fin.Arbitrary 📋 Plausible.Arbitrary
  {n : ℕ} : Plausible.Arbitrary (Fin n.succ)
• Plausible.Fin.shrinkable 📋 Plausible.Shrinkable
  {n : ℕ} : Plausible.Shrinkable (Fin n.succ)
• CommGroupWithZero.zpow_neg' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u_2} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (Int.negSucc n) a = (CommGroupWithZero.zpow (↑n.succ) a)⁻¹
• GroupWithZero.zpow_neg' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀) : GroupWithZero.zpow (Int.negSucc n) a = (GroupWithZero.zpow (↑n.succ) a)⁻¹
• GroupWithZero.zpow_succ' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀) : GroupWithZero.zpow (↑n.succ) a = GroupWithZero.zpow (↑n) a * a
• CommGroupWithZero.zpow_succ' 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u_2} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (↑n.succ) a = CommGroupWithZero.zpow (↑n) a * a
• GroupWithZero.mk 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u} [toMonoidWithZero : MonoidWithZero G₀] [toInv : Inv G₀] [toDiv : Div G₀] (div_eq_mul_inv : ∀ (a b : G₀), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G₀ → G₀) (zpow_zero' : ∀ (a : G₀), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G₀), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial G₀] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) : GroupWithZero G₀
• CommGroupWithZero.mk 📋 Mathlib.Algebra.GroupWithZero.Defs
  {G₀ : Type u_2} [toCommMonoidWithZero : CommMonoidWithZero G₀] [toInv : Inv G₀] [toDiv : Div G₀] (div_eq_mul_inv : ∀ (a b : G₀), a / b = a * b⁻¹ := by intros; rfl) (zpow : ℤ → G₀ → G₀) (zpow_zero' : ∀ (a : G₀), zpow 0 a = 1 := by intros; rfl) (zpow_succ' : ∀ (n : ℕ) (a : G₀), zpow (↑n.succ) a = zpow (↑n) a * a := by intros; rfl) (zpow_neg' : ∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹ := by intros; rfl) [toNontrivial : Nontrivial G₀] (inv_zero : 0⁻¹ = 0) (mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) : CommGroupWithZero G₀
• IsNilpotent.pow_succ 📋 Mathlib.Algebra.GroupWithZero.Basic
  (n : ℕ) {S : Type u_5} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ)
• Nat.cast_succ 📋 Mathlib.Data.Nat.Cast.Defs
  {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : ↑n.succ = ↑n + 1
• AddGroupWithOne.zsmul_neg' 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [self : AddGroupWithOne R] (n : ℕ) (a : R) : AddGroupWithOne.zsmul (Int.negSucc n) a = -AddGroupWithOne.zsmul (↑n.succ) a
• AddGroupWithOne.zsmul_succ' 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [self : AddGroupWithOne R] (n : ℕ) (a : R) : AddGroupWithOne.zsmul (↑n.succ) a = AddGroupWithOne.zsmul (↑n) a + a
• AddGroupWithOne.mk 📋 Mathlib.Data.Int.Cast.Defs
  {R : Type u} [toIntCast : IntCast R] [toAddMonoidWithOne : AddMonoidWithOne R] [toNeg : Neg R] [toSub : Sub R] (sub_eq_add_neg : ∀ (a b : R), a - b = a + -b := by intros; rfl) (zsmul : ℤ → R → R) (zsmul_zero' : ∀ (a : R), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) (neg_add_cancel : ∀ (a : R), -a + a = 0) (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : AddGroupWithOne R
• Ring.zsmul_neg' 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [self : Ring R] (n : ℕ) (a : R) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• Ring.zsmul_succ' 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [self : Ring R] (n : ℕ) (a : R) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• Ring.mk 📋 Mathlib.Algebra.Ring.Defs
  {R : Type u} [toSemiring : Semiring R] [toNeg : Neg R] [toSub : Sub R] (sub_eq_add_neg : ∀ (a b : R), a - b = a + -b := by intros; rfl) (zsmul : ℤ → R → R) (zsmul_zero' : ∀ (a : R), zsmul 0 a = 0 := by intros; rfl) (zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ) a = zsmul (↑n) a + a := by intros; rfl) (zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a := by intros; rfl) (neg_add_cancel : ∀ (a : R), -a + a = 0) [toIntCast : IntCast R] (intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n := by intros; rfl) (intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by intros; rfl) : Ring R
• Nat.sqrt_succ_le_succ_sqrt 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n.succ.sqrt ≤ n.sqrt.succ
• Nat.lt_succ_sqrt 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n < n.sqrt.succ * n.sqrt.succ
• Nat.lt_succ_sqrt' 📋 Mathlib.Data.Nat.Sqrt
  (n : ℕ) : n < n.sqrt.succ ^ 2
• DivisionRing.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : DivisionRing K] (n : ℕ) (a : K) : DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
• DivisionSemiring.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : DivisionSemiring K] (n : ℕ) (a : K) : DivisionSemiring.zpow (Int.negSucc n) a = (DivisionSemiring.zpow (↑n.succ) a)⁻¹
• Field.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u} [self : Field K] (n : ℕ) (a : K) : Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• Semifield.zpow_neg' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : Semifield K] (n : ℕ) (a : K) : Semifield.zpow (Int.negSucc n) a = (Semifield.zpow (↑n.succ) a)⁻¹
• DivisionSemiring.zpow_succ' 📋 Mathlib.Algebra.Field.Defs
  {K : Type u_2} [self : DivisionSemiring K] (n : ℕ) (a : K) : DivisionSemiring.zpow (↑n.succ) a = DivisionSemiring.zpow (↑n) a * a

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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 3a988db serving mathlib revision 028964f