mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, and `HasColimit (K ⋙ F)`, to show that `F` creates the colimit for `K`
it suffices to show that the chosen colimit point is in the essential image of `F`.
 -/
CategoryTheory.createsColimitOfFullyFaithfulOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    [inst_5 : CategoryTheory.Limits.HasColimit (K.comp F)] →
                      (X : C) → (F.obj X ≅ CategoryTheory.Limits.colimit (K.comp F)) → CategoryTheory.CreatesColimit K F
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
AlgEquiv.coe_mapIntegralClosure : ∀ {R : Type u_1} {A : Type u_2} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : A ≃ₐ[R] S) (x : ↥(integralClosure R A)),
  ↑(f.mapIntegralClosure x) = f ↑x
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : Y ⟶ A ⟹ X),
  ((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm f = CategoryTheory.MonoidalClosed.uncurry f
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.of_lt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ t o₂ → Ordnode.nil.Bounded o₁ ↑x → Ordnode.All (fun x_1 => x_1 < x) t → Ordnode.Valid' o₁ t ↑x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.induction : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i),
  p 0 → (∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p ((fun₀ | i => b) + f)) → p f
-- Init.Omega.Constraint
/-- An optional lower bound on a integer.  -/
Lean.Omega.LowerBound : Type
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_counit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I) (X : E) {Z : E} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((adj₁.comp adj₂).counit.app X) h =
    CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X)))
      (CategoryTheory.CategoryStruct.comp (adj₂.counit.app X) h)
-- Lean.Expr
Lean.Expr.isRawNatLit : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : Cᴹᵒᵖ} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f.unmop
-- Init.Data.Array.Find
Array.findIdx?_isNone : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_mul_pred_self : ∀ (n : ℕ), Even (n * (n - 1))
-- Init.Data.List.Basic
List.range_zero : List.range 0 = []
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {decls : Array (Std.Sat.AIG.Decl α)} →
        {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} →
          {a : ℕ} → {a_1 : Std.HashMap α ℕ} → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_induction : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {p : (x : M) → x ∈ s.saturation → Prop},
  (∀ (x : M) (hx : x ∈ s), p x ⋯) →
    (∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x + y) ⋯) →
      (∀ (x y : M) (hxy : x + y ∈ s.saturation), p (x + y) hxy → p x ⋯ ∧ p y ⋯) →
        ∀ {x : M} (hx : x ∈ s.saturation), p x hx
-- Mathlib.Topology.Constructible
IsCompact.isConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X] {U : Set X} [QuasiSeparatedSpace X],
  IsCompact U → IsOpen U → Topology.IsConstructible U
-- Mathlib.Order.WithBotTop
WithBotTop.coe_ne_top : ∀ {ι : Type u_1} (a : ι), WithBotTop.coe a ≠ ⊤
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivWithinAt_abs_pos : ∀ (s : Set ℝ) {x : ℝ}, 0 < x → HasDerivWithinAt (fun x => |x|) 1 s x
-- Mathlib.Data.ENat.Basic
ENat.addLECancellable_of_ne_top : ∀ {a : ℕ∞}, a ≠ ⊤ → AddLECancellable a
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitMono.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
  Nonempty (CategoryTheory.SplitMono f) → CategoryTheory.IsSplitMono f
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_le_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α}
  [inst_2 : DecidablePred fun x => x ≤ a], a < b → Multiset.filter (fun x => x ≤ a) (Multiset.Ico a b) = {a}
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.mk.injEq : ∀ {K : Type u_1} (b : ℤ) (fr : K) (b_1 : ℤ) (fr_1 : K),
  ({ b := b, fr := fr } = { b := b_1, fr := fr_1 }) = (b = b_1 ∧ fr = fr_1)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.aut_mul : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R]
  (a b : R ≃⋆ₐ[S] R), a * b = b.trans a
-- Mathlib.Algebra.Group.Defs
SubtractionCommMonoid.toAddCommMonoid : {G : Type u} → [self : SubtractionCommMonoid G] → AddCommMonoid G
-- Lean.Meta.Match.MatcherInfo
/-- Number of discriminants  -/
Lean.Meta.Match.MatcherInfo.numDiscrs : Lean.Meta.MatcherInfo → ℕ
-- Init.Control.Lawful.Instances
EStateM.run_pure : ∀ {α σ ε : Type u_1} (a : α) (s : σ), (pure a).run s = EStateM.Result.ok a s
-- Mathlib.Lean.Expr.Basic
Lean.Expr.getRevArg? : Lean.Expr → ℕ → Option Lean.Expr
-- Init.Data.Nat.Lemmas
Nat.anyLTTR_eq_true : ∀ {n : ℕ} {f : (i : ℕ) → i < n → Bool}, n.anyLTTR f = true ↔ ∃ i, ∃ (h : i < n), f i h = true
-- Mathlib.Analysis.Distribution.Distribution
/-- `𝓓'^{n}(Ω, F) = Distribution Ω F n` is the space of `F`-valued distributions on `Ω` with
order at most `n`.

In most cases you want to use the space `𝓓'(Ω, F) = Distribution Ω F ⊤`.  -/
Distribution : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      TopologicalSpace.Opens E →
        (F : Type u_2) → [inst : AddCommGroup F] → [Module ℝ F] → [TopologicalSpace F] → ℕ∞ → Type (max u_1 u_2)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The instance `Algebra R R[M]` whenever we have `Algebra R R`.

In particular this provides the instance `Algebra R R[M]`.  -/
AddMonoidAlgebra.algebra : {R : Type u_1} →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [Algebra R A] → [inst_3 : AddMonoid M] → Algebra R (AddMonoidAlgebra A M)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumcenter lies in the affine span.  -/
Affine.Simplex.circumcenter_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n), s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isShortNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3], W.b₆ = W.a₆
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instLattice : {α : Type u_1} → [Lattice α] → Lattice (WithZero α)
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.card_subset_divisors_le_length_of_chain : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M},
  (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → ∀ {m : Finset (Associates M)}, (∀ r ∈ m, r ≤ q) → m.card ≤ n + 1
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup_k_cons : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s).eraseDup_k =
    Lean.Grind.AC.Seq.rec
      (fun y => Bool.rec (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)) (Lean.Grind.AC.Seq.var x) (Nat.beq x y))
      (fun y s' x_1 =>
        Bool.rec (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s')) (Lean.Grind.AC.Seq.cons y s') (Nat.beq x y))
      s.eraseDup_k
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).unop
      (CategoryTheory.Limits.colimitUnopIsoOpLimit F).inv =
    CategoryTheory.Limits.colimit.ι F.unop (Opposite.unop j)
-- Batteries.Data.List.Lemmas
List.next?_cons : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).next? = some (a, l)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {u v : CategoryTheory.OverPresheafAux.OverArrows η s}, u = v ↔ u.val = v.val
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.coe_center : ∀ (G : Type u_1) [inst : AddGroup G], ↑(AddSubgroup.center G) = Set.addCenter G
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i j k : C}
  {α : g ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj f h} {η : h ⟶ i}
  {ηs : CategoryTheory.MonoidalCategoryStruct.tensorObj f i ⟶ j}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj h k ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i k}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj h k) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj i k)}
  {ηs₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f i) k ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj j k}
  {ηs₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj i k) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj j k}
  {η₃ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj h k) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj j k}
  {η₄ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f h) k ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj j k}
  {η₅ : CategoryTheory.MonoidalCategoryStruct.tensorObj g k ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj j k},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl h).hom
          (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl i).hom))
        k =
      η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η₁ = η₂ →
      CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs k = ηs₁ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f i k).inv ηs₁ = ηs₂ →
          CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃ →
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f h k).hom η₃ = η₄ →
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α k).hom η₄ = η₅ →
                CategoryTheory.MonoidalCategoryStruct.whiskerRight
                    (CategoryTheory.CategoryStruct.comp α.hom
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) ηs))
                    k =
                  η₅
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.smul_mem_fixedBy_iff_mem_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {g : G},
  g • a ∈ MulAction.fixedBy α g ↔ a ∈ MulAction.fixedBy α g
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.getArity : Lean.InductiveType → Lean.MetaM ℕ
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.OplaxFunctor B' B) {a b c : B'}
  (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid F).mapCompIso f g).inv =
    CategoryTheory.inv (F.mapComp f g)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.var : Int.Internal.Linear.Var → Int.Internal.Linear.Expr
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go : Lean.Level → Lean.Level → Bool
-- Mathlib.GroupTheory.Submonoid.Center
val_unitsCenterToCenterUnits_apply_coe : ∀ (M : Type u_1) [inst : Monoid M] (n : (↥(Submonoid.center M))ˣ), ↑↑((unitsCenterToCenterUnits M) n) = ↑↑n
-- Batteries.Data.List.Basic
List.swapTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (a : Array α) (a_1 : α) (xs : List α) (i : ℕ),
  List.swapTR.go l (a_1 :: xs) 0 i.succ a = a.toListAppend (Function.uncurry List.cons (xs.swapAt i a_1))
-- Mathlib.Data.Complex.Basic
Complex.intCast_im : ∀ (n : ℤ), (↑n).im = 0
-- Mathlib.Algebra.Homology.Homotopy
/-- Every chain map is homotopic to itself.  -/
Homotopy.refl : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → (f : C ⟶ D) → Homotopy f f
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.ext : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} ⦃f g : 𝒜 →+*ᵍ ℬ⦄, (∀ (x : A), f x = g x) → f = g
-- Mathlib.RingTheory.MvPowerSeries.Expand
/-- For any multivariate polynomial `φ`, then `MvPolynomial.expand p φ` and
`MvPowerSeries.expand p hp ↑φ` coincide.  -/
MvPowerSeries.expand_eq_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) {φ : MvPolynomial σ R},
  (MvPowerSeries.expand p hp) ↑φ = ↑((MvPolynomial.expand p) φ)
-- Init.Data.Nat.ToString
Nat.ofDigitChars_nil : ∀ {b init : ℕ}, b.ofDigitChars [] init = init
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.mk : Array (Option Lean.Expr) →
  Array (Option Lean.Level) →
    Array (Lean.Expr × Lean.Expr) →
      Array (Lean.Level × Lean.Level) →
        Array (Lean.Expr × Lean.Expr) → Array ℕ → List Lean.Level → Array Lean.Expr → Lean.Meta.Sym.UnifyM.State✝
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s s_1 : Set X) (e_s : s = s_1) (hs : IsOpen s),
  OpenPartialHomeomorph.ofSet s hs = OpenPartialHomeomorph.ofSet s_1 ⋯
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Let `f : γ → α`, `𝔖 : Set (Set α)`, `𝔗 : Set (Set γ)`, and assume that `∀ T ∈ 𝔗, f '' T ∈ 𝔖`.
Then, the function `(fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)` is uniformly continuous.

Note that one can easily see that assuming `∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S` would work too, but
we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)` where `𝔖'` is the
***noncovering*** bornology generated by `𝔖`.  -/
UniformOnFun.precomp_uniformContinuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} {f : γ → α},
  Set.MapsTo (fun x => f '' x) 𝔗 𝔖 → UniformContinuous fun g => (UniformOnFun.ofFun 𝔗) ((UniformOnFun.toFun 𝔖) g ∘ f)
-- Mathlib.Data.ENat.Lattice
ENat.iInf_eq_top_of_isEmpty : ∀ {ι : Sort u_1} {f : ι → ℕ} [IsEmpty ι], ⨅ i, ↑(f i) = ⊤
-- Mathlib.Order.OrderIsoNat
/-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
partially-ordered type.  -/
monotonicSequenceLimit : {α : Type u_1} → [inst : Preorder α] → (ℕ →o α) → α
-- Mathlib.Algebra.Order.Group.PosPart
le_iff_posPart_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
-- Mathlib.Order.RelClasses
/-- Construct a linear order from an `IsStrictTotalOrder` relation.

See note [reducible non-instances].  -/
linearOrderOfSTO : {α : Type u} → (r : α → α → Prop) → [IsStrictTotalOrder α r] → [DecidableRel r] → LinearOrder α
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.exists_insert_of_not_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α},
  M.Indep I → I ⊆ X → ¬M.IsBasis I X → M.IsBasis J X → ∃ e ∈ J \ I, M.Indep (insert e I)
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.setOfPred_wOppSide_eq_image2`. -/
AffineSubspace.setOf_wOppSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.WOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprHost.repr : Std.Http.Header.Host → ℕ → Std.Format
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  (s.dropEndWhile pat).isEmpty = s.revAll pat
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_congr_set_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) {s t : Set β},
  s = t → ∏' (x : ↑s), f ↑x = ∏' (x : ↑t), f ↑x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.isometry_toContinuousMap : ∀ {α : Type u_1} {R : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : Zero α]
  [inst_3 : MetricSpace R] [inst_4 : Zero R], Isometry ContinuousMapZero.toContinuousMap
-- Aesop.RuleTac.Forward.Basic
/-- Prefix of the `implDetail` hyps added by `forward`.  -/
Aesop.forwardImplDetailHypPrefix : Lean.Name
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEquivOfEqTop_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.PartialEquiv M N} (h_dom : f.dom = ⊤) (h_cod : f.cod = ⊤),
  (FirstOrder.Language.PartialEquiv.toEquivOfEqTop h_dom h_cod).toEmbedding =
    FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h_dom
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0),
  R.extMk f m hm hf =
    R.extEquivCohomologyClass.symm
      (CochainComplex.HomComplex.CohomologyClass.mk
        (CochainComplex.HomComplex.Cocycle.toSingleMk
          (CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso (-↑n) n ⋯).hom f) ⋯ (-↑m) ⋯ ⋯))
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- Make a morphism `⦋n⦌ ⟶ ⦋m⦌` from a monotone map between fin's.
This is useful for constructing morphisms between `⦋n⦌` directly
without identifying `n` with `⦋n⦌.len`.
 -/
SimplexCategory.mkHom : {n m : ℕ} → (Fin (n + 1) →o Fin (m + 1)) → ({ len := n } ⟶ { len := m })
-- Mathlib.FieldTheory.Perfect
powMulEquiv_apply : ∀ (M : Type u_1) (p : ℕ) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (a : M), (powMulEquiv M p) a = a ^ p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.ExtTreeMap.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).get!
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.JointlySurjective.exists_eq : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.Scheme.JointlySurjective K]
  {X : AlgebraicGeometry.Scheme}, ∀ S ∈ K.coverings X, ∀ (x : ↥X), ∃ Y g, S g ∧ x ∈ Set.range ⇑g
-- Mathlib.Geometry.Manifold.Instances.Sphere
sphere_ext_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (u v : ↑(Metric.sphere 0 1)),
  u = v ↔ inner ℝ ↑u ↑v = 1
-- Std.Data.ExtDTreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.ExtDTreeMap.mergeWith : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          ((a : α) → β a → β a → β a) → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
_private.Mathlib.RingTheory.Bialgebra.MonoidAlgebra.0.AddMonoidAlgebra.mapDomainOfBialgHomFun : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] →
          [inst_2 : AddGroup G] → [inst_3 : AddGroup H] → (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) → G → H
-- Mathlib.Algebra.Torsor.Defs
/-- Simplify subtraction for a torsor for an `AddGroup G` over
itself. -/
vsub_eq_sub : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G), g₁ -ᵥ g₂ = g₁ - g₂
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `single` as an additive monoid/group homomorphism  -/
HahnSeries.single.addMonoidHom : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddMonoid R] → Γ → R →+ HahnSeries Γ R
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.range_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α], Set.range TopologicalSpace.NonemptyCompacts.toCompacts = {⊥}ᶜ
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms map zero to zero.  -/
RingHom.map_zero : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 0 = 0