Loogle!

Result

Found 2546 declarations mentioning HAdd.hAdd, LT.lt, and OfNat.ofNat. Of these, 32 match your pattern(s).

• Nat.add_one_pos 📋 Init.Data.Nat.Basic
  (n : ℕ) : 0 < n + 1
• Int.succ_ofNat_pos 📋 Init.Data.Int.Order
  (n : ℕ) : 0 < ↑n + 1
• Fin.add_one_pos 📋 Init.Data.Fin.Lemmas
  {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) : 0 < i + 1
• Fin.reverseInduction.go.eq_1 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1)) (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x : motive ⟨j, h⟩) : Fin.reverseInduction.go cast i j h h2 x = if hi : ↑i = j then _root_.cast ⋯ x else match j, h, h2, x, hi with | 0, h, h2, x, hi => ⋯.elim | j.succ, h, h2, x, hi => Fin.reverseInduction.go cast i j ⋯ ⋯ (cast ⟨j, ⋯⟩ x)
• Fin.reverseInduction.go.eq_def 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1)) (j : ℕ) (h : j < n + 1) (h2 : ↑i ≤ j) (x : motive ⟨j, h⟩) : Fin.reverseInduction.go cast i j h h2 x = if hi : ↑i = j then _root_.cast ⋯ x else match j, h, h2, x, hi with | 0, h, h2, x, hi => ⋯.elim | j.succ, h, h2, x, hi => Fin.reverseInduction.go cast i j ⋯ ⋯ (cast ⟨j, ⋯⟩ x)
• 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
• 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 ⋯
• Array.PrefixTable.step.eq_def 📋 Batteries.Data.Array.Match
  {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) (x✝ : Fin (t.size + 1)) : t.step x x✝ = match x✝ with | ⟨k, hk⟩ => have cont := fun x_1 => match k, hk with | 0, hk => ⟨0, ⋯⟩ | k.succ, hk => have h2 := ⋯; let k' := t.toArray[k].2; have hk' := ⋯; t.step x ⟨k', ⋯⟩; if hsz : k < t.size then if (x == t.toArray[k].1) = true then ⟨k + 1, ⋯⟩ else cont () else cont ()
• Fin.dfoldrM_loop_zero 📋 Batteries.Data.Fin.Fold
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} {h : 0 < n + 1} [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α ⟨0, h⟩) : Fin.dfoldrM.loop n α f 0 h x = pure x
• Nat.cast_add_one_pos 📋 Mathlib.Data.Nat.Cast.Order.Basic
  {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1] (n : ℕ) : 0 < ↑n + 1
• ENat.add_one_pos 📋 Mathlib.Data.ENat.Basic
  {n : ℕ∞} : 0 < n + 1
• geom_sum_pos' 📋 Mathlib.Algebra.Order.Ring.GeomSum
  {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : 0 < x + 1) (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i
• geom_sum_pos_iff 📋 Mathlib.Algebra.Order.Ring.GeomSum
  {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hn : n ≠ 0) : 0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1
• geom_sum_pos_and_lt_one 📋 Mathlib.Algebra.Order.Ring.GeomSum
  {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R} (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) : 0 < ∑ i ∈ Finset.range n, x ^ i ∧ ∑ i ∈ Finset.range n, x ^ i < 1
• CategoryTheory.ComposableArrows.homMk₀_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0} (f : F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ⟶ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.homMk₀ f).app i = match i with | ⟨0, isLt⟩ => f
• CategoryTheory.ComposableArrows.isoMk₀_hom_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0} (e : F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i = match i with | ⟨0, isLt⟩ => e.hom
• CategoryTheory.ComposableArrows.isoMk₀_inv_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0} (e : F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i = match i with | ⟨0, isLt⟩ => e.inv
• CategoryTheory.ComposableArrows.homMk₁_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⟶ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) (right : F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ⟶ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) right = CategoryTheory.CategoryStruct.comp left (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.homMk₁ left right w).app i = match i with | ⟨0, isLt⟩ => left | ⟨1, isLt⟩ => right
• CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (i : Fin (1 + 1)) : (G.mapComposableArrowsObjMk₁Iso f).hom.app i = match i with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X) | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
• CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (i : Fin (1 + 1)) : (G.mapComposableArrowsObjMk₁Iso f).inv.app i = match i with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X) | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
• CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (i : Fin (1 + 1 + 1)) : (G.mapComposableArrowsObjMk₂Iso f g).hom.app i = match i with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X) | ⟨i.succ, hi⟩ => match ⟨i, ⋯⟩ with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y) | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Z)
• CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (i : Fin (1 + 1 + 1)) : (G.mapComposableArrowsObjMk₂Iso f g).inv.app i = match i with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X) | ⟨i.succ, hi⟩ => match ⟨i, ⋯⟩ with | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y) | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Z)
• CategoryTheory.ComposableArrows.isoMk₁_hom_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) (right : F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.isoMk₁ left right w).hom.app i = match i with | ⟨0, isLt⟩ => left.hom | ⟨1, isLt⟩ => right.hom
• CategoryTheory.ComposableArrows.isoMk₁_inv_app 📋 Mathlib.CategoryTheory.ComposableArrows.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1} (left : F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4) (right : F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5) (w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.isoMk₁ left right w).inv.app i = match i with | ⟨0, isLt⟩ => left.inv | ⟨1, isLt⟩ => right.inv
• CategoryTheory.ComposableArrows.Precomp.map.eq_2 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
  {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (isLt : 0 < n + 1 + 1) (isLt_1 : 1 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) : CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f
• CategoryTheory.ComposableArrows.Precomp.map.eq_1 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
  {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (isLt isLt_1 : 0 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) : CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id X
• CategoryTheory.ComposableArrows.Precomp.map.eq_3 📋 Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
  {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ F.left) (isLt : 0 < n + 1 + 1) (j : ℕ) (hj : j + 2 < n + 1 + 1) (x_3 : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) : CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x_3 = CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
• CategoryTheory.ComposableArrows.Precomp.obj.eq_1 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C) (isLt : 0 < n + 1 + 1) : CategoryTheory.ComposableArrows.Precomp.obj F X ⟨0, isLt⟩ = X
• Nat.Primes.prodNatEquiv_apply 📋 Mathlib.Data.Nat.Factorization.PrimePow
  (p : Nat.Primes) (k : ℕ) : Nat.Primes.prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩
• SzemerediRegularity.coe_m_add_one_pos 📋 Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
  {α : Type u_1} [DecidableEq α] [Fintype α] {P : Finpartition Finset.univ} : 0 < ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1
• Int.succ_natCast_pos 📋 Mathlib.Data.Int.Lemmas
  (n : ℕ) : 0 < ↑n + 1

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 7379a9f