Loogle!

Result

Found 1551 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.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.le.below.step 📋 Init.Prelude
  {n : ℕ} {motive : (a : ℕ) → n.le a → Prop} {m : ℕ} (a✝ : n.le m) : Nat.le.below a✝ → motive m a✝ → Nat.le.below ⋯
• 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.beq.eq_2 📋 Init.Data.Nat.Basic
  (n : ℕ) : Nat.zero.beq n.succ = false
• Nat.beq.eq_3 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ.beq Nat.zero = false
• 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.beq.eq_4 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n.succ.beq m.succ = n.beq m
• 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
• Nat.mod.eq_2 📋 Init.Data.Nat.Div.Basic
  (x✝ n : ℕ) : n.succ.mod x✝ = if x✝ ≤ n.succ then n.succ.modCore x✝ else n.succ
• Nat.modCore.go.eq_1 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (x fuel_2 : ℕ) (hfuel_2 : x < fuel_2.succ) : Nat.modCore.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.modCore.go y hy fuel_2 (x - y) ⋯ else x
• Nat.div.go.eq_1 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (x fuel_2 : ℕ) (hfuel_2 : x < fuel_2.succ) : Nat.div.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.div.go y hy fuel_2 (x - y) ⋯ + 1 else 0
• Nat.modCore.go.eq_def 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : Nat.modCore.go y hy fuel x hfuel = match fuel, hfuel with | fuel.succ, hfuel => if h : y ≤ x then Nat.modCore.go y hy fuel (x - y) ⋯ else x
• Nat.div.go.eq_def 📋 Init.Data.Nat.Div.Basic
  (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel) : Nat.div.go y hy fuel x hfuel = match fuel, hfuel with | fuel.succ, hfuel => if h : y ≤ x then Nat.div.go y hy fuel (x - y) ⋯ + 1 else 0
• List.replicate.eq_2 📋 Init.Data.List.Basic
  {α : Type u} (x✝ : α) (n : ℕ) : List.replicate n.succ x✝ = x✝ :: List.replicate n x✝
• List.lengthTRAux.eq_2 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : ℕ) (head : α) (as : List α) : (head :: as).lengthTRAux x✝ = as.lengthTRAux x✝.succ
• List.replicateTR.loop.eq_2 📋 Init.Data.List.Basic
  {α : Type u} (a : α) (x✝ : List α) (n : ℕ) : List.replicateTR.loop a n.succ x✝ = List.replicateTR.loop a n (a :: x✝)
• List.set.eq_2 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ a : α) (as : List α) (n : ℕ) : (a :: as).set n.succ x✝ = a :: as.set n x✝
• List.lengthTRAux.eq_def 📋 Init.Data.List.Basic
  {α : Type u_1} (x✝ : List α) (x✝¹ : ℕ) : x✝.lengthTRAux x✝¹ = match x✝, x✝¹ with | [], n => n | head :: as, n => as.lengthTRAux n.succ
• List.range'TR.go.eq_2 📋 Init.Data.List.Basic
  (step x✝ : ℕ) (x✝¹ : List ℕ) (n : ℕ) : List.range'TR.go step n.succ x✝ x✝¹ = List.range'TR.go step n (x✝ - step) ((x✝ - step) :: x✝¹)
• List.drop.eq_2 📋 Init.Data.Array.GetLit
  {α : Type u} (n : ℕ) : List.drop n.succ [] = []
• List.drop.eq_3 📋 Init.Data.Array.GetLit
  {α : Type u} (n : ℕ) (a : α) (as : List α) : List.drop n.succ (a :: as) = List.drop n as
• Array.toListLitAux.eq_2 📋 Init.Data.Array.GetLit
  {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (x : List α) (i : ℕ) (hi : i + 1 ≤ xs.size) : xs.toListLitAux n hsz i.succ hi x = xs.toListLitAux n hsz i ⋯ (xs.getLit i hsz ⋯ :: x)
• Nat.Linear.Poly.cancelAux.eq_2 📋 Init.Data.Nat.Linear
  (m₁ r₁ r₂ : Nat.Linear.Poly) (fuel_2 : ℕ) : Nat.Linear.Poly.cancelAux fuel_2.succ m₁ [] r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂)
• Nat.Linear.Poly.cancelAux.eq_3 📋 Init.Data.Nat.Linear
  (m₂ r₁ r₂ : Nat.Linear.Poly) (fuel_2 : ℕ) (x : m₂ = [] → False) : Nat.Linear.Poly.cancelAux fuel_2.succ [] m₂ r₁ r₂ = (List.reverse r₁, List.reverse r₂ ++ m₂)
• Nat.Linear.Poly.cancelAux.eq_4 📋 Init.Data.Nat.Linear
  (r₁ r₂ : Nat.Linear.Poly) (fuel_2 k₁ : ℕ) (v₁ : Nat.Linear.Var) (m₁_2 : List (ℕ × Nat.Linear.Var)) (k₂ : ℕ) (v₂ : Nat.Linear.Var) (m₂_2 : List (ℕ × Nat.Linear.Var)) : Nat.Linear.Poly.cancelAux fuel_2.succ ((k₁, v₁) :: m₁_2) ((k₂, v₂) :: m₂_2) r₁ r₂ = bif Nat.blt v₁ v₂ then Nat.Linear.Poly.cancelAux fuel_2 m₁_2 ((k₂, v₂) :: m₂_2) ((k₁, v₁) :: r₁) r₂ else bif Nat.blt v₂ v₁ then Nat.Linear.Poly.cancelAux fuel_2 ((k₁, v₁) :: m₁_2) m₂_2 r₁ ((k₂, v₂) :: r₂) else bif k₁.blt k₂ then Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ ((k₂.sub k₁, v₁) :: r₂) else bif k₂.blt k₁ then Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 ((k₁.sub k₂, v₁) :: r₁) r₂ else Nat.Linear.Poly.cancelAux fuel_2 m₁_2 m₂_2 r₁ r₂
• Nat.log2.eq_1 📋 Init.Data.Nat.Log2
  (n : ℕ) : n.log2 = Nat.rec (motive := fun x => ℕ → ℕ) (fun x => 0) (fun x ih n => Bool.rec 0 (ih (n.div 2)).succ (Nat.ble 2 n)) n n
• Int.fdiv.eq_3 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.ofNat m.succ).fdiv (Int.negSucc n) = Int.negSucc (m / n.succ)
• Int.fdiv.eq_5 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.negSucc m).fdiv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
• Int.fdiv.eq_6 📋 Init.Data.Int.DivMod.Basic
  (m n : ℕ) : (Int.negSucc m).fdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
• 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.natAbs.eq_2 📋 Init.Data.Int.Order
  (n_1 : ℕ) : (Int.negSucc n_1).natAbs = n_1.succ
• Int.sign.eq_1 📋 Init.Data.Int.Order
  (n : ℕ) : (Int.ofNat n.succ).sign = 1
• Int.ofNat_succ_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < ↑n.succ
• Int.natAbs.eq_def 📋 Init.Data.Int.Order
  (m : ℤ) : m.natAbs = match m with | Int.ofNat m => m | Int.negSucc m => m.succ
• Int.mul.eq_2 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.ofNat m_2).mul (Int.negSucc n_2) = Int.negOfNat (m_2 * n_2.succ)
• Int.mul.eq_3 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.negSucc m_2).mul (Int.ofNat n_2) = Int.negOfNat (m_2.succ * n_2)
• Int.mul.eq_4 📋 Init.Data.Int.Order
  (m_2 n_2 : ℕ) : (Int.negSucc m_2).mul (Int.negSucc n_2) = Int.ofNat (m_2.succ * n_2.succ)
• Int.lt.dest 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a < b) : ∃ n, a + ↑n.succ = b
• Int.ediv.eq_4 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.negSucc m).ediv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
• Int.ediv.eq_5 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.negSucc m).ediv (Int.negSucc n) = Int.ofNat (m / n.succ).succ
• Int.ediv.eq_2 📋 Init.Data.Int.DivMod.Bootstrap
  (m n : ℕ) : (Int.ofNat m).ediv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• 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
• List.get.eq_2 📋 Init.Data.List.BasicAux
  {α : Type u} (head : α) (as : List α) (i : ℕ) (h : i.succ < (head :: as).length) : (head :: as).get ⟨i.succ, h⟩ = as.get ⟨i, ⋯⟩
• List.get.eq_def 📋 Init.Data.List.BasicAux
  {α : Type u} (x✝ : List α) (x✝¹ : Fin x✝.length) : x✝.get x✝¹ = match x✝, x✝¹ with | a :: tail, ⟨0, isLt⟩ => a | head :: as, ⟨i.succ, h⟩ => as.get ⟨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
• Fin.foldr.loop.eq_2 📋 Init.Data.Fin.Fold
  {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (x : α) (i : ℕ) (h : i + 1 ≤ n) : Fin.foldr.loop n f i.succ h x = Fin.foldr.loop n f i ⋯ (f ⟨i, h⟩ x)
• List.splitAt.go.eq_2 📋 Init.Data.List.Lemmas
  {α : Type u} (l x✝ : List α) (x_3 : α) (xs : List α) (n : ℕ) : List.splitAt.go l (x_3 :: xs) n.succ x✝ = List.splitAt.go l xs n (x_3 :: x✝)
• List.splitAt.go.eq_3 📋 Init.Data.List.Lemmas
  {α : Type u} (l x✝ : List α) (x✝¹ : ℕ) (x✝² : List α) (x_4 : x✝ = [] → False) (x_5 : ∀ (x : α) (xs : List α) (n : ℕ), x✝ = x :: xs → x✝¹ = n.succ → False) : List.splitAt.go l x✝ x✝¹ x✝² = (x✝².reverse, x✝)
• 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.take.eq_2 📋 Init.Data.List.TakeDrop
  {α : Type u} (n : ℕ) : List.take n.succ [] = []
• List.take.eq_3 📋 Init.Data.List.TakeDrop
  {α : Type u} (n : ℕ) (a : α) (as : List α) : List.take n.succ (a :: as) = a :: List.take n as
• 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.tmod.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m).tmod (Int.negSucc n) = Int.ofNat (m % n.succ)
• Int.fmod.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).fmod (Int.ofNat n) = Int.subNatNat n (m % n).succ
• Int.tdiv.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
• Int.emod.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (x✝ : ℤ) (m : ℕ) : (Int.negSucc m).emod x✝ = Int.subNatNat x✝.natAbs (m % x✝.natAbs).succ
• Int.fmod.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m.succ).fmod (Int.negSucc n) = Int.subNatNat (m % n.succ) n
• Int.tdiv.eq_2 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.ofNat m).tdiv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• Int.tdiv.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tdiv (Int.ofNat n) = -Int.ofNat (m.succ / n)
• Int.tmod.eq_3 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tmod (Int.ofNat n) = -Int.ofNat (m.succ % n)
• Int.fmod.eq_5 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).fmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
• Int.tmod.eq_4 📋 Init.Data.Int.DivMod.Lemmas
  (m n : ℕ) : (Int.negSucc m).tmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)
• 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
• BitVec.reverse.eq_2 📋 Init.Data.BitVec.Lemmas
  (w : ℕ) (x_2 : BitVec (w + 1)) : x_2.reverse = (BitVec.truncate w x_2).reverse.concat x_2.msb
• BitVec.replicate.eq_2 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} (x✝ : BitVec w) (n : ℕ) : BitVec.replicate n.succ x✝ = BitVec.cast ⋯ (x✝ ++ BitVec.replicate n x✝)
• BitVec.sshiftRightRec.eq_2 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ) : x.sshiftRightRec y s_1.succ = (x.sshiftRightRec y s_1).sshiftRight' (y &&& BitVec.twoPow w₂ s_1.succ)
• BitVec.shiftLeftRec.eq_2 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ) : x.shiftLeftRec y s_1.succ = x.shiftLeftRec y s_1 <<< (y &&& BitVec.twoPow w₂ s_1.succ)
• BitVec.ushiftRightRec.eq_2 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ) : x.ushiftRightRec y s_1.succ = x.ushiftRightRec y s_1 >>> (y &&& BitVec.twoPow w₂ s_1.succ)
• BitVec.mulRec.eq_2 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x y : BitVec w) (s_2 : ℕ) : x.mulRec y s_2.succ = x.mulRec y s_2 + if y.getLsbD s_2.succ = true then x <<< s_2.succ else 0
• BitVec.uppcRec.eq_2 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x : BitVec w) (i : ℕ) (hs_2 : i + 1 < w) : x.uppcRec i.succ hs_2 = (x[w - 1 - i] || x.uppcRec i ⋯)
• BitVec.resRec.eq_def 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x y : BitVec w) (s : ℕ) (hs : s < w) (hslt : 0 < s) : x.resRec y s hs hslt = match hs0 : s, hs, hslt with | 0, hs, hslt => ⋯.elim | s'.succ, hs, hslt => match hs' : s', hs, hslt, hs0 with | 0, hs, hslt, hs0 => x.aandRec y 1 hs | s''.succ, hs, hslt, hs0 => x.resRec y s' ⋯ ⋯ || x.aandRec y s ⋯
• List.range_succ 📋 Init.Data.List.Range
  {n : ℕ} : List.range n.succ = List.range n ++ [n]
• List.range'.eq_2 📋 Init.Data.List.Range
  (x✝ x✝¹ n : ℕ) : List.range' x✝ n.succ x✝¹ = x✝ :: List.range' (x✝ + x✝¹) n x✝¹
• List.range_succ_eq_map 📋 Init.Data.List.Range
  {n : ℕ} : List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
• List.eraseIdx.eq_3 📋 Init.Data.List.Impl
  {α : Type u} (a : α) (as : List α) (n : ℕ) : (a :: as).eraseIdx n.succ = a :: as.eraseIdx 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
• Array.forIn'.loop.eq_2 📋 Init.Data.List.ToArray
  {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (b : β) (i_2 : ℕ) (h_2 : i_2 + 1 ≤ as.size) : Array.forIn'.loop as f i_2.succ h_2 b = do let __do_lift ← f as[as.size - 1 - i_2] ⋯ b match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => Array.forIn'.loop as f i_2 ⋯ b
• Nat.repeat.eq_2 📋 Init.Data.String.Basic
  {α : Type u} (f : α → α) (x✝ : α) (n : ℕ) : Nat.repeat f n.succ x✝ = f (Nat.repeat f n x✝)
• String.Slice.Pos.nextn.induct_unfolding 📋 Init.Data.String.Basic
  {s : String.Slice} (motive : s.Pos → ℕ → s.Pos → Prop) (case1 : ∀ (p : s.Pos), motive p 0 p) (case2 : ∀ (p : s.Pos) (n : ℕ) (h : p ≠ s.endPos), motive (p.next h) n ((p.next h).nextn n) → motive p n.succ ((p.next h).nextn n)) (case3 : ∀ (p : s.Pos) (n : ℕ), ¬p ≠ s.endPos → motive p n.succ p) (p : s.Pos) (n : ℕ) : motive p n (p.nextn n)

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 6ff4759 serving mathlib revision 519f454