Loogle!

Result

Found 892 declarations whose name contains "Ulift". Of these, only the first 200 are shown.

• PULift 📋 Init.Prelude
  (α : Sort s) : Sort (max s r 1)
• ULift 📋 Init.Prelude
  (α : Type s) : Type (max s r)
• PULift.down 📋 Init.Prelude
  {α : Sort s} (self : PULift α) : α
• PULift.up 📋 Init.Prelude
  {α : Sort s} (down : α) : PULift α
• ULift.down 📋 Init.Prelude
  {α : Type s} (self : ULift.{r, s} α) : α
• ULift.up 📋 Init.Prelude
  {α : Type s} (down : α) : ULift.{r, s} α
• instInhabitedULift 📋 Init.Prelude
  {α : Type u_1} [Inhabited α] : Inhabited (ULift.{u_2, u_1} α)
• PULift.down_up 📋 Init.Prelude
  {α : Sort u} (a : α) : { down := a }.down = a
• ULift.down_up 📋 Init.Prelude
  {α : Type u} (a : α) : { down := a }.down = a
• PULift.up_down 📋 Init.Prelude
  {α : Sort u} (b : PULift α) : { down := b.down } = b
• ULift.up_down 📋 Init.Prelude
  {α : Type u} (b : ULift.{v, u} α) : { down := b.down } = b
• ULift.up.sizeOf_spec 📋 Init.SizeOf
  {α : Type s} [SizeOf α] (down : α) : sizeOf { down := down } = 1 + sizeOf down
• PULift.up.injEq 📋 Init.Core
  {α : Sort s} (down down✝ : α) : ({ down := down } = { down := down✝ }) = (down = down✝)
• ULift.up.injEq 📋 Init.Core
  {α : Type s} (down down✝ : α) : ({ down := down } = { down := down✝ }) = (down = down✝)
• instReprULift 📋 Init.Data.Repr
  {α : Type u_1} [Repr α] : Repr (ULift.{v, u_1} α)
• instToStringULift 📋 Init.Data.ToString.Basic
  {α : Type u} [ToString α] : ToString (ULift.{v, u} α)
• Std.Iterators.ULiftT 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  (n : Type (max u v) → Type v') (α : Type u) : Type v'
• Std.Iterators.instMonadULiftT 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] : Monad (Std.Iterators.ULiftT n)
• Std.Iterators.ULiftT.run 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} {α : Type u} (x : Std.Iterators.ULiftT n α) : n (ULift.{v, u} α)
• Std.Iterators.instLawfulMonadULiftT 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] [LawfulMonad n] : LawfulMonad (Std.Iterators.ULiftT n)
• Std.Iterators.Types.ULiftIterator 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  (α : Type u) (m : Type u → Type u') (n : Type (max u v) → Type v') (β : Type u) (lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ) : Type (max u v)
• Std.Iterators.Types.ULiftIterator.inner 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (self : Std.Iterators.Types.ULiftIterator α m n β lift) : Std.IterM m β
• Std.Iterators.Types.ULiftIterator.mk 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (inner : Std.IterM m β) : Std.Iterators.Types.ULiftIterator α m n β lift
• Std.Iterators.Types.ULiftIterator.instIterator 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [Std.Iterators.Iterator α m β] [Monad n] : Std.Iterators.Iterator (Std.Iterators.Types.ULiftIterator α m n β lift) n (ULift.{v, u} β)
• Std.Iterators.IterM.uLift 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {β : Type u} (it : Std.IterM m β) (n : Type (max u v) → Type v') [lift : MonadLiftT m (Std.Iterators.ULiftT n)] : Std.IterM n (ULift.{v, u} β)
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (step : Std.Iterators.IterStep (Std.IterM m β) β) : Std.Iterators.IterStep (Std.IterM n (ULift.{v, u} β)) (ULift.{v, u} β)
• Std.Iterators.ULiftT.run_pure 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] {α : Type u} {a : α} : (pure a).run = pure { down := a }
• Std.Iterators.Types.ULiftIterator.instFinite 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Monad n] : Std.Iterators.Finite (Std.Iterators.Types.ULiftIterator α m n β lift) n
• Std.Iterators.Types.ULiftIterator.instFinitenessRelation 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [Std.Iterators.Iterator α m β] [Std.Iterators.Finite α m] [Monad n] : Std.Iterators.FinitenessRelation (Std.Iterators.Types.ULiftIterator α m n β lift) n
• Std.Iterators.Types.ULiftIterator.instIteratorCollect 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} {o : Type (max u v) → Type u_1} [Monad n] [Monad o] [Std.Iterators.Iterator α m β] : Std.Iterators.IteratorCollect (Std.Iterators.Types.ULiftIterator α m n β lift) n o
• Std.Iterators.Types.ULiftIterator.instIteratorLoop 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} {o : Type x → Type x'} [Monad n] [Monad o] [Std.Iterators.Iterator α m β] : Std.Iterators.IteratorLoop (Std.Iterators.Types.ULiftIterator α m n β lift) n o
• Std.Iterators.Types.ULiftIterator.instProductive 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [Std.Iterators.Iterator α m β] [Std.Iterators.Productive α m] [Monad n] : Std.Iterators.Productive (Std.Iterators.Types.ULiftIterator α m n β lift) n
• Std.Iterators.Types.ULiftIterator.instProductivenessRelation 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [Std.Iterators.Iterator α m β] [Std.Iterators.Productive α m] [Monad n] : Std.Iterators.ProductivenessRelation (Std.Iterators.Types.ULiftIterator α m n β lift) n
• Std.Iterators.Types.ULiftIterator.mk.injEq 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (inner inner✝ : Std.IterM m β) : ({ inner := inner } = { inner := inner✝ }) = (inner = inner✝)
• Std.Iterators.ULiftT.run_bind 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] {α β : Type u} {x : Std.Iterators.ULiftT n α} {f : α → Std.Iterators.ULiftT n β} : (x >>= f).run = do let a ← x.run (f a.down).run
• Std.Iterators.ULiftT.run_map 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {n : Type (max u v) → Type v'} [Monad n] {α β : Type u} {x : Std.Iterators.ULiftT n α} {f : α → β} : (f <$> x).run = do let a ← x.run pure { down := f a.down }
• Std.Iterators.Types.ULiftIterator.mk.sizeOf_spec 📋 Init.Data.Iterators.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [SizeOf α] [(a : Type u) → SizeOf (m a)] [(a : Type (max u v)) → SizeOf (n a)] [SizeOf β] (inner : Std.IterM m β) : sizeOf { inner := inner } = 1 + sizeOf inner
• Std.Iterators.Iter.uLift 📋 Init.Data.Iterators.Combinators.ULift
  {α β : Type u} (it : Std.Iter β) : Std.Iter (ULift.{v, u} β)
• Std.Iterators.Types.ULiftIterator.modifyStep 📋 Init.Data.Iterators.Combinators.ULift
  {α β : Type u} (step : Std.Iterators.IterStep (Std.Iter β) β) : Std.Iterators.IterStep (Std.Iter (ULift.{v, u} β)) (ULift.{v, u} β)
• instDecidableEqULift 📋 Init.Data.ULift
  {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ULift.{u_2, u_1} α✝)
• instSubsingletonULift 📋 Init.Data.ULift
  {α : Type u_1} [Subsingleton α] : Subsingleton (ULift.{u_2, u_1} α)
• instDecidableEqULift.decEq 📋 Init.Data.ULift
  {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : ULift.{u_2, u_1} α✝) : Decidable (x✝ = x✝¹)
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_3 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} : Std.Iterators.Types.ULiftIterator.Monadic.modifyStep Std.Iterators.IterStep.done = Std.Iterators.IterStep.done
• Std.Iterators.IterM.uLift.eq_1 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {β : Type u} (it : Std.IterM m β) (n : Type (max u v) → Type v') [lift : MonadLiftT m (Std.Iterators.ULiftT n)] : it.uLift n = { internalState := { inner := it } }
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_2 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (it' : Std.IterM m β) : Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.Iterators.IterStep.skip it') = Std.Iterators.IterStep.skip { internalState := { inner := it' } }
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_1 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (it' : Std.IterM m β) (out : β) : Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.Iterators.IterStep.yield it' out) = Std.Iterators.IterStep.yield { internalState := { inner := it' } } { down := out }
• Std.Iterators.IterM.toListRev_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toListRev = (fun l => List.map ULift.up l.down) <$> (monadLift it.toListRev).run
• Std.Iterators.IterM.count_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorLoop α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorLoop α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).count = (fun x => { down := x.down.down }) <$> (monadLift it.count).run
• Std.Iterators.IterM.toArray_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toArray = (fun l => Array.map ULift.up l.down) <$> (monadLift it.toArray).run
• Std.Iterators.IterM.toList_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad m] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [Std.Iterators.IteratorCollect α m m] [LawfulMonad m] [LawfulMonad n] [Std.Iterators.LawfulIteratorCollect α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).toList = (fun l => List.map ULift.up l.down) <$> (monadLift it.toList).run
• Std.Iterators.IterM.step_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
  {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Std.Iterators.Iterator α m β] [Monad n] {it : Std.IterM m β} [MonadLiftT m (Std.Iterators.ULiftT n)] : (it.uLift n).step = do let __do_lift ← (monadLift it.step).run match __do_lift.down.inflate with | ⟨Std.Iterators.IterStep.yield it' out, h⟩ => pure (Std.Shrink.deflate (Std.Iterators.PlausibleIterStep.yield (it'.uLift n) { down := out } ⋯)) | ⟨Std.Iterators.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.Iterators.PlausibleIterStep.skip (it'.uLift n) ⋯)) | ⟨Std.Iterators.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.Iterators.PlausibleIterStep.done ⋯))
• Std.Iterators.Iter.uLift_eq_toIter_uLift_toIterM 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} {it : Std.Iter β} : it.uLift = (it.toIterM.uLift Id).toIter
• Std.Iterators.Iter.toListRev_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id] [Std.Iterators.LawfulIteratorCollect α Id Id] : it.uLift.toListRev = List.map ULift.up it.toListRev
• Std.Iterators.Iter.count_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] [Std.Iterators.IteratorLoop α Id Id] [Std.Iterators.LawfulIteratorLoop α Id Id] : it.uLift.count = it.count
• Std.Iterators.Iter.toArray_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id] [Std.Iterators.LawfulIteratorCollect α Id Id] : it.uLift.toArray = Array.map ULift.up it.toArray
• Std.Iterators.Iter.toList_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] [Std.Iterators.IteratorCollect α Id Id] [Std.Iterators.LawfulIteratorCollect α Id Id] : it.uLift.toList = List.map ULift.up it.toList
• Std.Iterators.Iter.step_uLift 📋 Init.Data.Iterators.Lemmas.Combinators.ULift
  {α β : Type u} [Std.Iterators.Iterator α Id β] {it : Std.Iter β} : it.uLift.step = match it.step with | ⟨Std.Iterators.IterStep.yield it' out, h⟩ => Std.Iterators.PlausibleIterStep.yield it'.uLift { down := out } ⋯ | ⟨Std.Iterators.IterStep.skip it', h⟩ => Std.Iterators.PlausibleIterStep.skip it'.uLift ⋯ | ⟨Std.Iterators.IterStep.done, h⟩ => Std.Iterators.PlausibleIterStep.done ⋯
• ULift.down_ite 📋 Std.Do.SPred.DerivedLaws
  {α : Type u_1} {φ : Prop} [Decidable φ] (t e : α) : (if φ then { down := t } else { down := e }).down = if φ then t else e
• ULift.down_dite 📋 Std.Do.SPred.DerivedLaws
  {α : Type u_1} {φ : Prop} [Decidable φ] (t : φ → α) (e : ¬φ → α) : (if h : φ then { down := t h } else { down := e h }).down = if h : φ then t h else e h
• Std.Do.SPred.Tactic.instHasFrameCurryULiftPropUpAndOfAnd 📋 Std.Do.SPred.DerivedLaws
  {φ : Prop} (σs : List (Type u_1)) (P P' : Std.Do.SVal.StateTuple σs → Prop) (Q : Std.Do.SPred σs) [Std.Do.SPred.Tactic.HasFrame spred((Std.Do.SVal.curry fun t => { down := P t }) ∧ Std.Do.SVal.curry fun t => { down := P' t }) Q φ] : Std.Do.SPred.Tactic.HasFrame (Std.Do.SVal.curry fun t => { down := P t ∧ P' t }) Q φ
• nonempty_ulift 📋 Mathlib.Logic.Nonempty
  {α : Type u_1} : Nonempty (ULift.{u_4, u_1} α) ↔ Nonempty α
• isEmpty_ulift 📋 Mathlib.Logic.IsEmpty
  {α : Type u_4} : IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
• Equiv.ulift 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} : ULift.{u, v} α ≃ α
• Equiv.sigmaULiftPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P
• Equiv.ulift_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} : ⇑Equiv.ulift = ULift.down
• Equiv.ulift_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} : ⇑Equiv.ulift.symm = ULift.up
• ULift.down_injective 📋 Mathlib.Logic.Function.ULift
  {α : Type u_1} : Function.Injective ULift.down
• ULift.down_inj 📋 Mathlib.Logic.Function.ULift
  {α : Type u_1} {a b : ULift.{u_2, u_1} α} : a.down = b.down ↔ a = b
• ULift.instBEq_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [BEq α] : BEq (ULift.{v, u} α)
• ULift.instHasCompl 📋 Mathlib.Order.ULift
  {α : Type u} [HasCompl α] : HasCompl (ULift.{v, u} α)
• ULift.instLE_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [LE α] : LE (ULift.{v, u} α)
• ULift.instLT_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [LT α] : LT (ULift.{v, u} α)
• ULift.instMax_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [Max α] : Max (ULift.{v, u} α)
• ULift.instMin_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [Min α] : Min (ULift.{v, u} α)
• ULift.instOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [Ord α] : Ord (ULift.{v, u} α)
• ULift.instPartialOrder 📋 Mathlib.Order.ULift
  {α : Type u} [PartialOrder α] : PartialOrder (ULift.{v, u} α)
• ULift.instPreorder 📋 Mathlib.Order.ULift
  {α : Type u} [Preorder α] : Preorder (ULift.{v, u} α)
• ULift.instSDiff_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [SDiff α] : SDiff (ULift.{v, u} α)
• ULift.instOrientedOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [Ord α] [inst : Std.OrientedOrd α] : Std.OrientedOrd (ULift.{v, u} α)
• ULift.instTransOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [Ord α] [inst : Std.TransOrd α] : Std.TransOrd (ULift.{v, u} α)
• ULift.instLawfulBEqOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [BEq α] [Ord α] [inst : Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (ULift.{v, u} α)
• ULift.instLawfulLEOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [LE α] [Ord α] [inst : Std.LawfulLEOrd α] : Std.LawfulLEOrd (ULift.{v, u} α)
• ULift.instLawfulLTOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [LT α] [Ord α] [inst : Std.LawfulLTOrd α] : Std.LawfulLTOrd (ULift.{v, u} α)
• ULift.down_compl 📋 Mathlib.Order.ULift
  {α : Type u} [HasCompl α] (a : ULift.{u_1, u} α) : aᶜ.down = a.downᶜ
• ULift.up_compl 📋 Mathlib.Order.ULift
  {α : Type u} [HasCompl α] (a : α) : { down := aᶜ } = { down := a }ᶜ
• ULift.up_le 📋 Mathlib.Order.ULift
  {α : Type u} [LE α] {a b : α} : { down := a } ≤ { down := b } ↔ a ≤ b
• ULift.up_lt 📋 Mathlib.Order.ULift
  {α : Type u} [LT α] {a b : α} : { down := a } < { down := b } ↔ a < b
• ULift.up_beq 📋 Mathlib.Order.ULift
  {α : Type u} [BEq α] (a b : α) : ({ down := a } == { down := b }) = (a == b)
• ULift.up_compare 📋 Mathlib.Order.ULift
  {α : Type u} [Ord α] (a b : α) : compare { down := a } { down := b } = compare a b
• ULift.down_le 📋 Mathlib.Order.ULift
  {α : Type u} [LE α] {a b : ULift.{u_1, u} α} : a.down ≤ b.down ↔ a ≤ b
• ULift.down_lt 📋 Mathlib.Order.ULift
  {α : Type u} [LT α] {a b : ULift.{u_1, u} α} : a.down < b.down ↔ a < b
• ULift.down_beq 📋 Mathlib.Order.ULift
  {α : Type u} [BEq α] (a b : ULift.{u_1, u} α) : (a.down == b.down) = (a == b)
• ULift.down_compare 📋 Mathlib.Order.ULift
  {α : Type u} [Ord α] (a b : ULift.{u_1, u} α) : compare a.down b.down = compare a b
• ULift.up_inf 📋 Mathlib.Order.ULift
  {α : Type u} [Min α] (a b : α) : { down := a ⊓ b } = { down := a } ⊓ { down := b }
• ULift.up_sdiff 📋 Mathlib.Order.ULift
  {α : Type u} [SDiff α] (a b : α) : { down := a \ b } = { down := a } \ { down := b }
• ULift.up_sup 📋 Mathlib.Order.ULift
  {α : Type u} [Max α] (a b : α) : { down := a ⊔ b } = { down := a } ⊔ { down := b }
• ULift.down_inf 📋 Mathlib.Order.ULift
  {α : Type u} [Min α] (a b : ULift.{u_1, u} α) : (a ⊓ b).down = a.down ⊓ b.down
• ULift.down_sdiff 📋 Mathlib.Order.ULift
  {α : Type u} [SDiff α] (a b : ULift.{u_1, u} α) : (a \ b).down = a.down \ b.down
• ULift.down_sup 📋 Mathlib.Order.ULift
  {α : Type u} [Max α] (a b : ULift.{u_1, u} α) : (a ⊔ b).down = a.down ⊔ b.down
• ULift.instMax_mathlib.eq_1 📋 Mathlib.Order.ULift
  {α : Type u} [Max α] : ULift.instMax_mathlib = { max := fun x y => { down := x.down ⊔ y.down } }
• ULift.instMin_mathlib.eq_1 📋 Mathlib.Order.ULift
  {α : Type u} [Min α] : ULift.instMin_mathlib = { min := fun x y => { down := x.down ⊓ y.down } }
• ULift.instLawfulBOrd_mathlib 📋 Mathlib.Order.ULift
  {α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Std.LawfulBOrd α] : Std.LawfulBOrd (ULift.{v, u} α)
• ULift.instBot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : Bot (ULift.{v, u} α)
• ULift.instTop 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : Top (ULift.{v, u} α)
• ULift.instBoundedOrder 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [BoundedOrder α] : BoundedOrder (ULift.{v, u} α)
• ULift.instOrderBot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderBot α] : OrderBot (ULift.{v, u} α)
• ULift.instOrderTop 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderTop α] : OrderTop (ULift.{v, u} α)
• ULift.down_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : ⊥.down = ⊥
• ULift.down_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : ⊤.down = ⊤
• ULift.up_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : { down := ⊥ } = ⊥
• ULift.up_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : { down := ⊤ } = ⊤
• ULift.instBot.eq_1 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : ULift.instBot = { bot := { down := ⊥ } }
• ULift.instTop.eq_1 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : ULift.instTop = { top := { down := ⊤ } }
• Mathlib.instToExprULift_mathlib 📋 Mathlib.Tactic.ToExpr
  {α✝ : Type s} [Lean.ToExpr α✝] [Lean.ToLevel] [Lean.ToLevel] : Lean.ToExpr (ULift.{r, s} α✝)
• Mathlib.instToExprULift_mathlib.toExpr 📋 Mathlib.Tactic.ToExpr
  {α✝ : Type s} [Lean.ToExpr α✝] : Lean.ToLevel → Lean.ToLevel → ULift.{r, s} α✝ → Lean.Expr
• ULift.instDistribLattice 📋 Mathlib.Order.Lattice
  {α : Type u} [DistribLattice α] : DistribLattice (ULift.{v, u} α)
• ULift.instLattice 📋 Mathlib.Order.Lattice
  {α : Type u} [Lattice α] : Lattice (ULift.{v, u} α)
• ULift.instLinearOrder 📋 Mathlib.Order.Lattice
  {α : Type u} [LinearOrder α] : LinearOrder (ULift.{v, u} α)
• ULift.instSemilatticeInf 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeInf α] : SemilatticeInf (ULift.{v, u} α)
• ULift.instSemilatticeSup 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeSup α] : SemilatticeSup (ULift.{v, u} α)
• ULift.instSemilatticeInf.eq_1 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeInf α] : ULift.instSemilatticeInf = Function.Injective.semilatticeInf ULift.down ⋯ ⋯
• ULift.instSemilatticeSup.eq_1 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeSup α] : ULift.instSemilatticeSup = Function.Injective.semilatticeSup ULift.down ⋯ ⋯
• Equiv.ulift_symm_down 📋 Mathlib.Logic.Equiv.Basic
  {α : Type v} (x : α) : (Equiv.ulift.symm x).down = x
• Plausible.ULift.Arbitrary 📋 Plausible.Arbitrary
  {α : Type (max u_1 u_2)} [Plausible.Arbitrary α] : Plausible.Arbitrary (ULift.{u_2, max u_1 u_2} α)
• Plausible.ULift.sampleableExt 📋 Plausible.Sampleable
  {α : Type u_1} [Plausible.SampleableExt α] : Plausible.SampleableExt (ULift.{u_3, u_1} α)
• Plausible.ULift.shrinkable 📋 Plausible.Sampleable
  {α : Type u_1} [Plausible.Shrinkable α] : Plausible.Shrinkable (ULift.{u_2, u_1} α)
• Plausible.Testable.forallTypesULiftTestable 📋 Plausible.Testable
  {var : String} {f : Type u → Prop} [Plausible.Testable (f (ULift.{u, 0} ℤ))] : Plausible.Testable (Plausible.NamedBinder var (∀ (x : Type u), f x))
• RelIso.IsWellOrder.ulift 📋 Mathlib.Order.RelIso.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : IsWellOrder (ULift.{u_5, u} α) (ULift.down ⁻¹'o r)
• ULift.orderIso 📋 Mathlib.Order.Hom.Basic
  {α : Type u} [Preorder α] : ULift.{v, u} α ≃o α
• OrderHom.uliftLeftMap 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ULift.{u_8, u_2} α →o β
• OrderHom.uliftRightMap 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : α →o ULift.{u_8, u_3} β
• OrderHom.uliftMap 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ULift.{u_8, u_2} α →o ULift.{u_9, u_3} β
• OrderHom.uliftLeftMap_uliftRightMap_eq 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : f.uliftLeftMap.uliftRightMap = f.uliftMap
• OrderHom.uliftRightMap_uliftLeftMap_eq 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : f.uliftRightMap.uliftLeftMap = f.uliftMap
• OrderHom.uliftRightMap_coe_down 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : α) : (f.uliftRightMap i).down = f i
• OrderHom.uliftLeftMap_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) : f.uliftLeftMap i = f i.down
• OrderHom.uliftMap_coe_down 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) : (f.uliftMap i).down = f i.down
• ULift.orderIso_apply 📋 Mathlib.Order.Hom.Basic
  {α : Type u} [Preorder α] (self : ULift.{v, u} α) : ULift.orderIso.{v, u} self = self.down
• ULift.orderIso_symm_apply_down 📋 Mathlib.Order.Hom.Basic
  {α : Type u} [Preorder α] (down : α) : ((RelIso.symm ULift.orderIso.{v, u}) down).down = down
• ULift.instWellFoundedGT 📋 Mathlib.Order.WellFounded
  {α : Type u_1} [LT α] [WellFoundedGT α] : WellFoundedGT (ULift.{u_4, u_1} α)
• ULift.instWellFoundedLT 📋 Mathlib.Order.WellFounded
  {α : Type u_1} [LT α] [h : WellFoundedLT α] : WellFoundedLT (ULift.{u_4, u_1} α)
• ULift.instMonad_mathlib 📋 Mathlib.Control.ULift
  : Monad ULift.{u_2, u_1}
• ULift.instLawfulMonad_mathlib 📋 Mathlib.Control.ULift
  : LawfulMonad ULift.{u_2, u_1}
• ULift.pure 📋 Mathlib.Control.ULift
  {α : Type u} : α → ULift.{u_1, u} α
• ULift.instLawfulApplicative_mathlib 📋 Mathlib.Control.ULift
  : LawfulApplicative ULift.{u_2, u_1}
• ULift.instLawfulFunctor_mathlib 📋 Mathlib.Control.ULift
  : LawfulFunctor ULift.{u_2, u_1}
• ULift.map 📋 Mathlib.Control.ULift
  {α : Type u} {β : Type v} (f : α → β) (a : ULift.{u', u} α) : ULift.{v', v} β
• ULift.bind 📋 Mathlib.Control.ULift
  {α : Type u} {β : Type v} (a : ULift.{u_1, u} α) (f : α → ULift.{u_2, v} β) : ULift.{u_2, v} β
• ULift.pure.eq_1 📋 Mathlib.Control.ULift
  {α : Type u} : ULift.pure = ULift.up
• ULift.seq 📋 Mathlib.Control.ULift
  {α : Type u_1} {β : Type u_2} (f : ULift.{u_3, max u_1 u_2} (α → β)) (x : Unit → ULift.{u_4, u_1} α) : ULift.{u, u_2} β
• ULift.rec.constant 📋 Mathlib.Control.ULift
  {α : Type u} {β : Sort v} (b : β) : (ULift.rec fun x => b) = fun x => b
• ULift.bind_up 📋 Mathlib.Control.ULift
  {α : Type u} {β : Type v} (a : α) (f : α → ULift.{u_1, v} β) : { down := a }.bind f = f a
• ULift.map_up 📋 Mathlib.Control.ULift
  {α : Type u} {β : Type v} (f : α → β) (a : α) : ULift.map f { down := a } = { down := f a }
• ULift.seq_up 📋 Mathlib.Control.ULift
  {α : Type u} {β : Type v} (f : α → β) (x : α) : ({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
• ULift.instDecidableEq_mathlib 📋 Mathlib.Data.ULift
  {α : Type u} [DecidableEq α] : DecidableEq (ULift.{u_1, u} α)
• ULift.instIsEmpty 📋 Mathlib.Data.ULift
  {α : Type u} [IsEmpty α] : IsEmpty (ULift.{u_1, u} α)
• ULift.instNonempty_mathlib 📋 Mathlib.Data.ULift
  {α : Type u} [Nonempty α] : Nonempty (ULift.{u_1, u} α)
• ULift.instSubsingleton_mathlib 📋 Mathlib.Data.ULift
  {α : Type u} [Subsingleton α] : Subsingleton (ULift.{u_1, u} α)
• ULift.instUnique 📋 Mathlib.Data.ULift
  {α : Type u} [Unique α] : Unique (ULift.{u_1, u} α)
• ULift.down_bijective 📋 Mathlib.Data.ULift
  {α : Type u} : Function.Bijective ULift.down
• ULift.down_surjective 📋 Mathlib.Data.ULift
  {α : Type u} : Function.Surjective ULift.down
• ULift.up_bijective 📋 Mathlib.Data.ULift
  {α : Type u} : Function.Bijective ULift.up
• ULift.up_injective 📋 Mathlib.Data.ULift
  {α : Type u} : Function.Injective ULift.up
• ULift.up_surjective 📋 Mathlib.Data.ULift
  {α : Type u} : Function.Surjective ULift.up
• ULift.forall 📋 Mathlib.Data.ULift
  {α : Type u} {p : ULift.{u_1, u} α → Prop} : (∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }
• ULift.up_inj 📋 Mathlib.Data.ULift
  {α : Type u} {x y : α} : { down := x } = { down := y } ↔ x = y
• ULift.ext 📋 Mathlib.Data.ULift
  {α : Type u} (x y : ULift.{u_1, u} α) (h : x.down = y.down) : x = y
• ULift.map_bijective 📋 Mathlib.Data.ULift
  {α : Type u} {β : Type v} {f : α → β} : Function.Bijective (ULift.map f) ↔ Function.Bijective f
• ULift.map_injective 📋 Mathlib.Data.ULift
  {α : Type u} {β : Type v} {f : α → β} : Function.Injective (ULift.map f) ↔ Function.Injective f
• ULift.map_surjective 📋 Mathlib.Data.ULift
  {α : Type u} {β : Type v} {f : α → β} : Function.Surjective (ULift.map f) ↔ Function.Surjective f
• ULift.exists 📋 Mathlib.Data.ULift
  {α : Type u} {p : ULift.{u_1, u} α → Prop} : (∃ x, p x) ↔ ∃ x, p { down := x }
• ULift.ext_iff 📋 Mathlib.Data.ULift
  {α : Type u} {x y : ULift.{u_1, u} α} : x = y ↔ x.down = y.down
• ULift.rec_update 📋 Mathlib.Data.ULift
  {α : Type u} {β : ULift.{u_2, u} α → Type u_1} [DecidableEq α] (f : (a : α) → β { down := a }) (a : α) (x : β { down := a }) : (fun t => ULift.rec (Function.update f a x) t) = Function.update (fun t => ULift.rec f t) { down := a } x
• iInf_ulift 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {ι : Type u_8} [InfSet α] (f : ULift.{u_9, u_8} ι → α) : ⨅ i, f i = ⨅ i, f { down := i }
• iSup_ulift 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {ι : Type u_8} [SupSet α] (f : ULift.{u_9, u_8} ι → α) : ⨆ i, f i = ⨆ i, f { down := i }
• ULift.infSet 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [InfSet α] : InfSet (ULift.{v, u_1} α)
• ULift.instCompleteLattice 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] : CompleteLattice (ULift.{v, u_1} α)
• ULift.supSet 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [SupSet α] : SupSet (ULift.{v, u_1} α)
• ULift.down_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [InfSet α] (s : Set (ULift.{v, u_1} α)) : (sInf s).down = sInf (ULift.up ⁻¹' s)
• ULift.down_sSup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [SupSet α] (s : Set (ULift.{v, u_1} α)) : (sSup s).down = sSup (ULift.up ⁻¹' s)
• ULift.up_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [InfSet α] (s : Set α) : { down := sInf s } = sInf (ULift.down ⁻¹' s)
• ULift.up_sSup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [SupSet α] (s : Set α) : { down := sSup s } = sSup (ULift.down ⁻¹' s)
• ULift.down_iInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → ULift.{v, u_1} α) : (⨅ i, f i).down = ⨅ i, (f i).down
• ULift.down_iSup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → ULift.{v, u_1} α) : (⨆ i, f i).down = ⨆ i, (f i).down
• ULift.up_iInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → α) : { down := ⨅ i, f i } = ⨅ i, { down := f i }
• ULift.up_iSup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → α) : { down := ⨆ i, f i } = ⨆ i, { down := f i }
• instFiniteULift 📋 Mathlib.Data.Finite.Defs
  {α : Type v} [Finite α] : Finite (ULift.{u, v} α)
• instInfiniteULift 📋 Mathlib.Data.Finite.Defs
  {α : Type v} [Infinite α] : Infinite (ULift.{u, v} α)
• ULift.fintype 📋 Mathlib.Data.Fintype.Basic
  (α : Type u_4) [Fintype α] : Fintype (ULift.{u_5, u_4} α)
• Fintype.card_ulift 📋 Mathlib.Data.Fintype.Card
  (α : Type u_4) [Fintype α] : Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α
• instCountableULift 📋 Mathlib.Data.Countable.Defs
  {β : Type v} [Countable β] : Countable (ULift.{u, v} β)
• instUncountableULift 📋 Mathlib.Data.Countable.Defs
  {β : Type v} [Uncountable β] : Uncountable (ULift.{u, v} β)
• ULift.encodable 📋 Mathlib.Logic.Encodable.Basic
  {α : Type u_1} [Encodable α] : Encodable (ULift.{u_3, u_1} α)
• Denumerable.ulift 📋 Mathlib.Logic.Denumerable
  {α : Type u_1} [Denumerable α] : Denumerable (ULift.{u_3, u_1} α)
• ULift.add 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [Add α] : Add (ULift.{u_1, u} α)
• ULift.addCancelCommMonoid 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [AddCancelCommMonoid α] : AddCancelCommMonoid (ULift.{u_1, u} α)
• ULift.addCancelMonoid 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [AddCancelMonoid α] : AddCancelMonoid (ULift.{u_1, u} α)
• ULift.addCommGroup 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [AddCommGroup α] : AddCommGroup (ULift.{u_1, u} α)
• ULift.addCommMonoid 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [AddCommMonoid α] : AddCommMonoid (ULift.{u_1, u} α)
• ULift.addCommSemigroup 📋 Mathlib.Algebra.Group.ULift
  {α : Type u} [AddCommSemigroup α] : AddCommSemigroup (ULift.{u_1, u} α)

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 74bdd8d