Loogle!

Result

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

• Nat.lt_add_one 📋 Init.Prelude
  (n : ℕ) : n < n + 1
• Nat.add_one_ne 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 ≠ n
• Nat.add_one_ne_self 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 ≠ n
• Nat.ne_add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n ≠ n + 1
• Nat.add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 = n.succ
• Nat.succ_eq_add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n.succ = n + 1
• Nat.not_add_one_le_self 📋 Init.Data.Nat.Basic
  (n : ℕ) : ¬n + 1 ≤ n
• Nat.add_one_ne_zero 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 ≠ 0
• Nat.zero_ne_add_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : 0 ≠ n + 1
• Nat.add_one_pos 📋 Init.Data.Nat.Basic
  (n : ℕ) : 0 < n + 1
• Nat.not_add_one_le_zero 📋 Init.Data.Nat.Basic
  (n : ℕ) : ¬n + 1 ≤ 0
• Nat.add_one_le_of_lt 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n < m) : n + 1 ≤ m
• Nat.le_of_lt_add_one 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n < m + 1 → n ≤ m
• Nat.lt_add_one_of_le 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n ≤ m → n < m + 1
• Nat.lt_add_one_of_lt 📋 Init.Data.Nat.Basic
  {a b : ℕ} (h : a < b) : a < b + 1
• Nat.lt_of_add_one_le 📋 Init.Data.Nat.Basic
  {n m : ℕ} (h : n + 1 ≤ m) : n < m
• Nat.add_one_le_iff 📋 Init.Data.Nat.Basic
  {n m : ℕ} : n + 1 ≤ m ↔ n < m
• Nat.lt_add_one_iff 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m < n + 1 ↔ m ≤ n
• Nat.and_forall_add_one 📋 Init.Data.Nat.Basic
  {p : ℕ → Prop} : (p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n
• Nat.exists_eq_add_one_of_ne_zero 📋 Init.Data.Nat.Basic
  {n : ℕ} : n ≠ 0 → ∃ k, n = k + 1
• Nat.add_one_sub_one 📋 Init.Data.Nat.Basic
  (n : ℕ) : n + 1 - 1 = n
• Nat.lt_add_one_iff_lt_or_eq 📋 Init.Data.Nat.Basic
  {m n : ℕ} : m < n + 1 ↔ m < n ∨ m = n
• Nat.or_exists_add_one 📋 Init.Data.Nat.Basic
  {p : ℕ → Prop} : (p 0 ∨ ∃ n, p (n + 1)) ↔ Exists p
• Nat.add_one_add_one_ne_one 📋 Init.Data.Nat.Basic
  {a : ℕ} : a + 1 + 1 ≠ 1
• Nat.add_one_inj 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a + 1 = b + 1 ↔ a = b
• Nat.add_one_ne_add_one_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a + 1 ≠ b + 1 ↔ a ≠ b
• Nat.add_one_le_add_one_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a + 1 ≤ b + 1 ↔ a ≤ b
• Nat.add_one_lt_add_one_iff 📋 Init.Data.Nat.Basic
  {a b : ℕ} : a + 1 < b + 1 ↔ a < b
• Nat.sub_one_add_one 📋 Init.Data.Nat.Basic
  {a : ℕ} (h : a ≠ 0) : a - 1 + 1 = a
• Nat.eq_zero_or_eq_sub_one_add_one 📋 Init.Data.Nat.Basic
  {n : ℕ} : n = 0 ∨ n = n - 1 + 1
• Nat.sub_one_add_one_eq_of_pos 📋 Init.Data.Nat.Basic
  {n : ℕ} : 0 < n → n - 1 + 1 = n
• Nat.le_or_eq_of_le_add_one 📋 Init.Data.Nat.Basic
  {m n : ℕ} (h : m ≤ n + 1) : m ≤ n ∨ m = n + 1
• Nat.add_one_mul 📋 Init.Data.Nat.Basic
  (n m : ℕ) : (n + 1) * m = n * m + m
• Nat.mul_add_one 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n * (m + 1) = n * m + n
• Nat.pow_add_one 📋 Init.Data.Nat.Basic
  (n m : ℕ) : n ^ (m + 1) = n ^ m * n
• Fin.val_add_one_le_of_gt 📋 Init.Data.Fin.Basic
  {n : ℕ} {a b : Fin n} (h : a > b) : ↑b + 1 ≤ ↑a
• Fin.val_add_one_le_of_lt 📋 Init.Data.Fin.Basic
  {n : ℕ} {a b : Fin n} (h : a < b) : ↑a + 1 ≤ ↑b
• Int.negSucc_add_one_eq_neg_ofNat_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : Int.negSucc a + 1 = -↑b ↔ a = b
• Int.neg_ofNat_eq_negSucc_add_one_iff 📋 Init.Data.Int.Lemmas
  {a b : ℕ} : -↑a = Int.negSucc b + 1 ↔ a = b
• Int.natCast_add_one 📋 Init.Data.Int.Lemmas
  (n : ℕ) : ↑(n + 1) = ↑n + 1
• Int.add_one_le_of_lt 📋 Init.Data.Int.Order
  {a b : ℤ} (H : a < b) : a + 1 ≤ b
• Int.le_add_one 📋 Init.Data.Int.Order
  {a b : ℤ} (h : a ≤ b) : a ≤ b + 1
• Int.le_of_lt_add_one 📋 Init.Data.Int.Order
  {a b : ℤ} (H : a < b + 1) : a ≤ b
• Int.lt_add_one_of_le 📋 Init.Data.Int.Order
  {a b : ℤ} (H : a ≤ b) : a < b + 1
• Int.lt_of_add_one_le 📋 Init.Data.Int.Order
  {a b : ℤ} (H : a + 1 ≤ b) : a < b
• Int.add_one_le_iff 📋 Init.Data.Int.Order
  {a b : ℤ} : a + 1 ≤ b ↔ a < b
• Int.le_iff_lt_add_one 📋 Init.Data.Int.Order
  {a b : ℤ} : a ≤ b ↔ a < b + 1
• Int.lt_add_one_iff 📋 Init.Data.Int.Order
  {a b : ℤ} : a < b + 1 ↔ a ≤ b
• Int.lt_iff_add_one_le 📋 Init.Data.Int.Order
  {a b : ℤ} : a < b ↔ a + 1 ≤ b
• Int.sign_natCast_add_one 📋 Init.Data.Int.Order
  (n : ℕ) : (↑n + 1).sign = 1
• Int.sign_of_add_one 📋 Init.Data.Int.Order
  (x : ℕ) : (↑x + 1).sign = 1
• Int.toNat_natCast_add_one 📋 Init.Data.Int.Order
  {n : ℕ} : (↑n + 1).toNat = n + 1
• Int.le_add_one_iff 📋 Init.Data.Int.Order
  {m n : ℤ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
• Nat.gcd_add_one 📋 Init.Data.Nat.Gcd
  (x y : ℕ) : (x + 1).gcd y = (y % (x + 1)).gcd (x + 1)
• Nat.le_iff_lt_add_one 📋 Init.Data.Nat.Lemmas
  {x y : ℕ} : x ≤ y ↔ x < y + 1
• Nat.lt_iff_add_one_le 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m < n ↔ m + 1 ≤ n
• Nat.sub_lt_add_one 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : a - b < a + 1
• Nat.exists_add_one_eq 📋 Init.Data.Nat.Lemmas
  {a : ℕ} : (∃ n, n + 1 = a) ↔ 0 < a
• Nat.exists_eq_add_one 📋 Init.Data.Nat.Lemmas
  {a : ℕ} : (∃ n, a = n + 1) ↔ 0 < a
• Nat.le_add_one_iff 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
• Nat.le_and_le_add_one_iff 📋 Init.Data.Nat.Lemmas
  {n m : ℕ} : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
• Nat.pow_add_one' 📋 Init.Data.Nat.Lemmas
  {m n : ℕ} : m ^ (n + 1) = m * m ^ n
• Nat.add_one_mul_add_one 📋 Init.Data.Nat.Lemmas
  (a b : ℕ) : (a + 1) * (b + 1) = a * b + a + b + 1
• Nat.add_div_of_dvd_add_add_one 📋 Init.Data.Nat.Div.Lemmas
  {c a b : ℕ} (h : c ∣ a + b + 1) : (a + b) / c = a / c + b / c
• Nat.testBit_add_one 📋 Init.Data.Nat.Bitwise.Lemmas
  (x i : ℕ) : x.testBit (i + 1) = (x / 2).testBit i
• 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.last_add_one 📋 Init.Data.Fin.Lemmas
  (n : ℕ) : Fin.last n + 1 = 0
• Fin.add_one_le_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {k : Fin (n + 1)} : k + 1 ≤ k ↔ k = Fin.last n
• Fin.add_one_lt_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {k : Fin (n + 2)} : k + 1 < k ↔ k = Fin.last (n + 1)
• Fin.lt_add_one_iff 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {k : Fin (n + 1)} : k < k + 1 ↔ k < Fin.last n
• Fin.val_add_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) : ↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1
• Fin.add_one_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) : 0 < i + 1
• Fin.pred_add_one 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 2)) (h : ↑i < n + 1) : (i + 1).pred ⋯ = i.castLT h
• List.ne_nil_of_length_eq_add_one 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {l : List α✝} {n : ℕ} : l.length = n + 1 → l ≠ []
• List.exists_mem_of_length_eq_add_one 📋 Init.Data.List.Lemmas
  {α : Type u_1} {n : ℕ} {l : List α} : l.length = n + 1 → ∃ a, a ∈ l
• List.exists_cons_of_length_eq_add_one 📋 Init.Data.List.Lemmas
  {α : Type u_1} {n : ℕ} {l : List α} : l.length = n + 1 → ∃ h t, l = h :: t
• List.drop_add_one_eq_tail_drop 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {i : ℕ} {l : List α} : List.drop (i + 1) l = (List.drop i l).tail
• List.take_add_one 📋 Init.Data.List.TakeDrop
  {α : Type u_1} {l : List α} {i : ℕ} : List.take (i + 1) l = List.take i l ++ l[i]?.toList
• Int.emod_self_add_one 📋 Init.Data.Int.DivMod.Lemmas
  {x : ℤ} (h : 0 ≤ x) : x % (x + 1) = x
• Int.bmod_natAbs_add_one 📋 Init.Data.Int.DivMod.Lemmas
  (x : ℤ) (w : x ≠ -1) : x.bmod (x.natAbs + 1) = -x.sign
• Int.lt_fdiv_add_one_mul_self 📋 Init.Data.Int.DivMod.Lemmas
  (a : ℤ) {b : ℤ} (H : 0 < b) : a < (a.fdiv b + 1) * b
• Int.lt_tdiv_add_one_mul_self 📋 Init.Data.Int.DivMod.Lemmas
  (a : ℤ) {b : ℤ} (H : 0 < b) : a < (a.tdiv b + 1) * b
• Int.lt_ediv_add_one_mul_self 📋 Init.Data.Int.DivMod.Lemmas
  (a : ℤ) {b : ℤ} (H : 0 < b) : a < (a / b + 1) * b
• Int.bmod_self_add_one 📋 Init.Data.Int.DivMod.Lemmas
  {x : ℕ} : (↑x).bmod (x + 1) = if x = 0 then 0 else -1
• Int.le_emod_self_add_one_iff 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℤ} (h : 0 < b) : b ≤ a % b + 1 ↔ b ∣ a + 1
• Int.add_one_tdiv 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℤ} : (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 ∧ b ∣ a + 1 ∨ a < 0 ∧ b ∣ a then b.sign else 0
• Int.add_one_tdiv_of_pos 📋 Init.Data.Int.DivMod.Lemmas
  {a b : ℤ} (h : 0 < b) : (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 ∧ b ∣ a + 1 ∨ a < 0 ∧ b ∣ a then 1 else 0
• Int.ofNat_add_one_out 📋 Init.Data.Int.LemmasAux
  (n : ℕ) : ↑n + 1 = ↑n.succ
• BitVec.lt_add_one 📋 Init.Data.BitVec.Lemmas
  {w : ℕ} {b : BitVec w} (h : b ≠ BitVec.allOnes w) : b < b + 1
• UInt16.lt_add_one 📋 Init.Data.UInt.Lemmas
  {c : UInt16} (h : c ≠ -1) : c < c + 1
• UInt32.lt_add_one 📋 Init.Data.UInt.Lemmas
  {c : UInt32} (h : c ≠ -1) : c < c + 1
• UInt64.lt_add_one 📋 Init.Data.UInt.Lemmas
  {c : UInt64} (h : c ≠ -1) : c < c + 1
• UInt8.lt_add_one 📋 Init.Data.UInt.Lemmas
  {c : UInt8} (h : c ≠ -1) : c < c + 1
• USize.lt_add_one 📋 Init.Data.UInt.Lemmas
  {c : USize} (h : c ≠ -1) : c < c + 1
• UInt16.and_lt_add_one 📋 Init.Data.UInt.Bitwise
  {b c : UInt16} (h : c ≠ -1) : b &&& c < c + 1
• UInt32.and_lt_add_one 📋 Init.Data.UInt.Bitwise
  {b c : UInt32} (h : c ≠ -1) : b &&& c < c + 1
• UInt64.and_lt_add_one 📋 Init.Data.UInt.Bitwise
  {b c : UInt64} (h : c ≠ -1) : b &&& c < c + 1
• UInt8.and_lt_add_one 📋 Init.Data.UInt.Bitwise
  {b c : UInt8} (h : c ≠ -1) : b &&& c < c + 1
• USize.and_lt_add_one 📋 Init.Data.UInt.Bitwise
  {b c : USize} (h : c ≠ -1) : b &&& c < c + 1
• List.getElem?_intersperse_two_mul_add_one 📋 Init.Data.List.Nat.Basic
  {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : i + 1 < l.length) : (List.intersperse sep l)[2 * i + 1]? = some sep
• List.getElem_intersperse_two_mul_add_one 📋 Init.Data.List.Nat.Basic
  {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : 2 * i + 1 < (List.intersperse sep l).length) : (List.intersperse sep l)[2 * i + 1] = sep
• Array.ne_empty_of_size_eq_add_one 📋 Init.Data.Array.Lemmas
  {n : ℕ} {α✝ : Type u_1} {xs : Array α✝} (h : xs.size = n + 1) : xs ≠ #[]
• Array.exists_mem_of_size_eq_add_one 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n + 1) : ∃ a, a ∈ xs
• Array.exists_push_of_size_eq_add_one 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n + 1) : ∃ ys a, xs = ys.push a
• ByteArray.extract_add_one 📋 Init.Data.ByteArray.Lemmas
  {a : ByteArray} {i : ℕ} (ha : i + 1 ≤ a.size) : a.extract i (i + 1) = [a[i]].toByteArray
• Std.PRange.LawfulUpwardEnumerable.succMany?_add_one 📋 Init.Data.Range.Polymorphic.UpwardEnumerable
  {α : Type u} {inst✝ : Std.PRange.UpwardEnumerable α} [self : Std.PRange.LawfulUpwardEnumerable α] (n : ℕ) (a : α) : Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
• Std.PRange.UpwardEnumerable.succMany?_add_one 📋 Init.Data.Range.Polymorphic.UpwardEnumerable
  {α : Type u_1} [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α} : Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
• Std.PRange.UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany? 📋 Init.Data.Range.Polymorphic.UpwardEnumerable
  {α : Type u_1} [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {n : ℕ} {a : α} : Std.PRange.succMany? (n + 1) a = (Std.PRange.succ? a).bind fun x => Std.PRange.succMany? n x
• Std.PRange.UpwardEnumerable.succMany_add_one_eq_succMany_succ 📋 Init.Data.Range.Polymorphic.UpwardEnumerable
  {n : ℕ} {α : Type u} [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.InfinitelyUpwardEnumerable α] {a : α} : Std.PRange.succMany (n + 1) a = Std.PRange.succMany n (Std.PRange.succ a)
• Lean.Grind.NatModule.add_one_nsmul 📋 Init.Grind.Module.Basic
  {M : Type u} [self : Lean.Grind.NatModule M] (n : ℕ) (a : M) : (n + 1) • a = n • a + a
• Lean.Grind.Ring.intCast_natCast_add_one 📋 Init.Grind.Ring.Basic
  {α : Type u} [Lean.Grind.Ring α] (n : ℕ) : ↑(↑n + 1) = ↑n + 1
• Int16.toInt_maxValue_add_one 📋 Init.Data.SInt.Lemmas
  : Int16.maxValue.toInt + 1 = 2 ^ 15
• Int32.toInt_maxValue_add_one 📋 Init.Data.SInt.Lemmas
  : Int32.maxValue.toInt + 1 = 2 ^ 31
• Int64.toInt_maxValue_add_one 📋 Init.Data.SInt.Lemmas
  : Int64.maxValue.toInt + 1 = 2 ^ 63
• Int8.toInt_maxValue_add_one 📋 Init.Data.SInt.Lemmas
  : Int8.maxValue.toInt + 1 = 2 ^ 7
• ISize.toInt_maxValue_add_one 📋 Init.Data.SInt.Lemmas
  : ISize.maxValue.toInt + 1 = 2 ^ (System.Platform.numBits - 1)
• Lean.Grind.Field.zpow_add_one 📋 Init.Grind.Ring.Field
  {α : Type u_1} [Lean.Grind.Field α] {a : α} (h : a ≠ 0) (n : ℤ) : a ^ (n + 1) = a ^ n * a
• Rat.lt_floor_add_one 📋 Init.Data.Rat.Lemmas
  (a : ℚ) : a < ↑(a.floor + 1)
• Rat.zpow_add_one 📋 Init.Data.Rat.Lemmas
  {q : ℚ} (hq : q ≠ 0) (m : ℤ) : q ^ (m + 1) = q ^ m * q
• Int.trailingZeros_two_mul_add_one 📋 Init.Data.Dyadic.Basic
  (i : ℤ) : (2 * i + 1).trailingZeros = 0
• Std.Internal.List.Const.length_alterKey_eq_add_one 📋 Std.Data.Internal.List.Associative
  {α : Type u} [BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (h : Std.Internal.List.containsKey k l = false) (h' : (f (Std.Internal.List.getValue? k l)).isSome = true) : (Std.Internal.List.Const.alterKey k f l).length = l.length + 1
• Std.DHashMap.Internal.Raw₀.size_alter_eq_add_one 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : (↑m).WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isSome = true) : (↑(m.alter k f)).size = (↑m).size + 1
• Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_add_one 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (h : (↑m).WF) {k : α} {f : Option β → Option β} (h₁ : m.contains k = false) (h₂ : (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true) : (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size = (↑m).size + 1
• Std.DHashMap.size_alter_eq_add_one 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : k ∉ m) (h' : (f (m.get? k)).isSome = true) : (m.alter k f).size = m.size + 1
• Std.DHashMap.Const.size_alter_eq_add_one 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∉ m) (h' : (f (Std.DHashMap.Const.get? m k)).isSome = true) : (Std.DHashMap.Const.alter m k f).size = m.size + 1
• Std.DHashMap.Raw.size_alter_eq_add_one 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isSome = true) : (m.alter k f).size = m.size + 1
• Std.DHashMap.Raw.Const.size_alter_eq_add_one 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true) : (Std.DHashMap.Raw.Const.alter m k f).size = m.size + 1
• Std.HashMap.size_alter_eq_add_one 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∉ m) (h' : (f m[k]?).isSome = true) : (m.alter k f).size = m.size + 1
• Std.HashMap.Raw.size_alter_eq_add_one 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) (h₁ : k ∉ m) (h₂ : (f m[k]?).isSome = true) : (m.alter k f).size = m.size + 1
• Std.DTreeMap.Internal.Impl.Const.size_alter!_eq_add_one 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true) : (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size = t.size + 1
• Std.DTreeMap.Internal.Impl.size_alter!_eq_add_one 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : k ∉ t) (h₂ : (f (t.get? k)).isSome = true) : (Std.DTreeMap.Internal.Impl.alter! k f t).size = t.size + 1
• Std.DTreeMap.Internal.Impl.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : k ∉ t) (h₂ : (f (t.get? k)).isSome = true) : (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size = t.size + 1
• Std.DTreeMap.Internal.Impl.Const.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true) : (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size = t.size + 1
• Std.DTreeMap.Const.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f (Std.DTreeMap.Const.get? t k)).isSome = true) : (Std.DTreeMap.Const.alter t k f).size = t.size + 1
• Std.DTreeMap.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} (h₁ : k ∉ t) (h₂ : (f (t.get? k)).isSome = true) : (t.alter k f).size = t.size + 1
• Std.DTreeMap.Raw.Const.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true) : (Std.DTreeMap.Raw.Const.alter t k f).size = t.size + 1
• Std.DTreeMap.Raw.size_alter_eq_add_one 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : k ∉ t) (h₂ : (f (t.get? k)).isSome = true) : (t.alter k f).size = t.size + 1
• Std.TreeMap.size_alter_eq_add_one 📋 Std.Data.TreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f t[k]?).isSome = true) : (t.alter k f).size = t.size + 1
• Std.ExtDHashMap.Const.size_alter_eq_add_one 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∉ m) (h' : (f (Std.ExtDHashMap.Const.get? m k)).isSome = true) : (Std.ExtDHashMap.Const.alter m k f).size = m.size + 1
• Std.ExtDHashMap.size_alter_eq_add_one 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : k ∉ m) (h' : (f (m.get? k)).isSome = true) : (m.alter k f).size = m.size + 1
• Std.ExtHashMap.size_alter_eq_add_one 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∉ m) (h' : (f m[k]?).isSome = true) : (m.alter k f).size = m.size + 1
• Std.ExtDTreeMap.Const.size_alter_eq_add_one 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true) : (Std.ExtDTreeMap.Const.alter t k f).size = t.size + 1
• Std.ExtDTreeMap.size_alter_eq_add_one 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} (h₁ : k ∉ t) (h₂ : (f (t.get? k)).isSome = true) : (t.alter k f).size = t.size + 1
• Std.ExtTreeMap.size_alter_eq_add_one 📋 Std.Data.ExtTreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f t[k]?).isSome = true) : (t.alter k f).size = t.size + 1
• Std.TreeMap.Raw.size_alter_eq_add_one 📋 Std.Data.TreeMap.Raw.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∉ t) (h₂ : (f t[k]?).isSome = true) : (t.alter k f).size = t.size + 1
• List.length_tail_add_one 📋 Batteries.Data.List.Lemmas
  {α : Type u_1} (l : List α) (h : 0 < l.length) : l.tail.length + 1 = l.length
• Nat.le_add_one_of_avg_eq_left 📋 Batteries.Data.Nat.Bisect
  {a b : ℕ} (h : a.avg b = a) : b ≤ a + 1
• Nat.le_add_one_of_avg_eq_right 📋 Batteries.Data.Nat.Bisect
  {a b : ℕ} (h : a.avg b = b) : a ≤ b + 1
• Nat.bisect_add_one_false 📋 Batteries.Data.Nat.Bisect
  {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : p (Nat.bisect h hstart hstop + 1) = false
• Bool.ofNat_add_one 📋 Mathlib.Data.Bool.Basic
  {n : ℕ} : Bool.ofNat (n + 1) = true
• Nat.two_mul_ne_two_mul_add_one 📋 Mathlib.Data.Nat.Init
  {m n : ℕ} : 2 * n ≠ 2 * m + 1
• Nat.rec_add_one 📋 Mathlib.Data.Nat.Init
  {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ) : Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
• add_one_zsmul 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) : (n + 1) • a = n • a + a
• zpow_add_one 📋 Mathlib.Algebra.Group.Basic
  {G : Type u_3} [Group G] (a : G) (n : ℤ) : a ^ (n + 1) = a ^ n * a
• zpow_add_one₀ 📋 Mathlib.Algebra.GroupWithZero.Basic
  {G₀ : Type u_2} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) : a ^ (n + 1) = a ^ n * a
• Nat.cast_add_one 📋 Mathlib.Data.Nat.Cast.Defs
  {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : ↑(n + 1) = ↑n + 1
• one_add_one_eq_two 📋 Mathlib.Data.Nat.Cast.Defs
  {R : Type u_1} [AddMonoidWithOne R] : 1 + 1 = 2
• three_add_one_eq_four 📋 Mathlib.Data.Nat.Cast.Defs
  {R : Type u_1} [AddMonoidWithOne R] : 3 + 1 = 4
• two_add_one_eq_three 📋 Mathlib.Data.Nat.Cast.Defs
  {R : Type u_1} [AddMonoidWithOne R] : 2 + 1 = 3
• add_one_mul 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) : (a + 1) * b = a * b + b
• mul_add_one 📋 Mathlib.Algebra.Ring.Defs
  {α : Type u} [Add α] [MulOneClass α] [LeftDistribClass α] (a b : α) : a * (b + 1) = a * b + a
• Nat.cast_add_one_ne_zero 📋 Mathlib.Algebra.CharZero.Defs
  {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) : ↑n + 1 ≠ 0
• Int.inductionOn'_add_one 📋 Mathlib.Data.Int.Basic
  {C : ℤ → Sort u_1} {z b : ℤ} {H0 : C b} {Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)} {Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)} (hz : b ≤ z) : Int.inductionOn' (z + 1) b H0 Hs Hp = Hs z hz (Int.inductionOn' z b H0 Hs Hp)
• Nat.add_one_sqrt_le_of_ne_zero 📋 Mathlib.Data.Nat.Sqrt
  {n : ℕ} (hn : n ≠ 0) : (n + 1).sqrt ≤ n
• Nat.even_add_one 📋 Mathlib.Algebra.Group.Nat.Even
  {n : ℕ} : Even (n + 1) ↔ ¬Even n
• Nat.add_one_lt_of_even 📋 Mathlib.Algebra.Group.Nat.Even
  {m n : ℕ} (hn : Even n) (hm : Even m) (hnm : n < m) : n + 1 < m
• Nat.two_not_dvd_two_mul_add_one 📋 Mathlib.Algebra.Group.Nat.Even
  (n : ℕ) : ¬2 ∣ 2 * n + 1
• Int.even_add_one 📋 Mathlib.Algebra.Group.Int.Even
  {n : ℤ} : Even (n + 1) ↔ ¬Even n
• Int.two_not_dvd_two_mul_add_one 📋 Mathlib.Algebra.Group.Int.Even
  (n : ℤ) : ¬2 ∣ 2 * n + 1
• Nat.odd_add_one 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} : Odd (n + 1) ↔ ¬Odd n
• Nat.not_even_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  (n : ℕ) : ¬Even (2 * n + 1)
• Nat.two_dvd_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  (k : ℕ) : 2 ∣ k * (k + 1)
• Function.Involutive.iterate_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_4} {f : α → α} (hf : Function.Involutive f) (n : ℕ) : f^[2 * n + 1] = f
• Nat.div_two_mul_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : n / 2 * 2 + 1 = n
• Nat.two_mul_div_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Parity
  {n : ℕ} (h : Odd n) : 2 * (n / 2) + 1 = n
• Even.add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Even a) : Odd (a + 1)
• Odd.add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} (h : Odd a) : Even (a + 1)
• odd_add_one_self 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] {a : α} : Odd (a + 1 + a)
• odd_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  {α : Type u_2} [Semiring α] (a : α) : Odd (2 * a + 1)
• range_two_mul_add_one 📋 Mathlib.Algebra.Ring.Parity
  (α : Type u_4) [Semiring α] : (Set.range fun x => 2 * x + 1) = {a | Odd a}
• lt_add_one 📋 Mathlib.Algebra.Order.Monoid.NatCast
  {α : Type u_1} [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftStrictMono α] (a : α) : a < a + 1
• add_one_le_two_mul 📋 Mathlib.Algebra.Order.Ring.Unbundled.Basic
  {R : Type u} [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a
• Int.not_even_two_mul_add_one 📋 Mathlib.Algebra.Ring.Int.Parity
  (n : ℤ) : ¬Even (2 * n + 1)
• Int.two_dvd_mul_add_one 📋 Mathlib.Algebra.Ring.Int.Parity
  (k : ℤ) : 2 ∣ k * (k + 1)
• Int.ediv_two_mul_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → n / 2 * 2 + 1 = n
• Int.two_mul_ediv_two_add_one_of_odd 📋 Mathlib.Algebra.Ring.Int.Parity
  {n : ℤ} : Odd n → 2 * (n / 2) + 1 = n
• Nat.cast_add_one_pos 📋 Mathlib.Data.Nat.Cast.Order.Basic
  {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1] (n : ℕ) : 0 < ↑n + 1
• Nat.two_mul_sq_add_one_le_two_pow_two_mul 📋 Mathlib.Data.Nat.Cast.Order.Ring
  (k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)
• Nat.ceil_le_floor_add_one 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1
• Nat.add_one_le_ceil_iff 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} : n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
• Nat.lt_floor_add_one 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) : a < ↑⌊a⌋₊ + 1
• Nat.ceil_lt_add_one 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) : ↑⌈a⌉₊ < a + 1
• Nat.ceil_add_one 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1
• Nat.floor_add_one 📋 Mathlib.Algebra.Order.Floor.Semiring
  {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1
• div_add_one 📋 Mathlib.Algebra.Field.Basic
  {K : Type u_1} [DivisionSemiring K] {a b : K} (h : b ≠ 0) : a / b + 1 = (a + b) / b
• List.length_eraseIdx_add_one 📋 Mathlib.Data.List.Basic
  {ι : Type u_1} {l : List ι} {i : ℕ} (h : i < l.length) : (l.eraseIdx i).length + 1 = l.length
• List.length_erase_add_one 📋 Mathlib.Data.List.Basic
  {α : Type u} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (l.erase a).length + 1 = l.length
• List.length_eraseP_add_one 📋 Mathlib.Data.List.Basic
  {α : Type u} {p : α → Bool} {l : List α} {a : α} (al : a ∈ l) (pa : p a = true) : (List.eraseP p l).length + 1 = l.length
• Int.ceil_le_floor_add_one 📋 Mathlib.Algebra.Order.Floor.Ring
  {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : ⌈a⌉ ≤ ⌊a⌋ + 1
• Int.add_one_le_ceil_iff 📋 Mathlib.Algebra.Order.Floor.Ring
  {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : z + 1 ≤ ⌈a⌉ ↔ ↑z < 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.

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