Loogle!

Result

Found 18612 declarations mentioning HAdd.hAdd and OfNat.ofNat. Of these, 1749 have a name containing "succ". Of these, 1711 match your pattern(s). Of these, only the first 200 are shown.

• Nat.succ_eq_add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ = n + 1
• Nat.instNeZeroSucc 📋 Init.Data.Nat.Basic
  {n : ℕ} : NeZero (n + 1)
• 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.sub_succ_lt_self 📋 Init.Data.Nat.Basic
  (a i : ℕ) (h : i < a) : a - (i + 1) < a - i
• 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.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
• 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]
• 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.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.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.lt_succ 📋 Init.Data.Int.Order
  (a : ℤ) : a < a + 1
• 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
• 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.forall_lt_succ_right 📋 Init.Data.Nat.Lemmas
  {n : ℕ} {p : ℕ → Prop} : (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p 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.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
  (b : ℤ) (e : ℕ) : b ^ (e + 1) = b * b ^ e
• 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.eq_1 📋 Init.Data.Fin.Lemmas
  {n : ℕ} : Fin.castSucc = Fin.castAdd 1
• 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.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
• Fin.exists_castSucc_eq 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin (n + 1)} : (∃ j, j.castSucc = i) ↔ i ≠ Fin.last n
• Fin.castSucc_natAdd 📋 Init.Data.Fin.Lemmas
  {k : ℕ} (n : ℕ) (i : Fin k) : (Fin.natAdd n i).castSucc = Fin.natAdd n i.castSucc
• Fin.natAdd_castSucc 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} {i : Fin m} : Fin.natAdd n i.castSucc = (Fin.natAdd n i).castSucc
• Fin.succ_mk 📋 Init.Data.Fin.Lemmas
  (n i : ℕ) (h : i < n) : ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩
• Fin.castSucc_fin_succ 📋 Init.Data.Fin.Lemmas
  (n : ℕ) (j : Fin n) : j.succ.castSucc = j.castSucc.succ
• Fin.castSucc_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) : i.succ.castSucc = i.castSucc.succ
• Fin.succ_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) : i.castSucc.succ = i.succ.castSucc
• Fin.succ_cast_eq 📋 Init.Data.Fin.Lemmas
  {n n' : ℕ} (i : Fin n) (h : n = n') : (Fin.cast h i).succ = Fin.cast ⋯ i.succ
• Fin.subNat_one_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (Fin.subNat 1 i h).succ = i
• Fin.succ_ne_zero 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (k : Fin n) : k.succ ≠ 0
• Fin.castSucc_castLT 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) (h : ↑i < n) : (i.castLT h).castSucc = i
• Fin.reverseInduction_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive (Fin.last n)} {succ : (i : Fin n) → motive i.succ → motive i.castSucc} (i : Fin n) : Fin.reverseInduction zero succ i.castSucc = succ i (Fin.reverseInduction zero succ i.succ)
• 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.pred_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i
• Fin.castSucc_zero 📋 Init.Data.Fin.Lemmas
  {n : ℕ} [NeZero n] : Fin.castSucc 0 = 0
• Fin.succ_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a : Fin n) : 0 < a.succ
• 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.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 : Fin n) : Fin.cases zero succ i.succ = succ i
• Fin.castSucc_lt_iff_succ_le 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin n} {j : Fin (n + 1)} : i.castSucc < j ↔ i.succ ≤ j
• Fin.le_castSucc_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ
• Fin.castSucc_eq_zero_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0
• Fin.castSucc_ne_zero_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0
• Fin.forall_fin_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ
• Fin.cast_castSucc 📋 Init.Data.Fin.Lemmas
  {n n' : ℕ} {h : n + 1 = n' + 1} {i : Fin n} : Fin.cast h i.castSucc = (Fin.cast ⋯ i).castSucc
• Fin.one_lt_succ_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a : Fin n) : 1 < a.succ.succ
• Fin.succ_pred 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) (h : i ≠ 0) : (i.pred h).succ = i
• Fin.eq_succ_of_ne_zero 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j, i = j.succ
• Fin.castSucc_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc
• Fin.eq_zero_or_eq_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) : i = 0 ∨ ∃ j, i = j.succ
• 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.exists_fin_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i, P i.succ
• Fin.mk_succ_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : ℕ) (h : i < n) : 0 < ⟨i.succ, ⋯⟩
• Fin.pred_eq_iff_eq_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} : i.pred hi = j ↔ i = j.succ
• Fin.induction_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ) (i : Fin n) : Fin.induction zero succ i.succ = succ i (Fin.induction zero succ i.castSucc)
• Fin.succ_succ_ne_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (a : Fin n) : a.succ.succ ≠ 1
• 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.coeSucc_eq_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {a : Fin n} : a.castSucc + 1 = a.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.castSucc_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} : Fin.castSucc 1 = 1
• Fin.succ_one_eq_two 📋 Init.Data.Fin.Lemmas
  {n : ℕ} : Fin.succ 1 = 2
• Fin.succ_zero_eq_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} : Fin.succ 0 = 1
• 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.pred_castSucc_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin n) : i.succ.castSucc.pred ⋯ = i.castSucc
• Fin.pred_mk_succ' 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : ℕ) (h₁ : i + 1 < n + 1 + 1) (h₂ : ⟨i + 1, h₁⟩ ≠ 0) : ⟨i + 1, h₁⟩.pred h₂ = ⟨i, ⋯⟩
• Fin.pred_mk_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : ℕ) (h : i < n + 1) : ⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩
• Fin.foldr_succ_last 📋 Init.Data.Fin.Fold
  {n : ℕ} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : Fin.foldr (n + 1) f x = Fin.foldr n (fun x => f x.castSucc) (f (Fin.last n) x)
• Fin.foldl_succ_last 📋 Init.Data.Fin.Fold
  {α : Sort u_1} {n : ℕ} (f : α → Fin (n + 1) → α) (x : α) : Fin.foldl (n + 1) f x = f (Fin.foldl n (fun x1 x2 => f x1 x2.castSucc) x) (Fin.last n)
• Fin.foldrM_succ_last 📋 Init.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) : Fin.foldrM (n + 1) f = fun x => f (Fin.last n) x >>= Fin.foldrM n fun i => f i.castSucc
• Fin.foldlM_succ_last 📋 Init.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] (f : α → Fin (n + 1) → m α) : Fin.foldlM (n + 1) f = fun x => do let x ← Fin.foldlM n (fun x j => f x j.castSucc) x f x (Fin.last n)
• Fin.foldr_succ 📋 Init.Data.Fin.Fold
  {n : ℕ} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : Fin.foldr (n + 1) f x = f 0 (Fin.foldr n (fun i => f i.succ) x)
• Fin.foldl_succ 📋 Init.Data.Fin.Fold
  {α : Sort u_1} {n : ℕ} (f : α → Fin (n + 1) → α) (x : α) : Fin.foldl (n + 1) f x = Fin.foldl n (fun x i => f x i.succ) (f x 0)
• Fin.foldlM_succ 📋 Init.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] (f : α → Fin (n + 1) → m α) : Fin.foldlM (n + 1) f = fun x => f x 0 >>= Fin.foldlM n fun x j => f x j.succ
• Fin.foldrM_succ 📋 Init.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) : Fin.foldrM (n + 1) f = fun x => Fin.foldrM n (fun i => f i.succ) x >>= f 0
• List.replicate_succ_ne_nil 📋 Init.Data.List.Lemmas
  {α : Type u_1} {n : ℕ} {a : α} : List.replicate (n + 1) a ≠ []
• List.getD_cons_succ 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {x : α✝} {xs : List α✝} {n : ℕ} {d : α✝} : (x :: xs).getD (n + 1) d = xs.getD n d
• List.set_cons_succ 📋 Init.Data.List.Lemmas
  {α : Type u_1} {x : α} {xs : List α} {i : ℕ} {a : α} : (x :: xs).set (i + 1) a = x :: xs.set i a
• List.replicate_succ' 📋 Init.Data.List.Lemmas
  {n : ℕ} {α✝ : Type u_1} {a : α✝} : List.replicate (n + 1) a = List.replicate n a ++ [a]
• List.getElem?_cons_succ 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} {l : List α} : (a :: l)[i + 1]? = l[i]?
• List.getElem!_cons_succ 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {i : ℕ} [Inhabited α] {l : List α} : (a :: l)[i + 1]! = l[i]!
• List.get_cons_succ 📋 Init.Data.List.Lemmas
  {α : Type u_1} {i : ℕ} {a : α} {as : List α} {h : i + 1 < (a :: as).length} : (a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩
• List.getElem?_insert_succ 📋 Init.Data.List.Lemmas
  {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : ℕ} : (List.insert a l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?
• List.ofFn_succ_last 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} : List.ofFn f = (List.ofFn fun i => f i.castSucc) ++ [f (Fin.last n)]
• List.ofFn_succ 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} : List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
• List.ofFnM_succ_last 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let as ← List.ofFnM fun i => f i.castSucc let a ← f (Fin.last n) pure (as ++ [a])
• List.getElem?_take_of_succ 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {l : List α} {i : ℕ} : (List.take (i + 1) l)[i]? = l[i]?
• List.take_succ 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {l : List α} {i : ℕ} : List.take (i + 1) l = List.take i l ++ l[i]?.toList
• List.take_succ_eq_append_getElem 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {i : ℕ} {l : List α} (h : i < l.length) : List.take (i + 1) l = List.take i l ++ [l[i]]
• List.finRange_succ 📋 Init.Data.List.FinRange
  {n : ℕ} : List.finRange (n + 1) = 0 :: List.map Fin.succ (List.finRange n)
• List.ofFnM_succ 📋 Init.Data.List.FinRange
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let a ← f 0 let as ← List.ofFnM fun i => f i.succ pure (a :: as)
• List.finRange_succ_last 📋 Init.Data.List.FinRange
  {n : ℕ} : List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
• Nat.all_succ 📋 Init.Data.Nat.Fold
  {n : ℕ} (f : (i : ℕ) → i < n + 1 → Bool) : (n + 1).all f = ((n.all fun i h => f i ⋯) && f n ⋯)
• Nat.any_succ 📋 Init.Data.Nat.Fold
  {n : ℕ} (f : (i : ℕ) → i < n + 1 → Bool) : (n + 1).any f = ((n.any fun i h => f i ⋯) || f n ⋯)
• Nat.foldRev_succ 📋 Init.Data.Nat.Fold
  {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n + 1 → α → α) (init : α) : (n + 1).foldRev f init = n.foldRev (fun i h => f i ⋯) (f n ⋯ init)
• Nat.fold_succ 📋 Init.Data.Nat.Fold
  {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n + 1 → α → α) (init : α) : (n + 1).fold f init = f n ⋯ (n.fold (fun i h => f i ⋯) init)
• Nat.dfoldRev_succ 📋 Init.Data.Nat.Fold
  {n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev_succ._auto_3 → Type u} (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) (init : α (n + 1) ⋯) : (n + 1).dfoldRev f init = n.dfoldRev (fun i h => f i ⋯) (f n ⋯ init)
• Nat.dfold_succ 📋 Init.Data.Nat.Fold
  {n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfold_succ._auto_3 → Type u} (f : (i : ℕ) → (h : i < n + 1) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯) : (n + 1).dfold f init = f n ⋯ (n.dfold (fun i h => f i ⋯) init)
• Int.dvd_negSucc 📋 Init.Data.Int.DivMod.Lemmas
  {a : ℤ} {b : ℕ} : a ∣ Int.negSucc b ↔ a ∣ ↑(b + 1)
• Int.negSucc_dvd 📋 Init.Data.Int.DivMod.Lemmas
  {a : ℕ} {b : ℤ} : Int.negSucc a ∣ b ↔ ↑(a + 1) ∣ b
• Int.negSucc_ediv 📋 Init.Data.Int.DivMod.Lemmas
  (m : ℕ) {b : ℤ} (H : 0 < b) : Int.negSucc m / b = -((↑m).ediv b + 1)
• Int.not_dvd_iff_lt_mul_succ 📋 Init.Data.Int.DivMod.Lemmas
  {n : ℤ} (m : ℤ) (hn : 0 < n) : ¬n ∣ m ↔ ∃ k, n * k < m ∧ m < n * (k + 1)
• Int.negSucc_emod_negSucc_eq_zero_iff 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℕ} : Int.negSucc a % Int.negSucc b = 0 ↔ (a + 1) % (b + 1) = 0
• Int.negSucc_emod_ofNat_succ_eq_zero_iff 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℕ} : Int.negSucc a % (↑b + 1) = 0 ↔ (a + 1) % (b + 1) = 0
• Int.shiftLeft_succ 📋 Init.Data.Int.Bitwise.Lemmas
  (m : ℤ) (n : ℕ) : m <<< (n + 1) = m <<< n * 2
• Int.shiftLeft_succ' 📋 Init.Data.Int.Bitwise.Lemmas
  (m : ℤ) (n : ℕ) : m <<< (n + 1) = 2 * m <<< n
• BitVec.instDecidableForallBitVecSucc 📋 Init.Data.BitVec.Decidable
  {n : ℕ} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v))] : Decidable (∀ (v : BitVec (n + 1)), P v)
• BitVec.instDecidableExistsBitVecSucc 📋 Init.Data.BitVec.Decidable
  {n : ℕ} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), ¬P (BitVec.cons x v))] : Decidable (∃ v, P v)
• BitVec.getLsbD_concat_succ 📋 Init.Data.BitVec.Lemmas
  {w✝ : ℕ} {x : BitVec w✝} {b : Bool} {i : ℕ} : (x.concat b).getLsbD (i + 1) = x.getLsbD i
• BitVec.getMsbD_cons_succ 📋 Init.Data.BitVec.Lemmas
  {a : Bool} {w✝ : ℕ} {x : BitVec w✝} {i : ℕ} : (BitVec.cons a x).getMsbD (i + 1) = x.getMsbD i
• BitVec.setWidth_succ 📋 Init.Data.BitVec.Lemmas
  {w i : ℕ} (x : BitVec w) : BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)
• BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x : BitVec w} {i : ℕ} (hx : x.getLsbD i = false) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x)
• BitVec.pow_succ 📋 Init.Data.BitVec.Lemmas
  {w n : ℕ} {x : BitVec w} : x ^ (n + 1) = x ^ n * x
• BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {x : BitVec w} {i : ℕ} (hx : x.getLsbD i = true) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) ||| BitVec.twoPow w i
• BitVec.getElem_shiftConcat_succ 📋 Init.Data.BitVec.Lemmas
  {w i : ℕ} {x : BitVec w} {b : Bool} (h : i + 1 < w) : (x.shiftConcat b)[i + 1] = x[i]
• BitVec.getElem?_succ_ofBool 📋 Init.Data.BitVec.Lemmas
  (b : Bool) (i : ℕ) : (BitVec.ofBool b)[i + 1]? = none
• BitVec.getLsbD_succ_last 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} (x : BitVec (w + 1)) : x.getLsbD w = decide (2 ^ w ≤ x.toNat)
• BitVec.clzAuxRec_succ 📋 Init.Data.BitVec.Lemmas
  {w n : ℕ} (x : BitVec w) : x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) = true then BitVec.ofNat w (w - 1 - (n + 1)) else x.clzAuxRec n
• BitVec.replicate_succ 📋 Init.Data.BitVec.Lemmas
  {w n : ℕ} {x : BitVec w} : BitVec.replicate (n + 1) x = BitVec.cast ⋯ (x ++ BitVec.replicate n x)
• BitVec.replicate_succ' 📋 Init.Data.BitVec.Lemmas
  {w n : ℕ} {x : BitVec w} : BitVec.replicate (n + 1) x = BitVec.cast ⋯ (BitVec.replicate n x ++ x)
• BitVec.getElem_concat_succ 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {b : Bool} {x : BitVec w} {i : ℕ} (h : i + 1 < w + 1) : (x.concat b)[i + 1] = x[i]
• BitVec.divRec_succ 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (m : ℕ) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.divRec (m + 1) args qr = BitVec.divRec m args (BitVec.divSubtractShift args qr)
• BitVec.carry_succ 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (i : ℕ) (x y : BitVec w) (c : Bool) : BitVec.carry (i + 1) x y c = (x.getLsbD i).atLeastTwo (y.getLsbD i) (BitVec.carry i x y c)
• BitVec.sshiftRightRec_succ_eq 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ) : x.sshiftRightRec y (n + 1) = (x.sshiftRightRec y n).sshiftRight' (y &&& BitVec.twoPow w₂ (n + 1))
• BitVec.shiftLeftRec_succ 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ n : ℕ} {x : BitVec w₁} {y : BitVec w₂} : x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& BitVec.twoPow w₂ (n + 1))
• BitVec.ushiftRightRec_succ 📋 Init.Data.BitVec.Bitblast
  {w₁ w₂ n : ℕ} (x : BitVec w₁) (y : BitVec w₂) : x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& BitVec.twoPow w₂ (n + 1))
• BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x : BitVec w) (i : ℕ) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) + (x &&& BitVec.twoPow w i)
• BitVec.carry_succ_one 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (i : ℕ) (x : BitVec w) (h : 0 < w) : BitVec.carry (i + 1) x (1#w) false = decide (∀ j ≤ i, x.getLsbD j = true)
• BitVec.mulRec_succ_eq 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (x y : BitVec w) (s : ℕ) : x.mulRec y (s + 1) = x.mulRec y s + if y.getLsbD (s + 1) = true then x <<< (s + 1) else 0
• BitVec.divRec_succ' 📋 Init.Data.BitVec.Bitblast
  {w : ℕ} (m : ℕ) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) : BitVec.divRec (m + 1) args qr = have wn := qr.wn - 1; have wr := qr.wr + 1; have r' := qr.r.shiftConcat (args.n.getLsbD wn); have input := if r' < args.d then { wn := wn, wr := wr, q := qr.q.shiftConcat false, r := r' } else { wn := wn, wr := wr, q := qr.q.shiftConcat true, r := r' - args.d }; BitVec.divRec m args input
• UInt16.mul_succ 📋 Init.Data.UInt.Lemmas
  {a b : UInt16} : a * (b + 1) = a * b + a
• UInt16.succ_mul 📋 Init.Data.UInt.Lemmas
  {a b : UInt16} : (a + 1) * b = a * b + b
• UInt32.mul_succ 📋 Init.Data.UInt.Lemmas
  {a b : UInt32} : a * (b + 1) = a * b + a
• UInt32.succ_mul 📋 Init.Data.UInt.Lemmas
  {a b : UInt32} : (a + 1) * b = a * b + b
• UInt64.mul_succ 📋 Init.Data.UInt.Lemmas
  {a b : UInt64} : a * (b + 1) = a * b + a
• UInt64.succ_mul 📋 Init.Data.UInt.Lemmas
  {a b : UInt64} : (a + 1) * b = a * b + b

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