Loogle!

Result

Found 68 declarations whose name contains "until".

• String.nextUntil 📋 Init.Data.String.Basic
  (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos
• Lean.doElemRepeat__Until_ 📋 Init.While
  : Lean.ParserDescr
• String.Iterator.foldUntil 📋 Init.Data.String.Extra
  {α : Type u_1} (it : String.Iterator) (init : α) (f : α → Char → Option α) : α × String.Iterator
• String.Iterator.foldUntil.eq_def 📋 Init.Data.String.Extra
  {α : Type u_1} (it : String.Iterator) (init : α) (f : α → Char → Option α) : it.foldUntil init f = if it.atEnd = true then (init, it) else match f init it.curr with | some a => it.next.foldUntil a f | x => (init, it)
• IO.Condvar.waitUntil 📋 Init.System.Mutex
  {m : Type → Type u_1} [Monad m] [MonadLift BaseIO m] (condvar : IO.Condvar) (mutex : IO.BaseMutex) (pred : m Bool) : m Unit
• Std.Condvar.waitUntil 📋 Std.Sync.Mutex
  {m : Type → Type u_1} [Monad m] [MonadLiftT BaseIO m] (condvar : Std.Condvar) (mutex : Std.BaseMutex) (pred : m Bool) : m Unit
• Lean.Meta.whnfUntil 📋 Lean.Meta.WHNF
  (e : Lean.Expr) (declName : Lean.Name) : Lean.MetaM (Option Lean.Expr)
• Lean.Parser.takeUntilFn 📋 Lean.Parser.Basic
  (p : Char → Bool) : Lean.Parser.ParserFn
• Lean.Lsp.TextDocumentSyncOptions.willSaveWaitUntil 📋 Lean.Data.Lsp.TextSync
  (self : Lean.Lsp.TextDocumentSyncOptions) : Bool
• IO.AsyncList.waitUntil 📋 Lean.Server.AsyncList
  {α : Type u_1} {ε : Type u_2} (p : α → Bool) : IO.AsyncList ε α → Lean.Server.ServerTask (List α × Option ε)
• Lean.ParseImports.takeUntil 📋 Lean.Elab.ParseImportsFast
  (p : Char → Bool) : Lean.ParseImports.Parser
• Lean.Elab.Tactic.iterateUntilFailure 📋 Mathlib.Tactic.Core
  {m : Type → Type u} [Monad m] [MonadExcept Lean.Exception m] (tac : m Unit) : m Unit
• Lean.Elab.Tactic.iterateUntilFailureCount 📋 Mathlib.Tactic.Core
  {m : Type → Type u} [Monad m] [MonadExcept Lean.Exception m] {α : Type} (tac : m α) : m ℕ
• Lean.Elab.Tactic.iterateUntilFailureWithResults 📋 Mathlib.Tactic.Core
  {m : Type → Type u} [Monad m] [MonadExcept Lean.Exception m] {α : Type} (tac : m α) : m (List α)
• Lean.Meta.forallMetaTelescopeReducingUntilDefEq 📋 Mathlib.Lean.Meta.Basic
  (e t : Lean.Expr) (kind : Lean.MetavarKind := Lean.MetavarKind.natural) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
• SimpleGraph.Walk.dropUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.Walk u w
• SimpleGraph.Walk.takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.Walk v u
• SimpleGraph.Walk.takeUntil_first 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] (p : G.Walk u v) : p.takeUntil u ⋯ = SimpleGraph.Walk.nil
• SimpleGraph.Walk.takeUntil_nil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {h : u ∈ SimpleGraph.Walk.nil.support} : SimpleGraph.Walk.nil.takeUntil u h = SimpleGraph.Walk.nil
• SimpleGraph.Walk.nil_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk u v) (hwp : w ∈ p.support) : (p.takeUntil w hwp).Nil ↔ u = w
• SimpleGraph.Walk.length_dropUntil_le 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).length ≤ p.length
• SimpleGraph.Walk.length_takeUntil_le 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).length ≤ p.length
• SimpleGraph.Walk.support_dropUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).support ⊆ p.support
• SimpleGraph.Walk.support_takeUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).support ⊆ p.support
• SimpleGraph.Walk.snd_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (hsu : w ≠ u) (p : G.Walk u v) (h : w ∈ p.support) : (p.takeUntil w h).snd = p.snd
• SimpleGraph.Walk.count_support_takeUntil_eq_one 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : List.count u (p.takeUntil u h).support = 1
• SimpleGraph.Walk.edges_dropUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.edges_takeUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.length_takeUntil_lt 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (h : u ∈ p.support) (huw : u ≠ w) : (p.takeUntil u h).length < p.length
• SimpleGraph.Walk.darts_dropUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).darts ⊆ p.darts
• SimpleGraph.Walk.darts_takeUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).darts ⊆ p.darts
• SimpleGraph.Walk.takeUntil.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v : V} (x : V) (x_1 : x ∈ SimpleGraph.Walk.nil.support) : SimpleGraph.Walk.nil.takeUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil
• SimpleGraph.Walk.getVert_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {w : V} [DecidableEq V] {u v : V} {n : ℕ} {p : G.Walk u v} (hw : w ∈ p.support) (hn : n ≤ (p.takeUntil w hw).length) : (p.takeUntil w hw).getVert n = p.getVert n
• SimpleGraph.Walk.count_edges_takeUntil_le_one 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) : List.count s(u, x) (p.takeUntil u h).edges ≤ 1
• SimpleGraph.Walk.not_mem_support_takeUntil_support_takeUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {p : G.Walk u v} {w x : V} (h : x ≠ w) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) : w ∉ (p.takeUntil x ⋯).support
• SimpleGraph.Walk.takeUntil_cons 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] {v' : V} {p : G.Walk v' v} (hwp : w ∈ p.support) (h : u ≠ w) (hadj : G.Adj u v') : (SimpleGraph.Walk.cons hadj p).takeUntil w ⋯ = SimpleGraph.Walk.cons hadj (p.takeUntil w hwp)
• SimpleGraph.Walk.takeUntil_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {w x : V} (p : G.Walk u v) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) : (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯
• SimpleGraph.Walk.takeUntil.eq_2 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x v_1 : V) (r : G.Adj v v_1) (p : G.Walk v_1 w) (x_1 : x ∈ (SimpleGraph.Walk.cons r p).support) : (SimpleGraph.Walk.cons r p).takeUntil x x_1 = if hx : v = x then hx ▸ SimpleGraph.Walk.nil else SimpleGraph.Walk.cons r (p.takeUntil x ⋯)
• SimpleGraph.Walk.takeUntil.induct 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] (motive : {v w : V} → (p : G.Walk v w) → (u : V) → u ∈ p.support → Prop) (case1 : ∀ (a u : V) (h : u ∈ SimpleGraph.Walk.nil.support), motive SimpleGraph.Walk.nil u h) (case2 : ∀ (w v : V) (p : G.Walk v w) (u : V) (r : G.Adj u v) (h : u ∈ (SimpleGraph.Walk.cons r p).support), motive (SimpleGraph.Walk.cons r p) u h) (case3 : ∀ (a w v : V) (r : G.Adj a v) (p : G.Walk v w) (u : V) (h : u ∈ (SimpleGraph.Walk.cons r p).support) (h_1 : ¬a = u), motive p u ⋯ → motive (SimpleGraph.Walk.cons r p) u h) {v w : V} (p : G.Walk v w) (u : V) (a✝ : u ∈ p.support) : motive p u a✝
• SimpleGraph.Walk.dropUntil_copy 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u ∈ (p.copy hv hw).support) : (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw
• SimpleGraph.Walk.takeUntil_copy 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u ∈ (p.copy hv hw).support) : (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯
• SimpleGraph.Walk.IsCycle.isPath_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} {v w : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) (h : w ∈ c.support) : (c.takeUntil w h).IsPath
• SimpleGraph.Walk.IsPath.dropUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.dropUntil u h).IsPath
• SimpleGraph.Walk.IsPath.takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.takeUntil u h).IsPath
• SimpleGraph.Walk.IsTrail.dropUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u ∈ p.support) : (p.dropUntil u h).IsTrail
• SimpleGraph.Walk.IsTrail.takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u ∈ p.support) : (p.takeUntil u h).IsTrail
• SimpleGraph.Walk.endpoint_not_mem_support_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w ∈ p.support) (h : v ≠ w) : v ∉ (p.takeUntil w hw).support
• SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) : ∃ x ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
• Estimator.improveUntil 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) : Except (Option ε) ε
• Estimator.improveUntilAux 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : Except (Option ε) ε
• Estimator.improveUntil_spec 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) : match Estimator.improveUntil a p e with | Except.error a_1 => ¬p a.get = true | Except.ok e' => p (EstimatorData.bound a e') = true
• Estimator.improveUntilAux_spec 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : match Estimator.improveUntilAux a p e r with | Except.error a_1 => ¬p a.get = true | Except.ok e' => p (EstimatorData.bound a e') = true
• Estimator.improveUntilAux.eq_1 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : Estimator.improveUntilAux a p e r = if p (EstimatorData.bound a e) = true then pure e else match EstimatorData.improve a e, ⋯ with | none, x => Except.error (if r = true then none else some e) | some e', x => Estimator.improveUntilAux a p e' true
• Estimator.improveUntilAux.eq_def 📋 Mathlib.Order.Estimator
  {α : Type u_1} {ε : Type u_2} [Preorder α] (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : Estimator.improveUntilAux a p e r = if p (EstimatorData.bound a e) = true then pure e else match EstimatorData.improve a e, ⋯ with | none, x => Except.error (if r = true then none else some e) | some e', x => Estimator.improveUntilAux a p e' true
• PreTilt.untiltAux 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) (n : ℕ) : O
• PreTilt.untiltAux.eq_1 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) : x.untiltAux 0 = 1
• PreTilt.untiltFun 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) : O
• PreTilt.untilt 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] : PreTilt O p →* O
• PreTilt.pow_dvd_untiltAux_sub_untiltAux 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) {m n : ℕ} (h : m ≤ n) : ↑p ^ m ∣ x.untiltAux m - x.untiltAux n
• PreTilt.pow_dvd_one_untiltAux_sub_one 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (m : ℕ) : ↑p ^ m ∣ PreTilt.untiltAux 1 m - 1
• PreTilt.untiltAux_smodEq_untiltFun 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) (n : ℕ) : x.untiltAux n ≡ x.untiltFun [SMOD Ideal.span {↑p} ^ n]
• PreTilt.pow_dvd_mul_untiltAux_sub_untiltAux_mul 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x y : PreTilt O p) (m : ℕ) : ↑p ^ m ∣ (x * y).untiltAux m - x.untiltAux m * y.untiltAux m
• PreTilt.untilt.eq_1 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] : PreTilt.untilt = { toFun := PreTilt.untiltFun, map_one' := ⋯, map_mul' := ⋯ }
• PreTilt.untiltFun.eq_1 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) : x.untiltFun = Classical.choose ⋯
• PreTilt.exists_smodEq_untiltAux 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsPrecomplete (Ideal.span {↑p}) O] (x : PreTilt O p) : ∃ y, ∀ (n : ℕ), x.untiltAux n ≡ y [SMOD Ideal.span {↑p} ^ n • ⊤]
• PreTilt.untiltAux.eq_2 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] (x : PreTilt O p) (n_2 : ℕ) : x.untiltAux n_2.succ = Quotient.out ((Perfection.coeff (ModP O p) p n_2) x) ^ p ^ n_2
• PreTilt.mk_untilt_eq_coeff_zero 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] (x : PreTilt O p) : (Ideal.Quotient.mk (Ideal.span {↑p})) (PreTilt.untilt x) = (Perfection.coeff (ModP O p) p 0) x
• PreTilt.mk_comp_untilt_eq_coeff_zero 📋 Mathlib.RingTheory.Perfectoid.Untilt
  {O : Type u_1} [CommRing O] {p : ℕ} [Fact (Nat.Prime p)] [Fact ¬IsUnit ↑p] [IsAdicComplete (Ideal.span {↑p}) O] : ⇑(Ideal.Quotient.mk (Ideal.span {↑p})) ∘ ⇑PreTilt.untilt = ⇑(Perfection.coeff (ModP O p) p 0)

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 19971e9 serving mathlib revision 5f22769