Loogle!

Result

Found 124 declarations mentioning Functor.

• Functor 📋 Init.Prelude
  (f : Type u → Type v) : Type (max (u + 1) v)
• Applicative.toFunctor 📋 Init.Prelude
  {f : Type u → Type v} [self : Applicative f] : Functor f
• ReaderT.instFunctorOfMonad 📋 Init.Prelude
  {ρ : Type u} {m : Type u → Type v} [Monad m] : Functor (ReaderT ρ m)
• Functor.mapConst 📋 Init.Prelude
  {f : Type u → Type v} [self : Functor f] {α β : Type u} : α → f β → f α
• Functor.map 📋 Init.Prelude
  {f : Type u → Type v} [self : Functor f] {α β : Type u} : (α → β) → f α → f β
• Applicative.mk 📋 Init.Prelude
  {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f] [toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f
• Functor.mk 📋 Init.Prelude
  {f : Type u → Type v} (map : {α β : Type u} → (α → β) → f α → f β) (mapConst : {α β : Type u} → α → f β → f α) : Functor f
• notM 📋 Init.Control.Basic
  {m : Type → Type v} [Functor m] (x : m Bool) : m Bool
• Functor.discard 📋 Init.Control.Basic
  {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit.{u + 1}
• Functor.mapRev 📋 Init.Control.Basic
  {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β
• tryFinally 📋 Init.Control.Except
  {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α
• StateT.run' 📋 Init.Control.State
  {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α
• instFunctorOption 📋 Init.Data.Option.Basic
  : Functor Option
• Array.instFunctor 📋 Init.Data.Array.Basic
  : Functor Array
• LawfulFunctor 📋 Init.Control.Lawful.Basic
  (f : Type u → Type v) [Functor f] : Prop
• Functor.map_unit 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} [Functor f] [LawfulFunctor f] {a : f PUnit.{u_1 + 1}} : (fun x => PUnit.unit) <$> a = a
• id_map' 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} {α : Type u_1} [Functor f] [LawfulFunctor f] (x : f α) : (fun a => a) <$> x = x
• LawfulFunctor.id_map 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α : Type u} (x : f α) : id <$> x = x
• map_congr 📋 Init.Control.Lawful.Basic
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] {x : m α} {f g : α → β} (h : ∀ (a : α), f a = g a) : f <$> x = g <$> x
• LawfulFunctor.map_const 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• Functor.map_map 📋 Init.Control.Lawful.Basic
  {f : Type u_1 → Type u_2} {α β γ : Type u_1} [Functor f] [LawfulFunctor f] (m : α → β) (g : β → γ) (x : f α) : g <$> m <$> x = (fun a => g (m a)) <$> x
• LawfulFunctor.comp_map 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} {inst✝ : Functor f} [self : LawfulFunctor f] {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α) : (h ∘ g) <$> x = h <$> g <$> x
• LawfulFunctor.mk 📋 Init.Control.Lawful.Basic
  {f : Type u → Type v} [Functor f] (map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) (id_map : ∀ {α : Type u} (x : f α), id <$> x = x) (comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) : LawfulFunctor f
• map_inj_of_left_inverse 📋 Init.Control.Lawful.Lemmas
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] {f : α → β} (w : ∃ g, ∀ (x : α), g (f x) = x) {x y : m α} : f <$> x = f <$> y ↔ x = y
• map_inj_right_of_nonempty 📋 Init.Control.Lawful.Lemmas
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β} (w : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y
• List.instFunctor 📋 Init.Data.List.Control
  : Functor List
• Std.Iterators.instFunctorPostconditionT 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] : Functor (Std.Iterators.PostconditionT m)
• Std.Iterators.PostconditionT.lift 📋 Init.Data.Iterators.PostconditionMonad
  {α : Type w} {m : Type w → Type w'} [Functor m] (x : m α) : Std.Iterators.PostconditionT m α
• Std.Iterators.PostconditionT.map 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} (f : α → β) (x : Std.Iterators.PostconditionT m α) : Std.Iterators.PostconditionT m β
• Std.Iterators.PostconditionT.property_lift 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α : Type w} {x : m α} : (Std.Iterators.PostconditionT.lift x).Property = fun x => True
• Std.Iterators.PostconditionT.property_map 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} {x : Std.Iterators.PostconditionT m α} {f : α → β} {b : β} : (Std.Iterators.PostconditionT.map f x).Property b ↔ ∃ a, f a = b ∧ x.Property a
• Std.Iterators.PostconditionT.operation_lift 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α : Type w} {x : m α} : (Std.Iterators.PostconditionT.lift x).operation = (fun x_1 => ⟨x_1, ⋯⟩) <$> x
• Std.Iterators.PostconditionT.map.eq_1 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} (f : α → β) (x : Std.Iterators.PostconditionT m α) : Std.Iterators.PostconditionT.map f x = { Property := fun b => ∃ a, f ↑a = b, operation := (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation }
• Std.Iterators.PostconditionT.operation_map 📋 Init.Data.Iterators.PostconditionMonad
  {m : Type w → Type w'} [Functor m] {α β : Type w} {x : Std.Iterators.PostconditionT m α} {f : α → β} : (Std.Iterators.PostconditionT.map f x).operation = (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation
• Std.Iterators.Types.Map 📋 Init.Data.Iterators.Combinators.Monadic.FilterMap
  (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) [Functor n] (f : β → Std.Iterators.PostconditionT n γ) : Type w
• Std.Iterators.Types.Map.eq_1 📋 Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
  (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) [Functor n] (f : β → Std.Iterators.PostconditionT n γ) : Std.Iterators.Types.Map α m n lift f = Std.Iterators.Types.FilterMap α m n lift fun b => Std.Iterators.PostconditionT.map some (f b)
• Std.Iterators.instFunctorHetT 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] : Functor (Std.Iterators.HetT m)
• Std.Iterators.HetT.map 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (f : α → β) (x : Std.Iterators.HetT m α) : Std.Iterators.HetT m β
• Std.Iterators.HetT.pmap 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α) (f : (a : α) → x.Property a → β) : Std.Iterators.HetT m β
• Std.Iterators.HetT.map.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (f : α → β) (x : Std.Iterators.HetT m α) : Std.Iterators.HetT.map f x = x.pmap fun a x => f a
• Std.Iterators.HetT.property_map 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} {x : Std.Iterators.HetT m α} {f : α → β} {b : β} : (Std.Iterators.HetT.map f x).Property b ↔ ∃ a, f a = b ∧ x.Property a
• Std.Iterators.HetT.pmap.eq_1 📋 Std.Data.Iterators.Lemmas.Equivalence.HetT
  {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α) (f : (a : α) → x.Property a → β) : x.pmap f = { Property := fun b => ∃ a, ∃ (h : x.Property a), f a h = b, small := ⋯, operation := (fun a => Std.Internal.USquash.deflate ⟨f ↑a.inflate ⋯, ⋯⟩) <$> x.operation }
• Std.Internal.IO.Async.BaseAsync.instFunctor 📋 Std.Internal.Async.Basic
  : Functor Std.Internal.IO.Async.BaseAsync
• Std.Internal.IO.Async.MaybeTask.instFunctor 📋 Std.Internal.Async.Basic
  : Functor Std.Internal.IO.Async.MaybeTask
• Std.Internal.IO.Async.EAsync.instFunctor 📋 Std.Internal.Async.Basic
  {ε : Type} : Functor (Std.Internal.IO.Async.EAsync ε)
• Std.Internal.IO.Async.ETask.instFunctor 📋 Std.Internal.Async.Basic
  {ε : Type} : Functor (Std.Internal.IO.Async.ETask ε)
• Std.Internal.IO.Async.instMonadAsyncStateTOfMonadOfFunctor 📋 Std.Internal.Async.Basic
  {m t : Type → Type} {s : Type} [Monad m] [Functor t] [inst : Std.Internal.IO.Async.MonadAsync t m] : Std.Internal.IO.Async.MonadAsync t (StateT s m)
• Std.Internal.IO.Async.ContextAsync.instFunctor 📋 Std.Internal.Async.ContextAsync
  : Functor Std.Internal.IO.Async.ContextAsync
• MonadSatisfying 📋 Batteries.Classes.SatisfiesM
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] : Type (max (u + 1) v)
• SatisfiesM 📋 Batteries.Classes.SatisfiesM
  {α : Type u} {m : Type u → Type v} [Functor m] (p : α → Prop) (x : m α) : Prop
• SatisfiesM.trivial 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} [Functor m] [LawfulFunctor m] {x : m α} : SatisfiesM (fun x => True) x
• SatisfiesM.of_true 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} [Functor m] [LawfulFunctor m] {x : m α} (h : ∀ (a : α), p a) : SatisfiesM p x
• MonadSatisfying.satisfying 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} {inst✝ : Functor m} {inst✝¹ : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x) : m { a // p a }
• SatisfiesM.imp 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p q : α → Prop} [Functor m] [LawfulFunctor m] {x : m α} (h : SatisfiesM p x) (H : ∀ {a : α}, p a → q a) : SatisfiesM q x
• SatisfiesM.map_pre 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α α✝ : Type u_1} {p : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM (fun a => p (f a)) x) : SatisfiesM p (f <$> x)
• SatisfiesM.mapConst 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {q : α → Prop} {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM q x) (ha : ∀ {b : α}, q b → p a) : SatisfiesM p (Functor.mapConst a x)
• SatisfiesM.map 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α✝ : Type u_1} {q : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) (hf : ∀ {a : α}, p a → q (f a)) : SatisfiesM q (f <$> x)
• SatisfiesM.map_post 📋 Batteries.Classes.SatisfiesM
  {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α✝ : Type u_1} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) : SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <$> x)
• MonadSatisfying.val_eq 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} {inst✝ : Functor m} {inst✝¹ : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x) : Subtype.val <$> satisfying h = x
• MonadSatisfying.mk 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} [Functor m] [LawfulFunctor m] (satisfying : {α : Type u} → {p : α → Prop} → {x : m α} → SatisfiesM p x → m { a // p a }) (val_eq : ∀ {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x), Subtype.val <$> satisfying h = x) : MonadSatisfying m
• MonadSatisfying.satisfying.congr_simp 📋 Batteries.Classes.SatisfiesM
  {m : Type u → Type v} {inst✝ : Functor m} {inst✝¹ : LawfulFunctor m} [self : MonadSatisfying m] {α : Type u} {p : α → Prop} {x x✝ : m α} (e_x : x = x✝) (h : SatisfiesM p x) : satisfying h = satisfying ⋯
• LawfulFunctor.map_inj_right_of_nonempty 📋 Batteries.Control.Monad
  {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β} (w : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y
• Lean.Expr.modifyAppArgM 📋 Mathlib.Lean.Expr.Basic
  {M : Type → Type u} [Functor M] [Pure M] (modifier : Lean.Expr → M Lean.Expr) : Lean.Expr → M Lean.Expr
• Set.instFunctor 📋 Mathlib.Data.Set.Defs
  : Functor Set
• EquivFunctor.ofLawfulFunctor 📋 Mathlib.Control.EquivFunctor
  (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : EquivFunctor f
• EquivFunctor.ofLawfulFunctor.congr_simp 📋 Mathlib.Control.EquivFunctor
  (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : EquivFunctor.ofLawfulFunctor f = EquivFunctor.ofLawfulFunctor f
• Functor.AddConst.functor 📋 Mathlib.Control.Functor
  {γ : Type u_1} : Functor (Functor.AddConst γ)
• Functor.Const.functor 📋 Mathlib.Control.Functor
  {γ : Type u_1} : Functor (Functor.Const γ)
• Functor.supp 📋 Mathlib.Control.Functor
  {F : Type u → Type v} [Functor F] {α : Type u} (x : F α) : Set α
• Functor.Liftp 📋 Mathlib.Control.Functor
  {F : Type u → Type v} [Functor F] {α : Type u} (p : α → Prop) (x : F α) : Prop
• Functor.mapConstRev 📋 Mathlib.Control.Functor
  {f : Type u → Type v} [Functor f] {α β : Type u} : f β → α → f α
• Functor.Comp.functor 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] : Functor (Functor.Comp F G)
• Functor.Liftr 📋 Mathlib.Control.Functor
  {F : Type u → Type v} [Functor F] {α : Type u} (r : α → α → Prop) (x y : F α) : Prop
• Functor.Comp.map 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) : Functor.Comp F G α → Functor.Comp F G β
• Functor.Comp.functor_comp_id 📋 Mathlib.Control.Functor
  {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] : Functor.Comp.functor = AF
• Functor.Comp.functor_id_comp 📋 Mathlib.Control.Functor
  {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F] : Functor.Comp.functor = AF
• Functor.Comp.lawfulFunctor 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] : LawfulFunctor (Functor.Comp F G)
• Functor.map_id 📋 Mathlib.Control.Functor
  {F : Type u → Type v} {α : Type u} [Functor F] [LawfulFunctor F] : (fun x => id <$> x) = id
• Functor.of_mem_supp 📋 Mathlib.Control.Functor
  {F : Type u → Type v} [Functor F] {α : Type u} {x : F α} {p : α → Prop} (h : Functor.Liftp p x) (y : α) : y ∈ Functor.supp x → p y
• Functor.Comp.id_map 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] {α : Type v} (x : Functor.Comp F G α) : Functor.Comp.map id x = x
• Functor.ext 📋 Mathlib.Control.Functor
  {F : Type u_1 → Type u_2} {F1 F2 : Functor F} [LawfulFunctor F] [LawfulFunctor F] : (∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x) → F1 = F2
• Functor.Comp.map.eq_1 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x✝ : Functor.Comp F G α) : Functor.Comp.map h x✝ = Functor.Comp.mk ((fun x => h <$> x) <$> x✝)
• Functor.map_comp_map 📋 Mathlib.Control.Functor
  {F : Type u → Type v} {α β γ : Type u} [Functor F] [LawfulFunctor F] (f : α → β) (g : β → γ) : ((fun x => g <$> x) ∘ fun x => f <$> x) = fun x => (g ∘ f) <$> x
• Functor.Comp.map_mk 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : F (G α)) : h <$> Functor.Comp.mk x = Functor.Comp.mk ((fun x => h <$> x) <$> x)
• Functor.Comp.run_map 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] {α β : Type v} (h : α → β) (x : Functor.Comp F G α) : (h <$> x).run = (fun x => h <$> x) <$> x.run
• Functor.Comp.comp_map 📋 Mathlib.Control.Functor
  {F : Type u → Type w} {G : Type v → Type u} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] {α β γ : Type v} (g' : α → β) (h : β → γ) (x : Functor.Comp F G α) : Functor.Comp.map (h ∘ g') x = Functor.Comp.map h (Functor.Comp.map g' x)
• Traversable.toFunctor 📋 Mathlib.Control.Traversable.Basic
  {t : Type u → Type u} [self : Traversable t] : Functor t
• Traversable.mk 📋 Mathlib.Control.Traversable.Basic
  {t : Type u → Type u} [toFunctor : Functor t] (traverse : {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t α → m (t β)) : Traversable t
• StateT.eval 📋 Mathlib.Control.Monad.Basic
  {α σ : Type u} {m : Type u → Type v} [Functor m] (cmd : StateT σ m α) (s : σ) : m α
• Filter.instFunctor 📋 Mathlib.Order.Filter.Defs
  : Functor Filter
• Ultrafilter.functor 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : Functor Ultrafilter
• CategoryTheory.ofTypeFunctor 📋 Mathlib.CategoryTheory.Types.Basic
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] : CategoryTheory.Functor (Type u) (Type v)
• CategoryTheory.ofTypeFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] : (CategoryTheory.ofTypeFunctor m).obj = m
• CategoryTheory.ofTypeFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
  (m : Type u → Type v) [Functor m] [LawfulFunctor m] {α β : Type u} (f : α → β) : (CategoryTheory.ofTypeFunctor m).map f = Functor.map f
• Bifunctor.functor 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] {α : Type u₀} : Functor (F α)
• Function.bicompr.bifunctor 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] : Bifunctor (Function.bicompr G F)
• Function.bicompl.bifunctor 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u_1 → Type u₀) (H : Type u_2 → Type u₁) [Functor G] [Functor H] : Bifunctor (Function.bicompl F G H)
• Function.bicompr.lawfulBifunctor 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u₂ → Type u_1) [Functor G] [LawfulFunctor G] [LawfulBifunctor F] : LawfulBifunctor (Function.bicompr G F)
• Function.bicompl.lawfulBifunctor 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] (G : Type u_1 → Type u₀) (H : Type u_2 → Type u₁) [Functor G] [Functor H] [LawfulFunctor G] [LawfulFunctor H] [LawfulBifunctor F] : LawfulBifunctor (Function.bicompl F G H)
• Functor.mapEquiv 📋 Mathlib.Logic.Equiv.Functor
  {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) : f α ≃ f β
• Functor.mapEquiv_refl 📋 Mathlib.Logic.Equiv.Functor
  {α : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] : Functor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
• Functor.mapEquiv.congr_simp 📋 Mathlib.Logic.Equiv.Functor
  {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h h✝ : α ≃ β) (e_h : h = h✝) : Functor.mapEquiv f h = Functor.mapEquiv f h✝
• Functor.mapEquiv_apply 📋 Mathlib.Logic.Equiv.Functor
  {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) (x : f α) : (Functor.mapEquiv f h) x = ⇑h <$> x
• Functor.mapEquiv_symm_apply 📋 Mathlib.Logic.Equiv.Functor
  {α β : Type u} (f : Type u → Type v) [Functor f] [LawfulFunctor f] (h : α ≃ β) (y : f β) : (Functor.mapEquiv f h).symm y = ⇑h.symm <$> y
• Stream'.Seq.instFunctor 📋 Mathlib.Data.Seq.Basic
  : Functor Stream'.Seq
• MeasureTheory.OuterMeasure.instFunctor 📋 Mathlib.MeasureTheory.OuterMeasure.Operations
  : Functor MeasureTheory.OuterMeasure
• ULiftable.refl 📋 Mathlib.Control.ULiftable
  (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : ULiftable f f
• ULiftable.downMap 📋 Mathlib.Control.ULiftable
  {F : Type (max u₀ v₀) → Type u₁} {G : Type u₀ → Type v₁} [ULiftable G F] [Functor F] {α : Type (max u₀ v₀)} {β : Type u₀} (f : α → β) (x : F α) : G β
• ULiftable.upMap 📋 Mathlib.Control.ULiftable
  {F : Type u₀ → Type u₁} {G : Type (max u₀ v₀) → Type v₁} [ULiftable F G] [Functor G] {α : Type u₀} {β : Type (max u₀ v₀)} (f : α → β) (x : F α) : G β
• Equiv.functor 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] : Functor t'
• Equiv.map 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] {α β : Type u} (f : α → β) (x : t' α) : t' β
• Equiv.lawfulFunctor 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [LawfulFunctor t] : LawfulFunctor t'
• Equiv.id_map 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [LawfulFunctor t] {α : Type u} (x : t' α) : Equiv.map eqv id x = x
• Equiv.comp_map 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [LawfulFunctor t] {α β γ : Type u} (g : α → β) (h : β → γ) (x : t' α) : Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)
• Equiv.lawfulFunctor' 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] [LawfulFunctor t] [F : Functor t'] (h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f) (h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f) : LawfulFunctor t'
• Equiv.map.eq_1 📋 Mathlib.Control.Traversable.Equiv
  {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [Functor t] {α β : Type u} (f : α → β) (x : t' α) : Equiv.map eqv f x = (eqv β) (f <$> (eqv α).symm x)
• Multiset.functor 📋 Mathlib.Data.Multiset.Functor
  : Functor Multiset
• Finset.functor 📋 Mathlib.Data.Finset.Functor
  [(P : Prop) → Decidable P] : Functor Finset
• PFunctor.instFunctorObj 📋 Mathlib.Data.PFunctor.Univariate.Basic
  (P : PFunctor.{uA, uB}) : Functor ↑P
• Functor.supp.eq_1 📋 Mathlib.Data.PFunctor.Univariate.Basic
  {F : Type u → Type v} [Functor F] {α : Type u} (x : F α) : Functor.supp x = {y | ∀ ⦃p : α → Prop⦄, Functor.Liftp p x → p y}
• QPF.toFunctor 📋 Mathlib.Data.QPF.Univariate.Basic
  {F : Type u → Type v} [self : QPF F] : Functor F
• QPF.mk 📋 Mathlib.Data.QPF.Univariate.Basic
  {F : Type u → Type v} [toFunctor : Functor F] (P : PFunctor.{u, u'}) (abs : {α : Type u} → ↑P α → F α) (repr : {α : Type u} → F α → ↑P α) (abs_repr : ∀ {α : Type u} (x : F α), abs (repr x) = x) (abs_map : ∀ {α β : Type u} (f : α → β) (p : ↑P α), abs (P.map f p) = f <$> abs p) : QPF F
• QPF.quotientQPF 📋 Mathlib.Data.QPF.Univariate.Basic
  {F : Type u → Type u} [q : QPF F] {G : Type u → Type u} [Functor G] {FG_abs : {α : Type u} → F α → G α} {FG_repr : {α : Type u} → G α → F α} (FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x) : QPF G
• WittVector.instFunctor 📋 Mathlib.RingTheory.WittVector.Defs
  (p : ℕ) : Functor (WittVector p)

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 79343e3 serving mathlib revision 706fd95