mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  (fiber : CategoryTheory.Functor C (Type w))
  (isCofiltered :
    autoParam (CategoryTheory.IsCofiltered fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam)
  (initiallySmall :
    autoParam (CategoryTheory.InitiallySmall fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam)
  (jointly_surjective :
    ∀ {X : C},
      ∀ R ∈ J X,
        ∀ (x : fiber.obj X), ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber.map f)) y = x)
  (fiber_1 : CategoryTheory.Functor C (Type w))
  (isCofiltered_1 :
    autoParam (CategoryTheory.IsCofiltered fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam)
  (initiallySmall_1 :
    autoParam (CategoryTheory.InitiallySmall fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam)
  (jointly_surjective_1 :
    ∀ {X : C},
      ∀ R ∈ J X,
        ∀ (x : fiber_1.obj X),
          ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber_1.map f)) y = x),
  ({ fiber := fiber, isCofiltered := isCofiltered, initiallySmall := initiallySmall,
        jointly_surjective := jointly_surjective } =
      { fiber := fiber_1, isCofiltered := isCofiltered_1, initiallySmall := initiallySmall_1,
        jointly_surjective := jointly_surjective_1 }) =
    (fiber = fiber_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Whisker a bicone with an equivalence between the indexing types.  -/
CategoryTheory.Limits.Bicone.whisker : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {K : Type w'} →
          {f : J → C} → CategoryTheory.Limits.Bicone f → (g : K ≃ J) → CategoryTheory.Limits.Bicone (f ∘ ⇑g)
-- Init.Data.List.Lemmas
List.partition_eq_filter_filter : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.partition p l = (List.filter p l, List.filter (not ∘ p) l)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.map_adj : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v w : V},
  G.Adj v w → G'.Adj (f v) (f w)
-- Mathlib.Order.OrderDual
/-- Transfer `Top` across an `Equiv`.  -/
Equiv.top : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Top β] → Top α
-- Mathlib.Algebra.Group.Prod
Prod.mk_one_mul_mk_one : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : MulOneClass N] (a₁ a₂ : M), (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
-- Mathlib.Computability.Primrec.Basic
Primcodable.bool : Primcodable Bool
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
LaurentPolynomial.counit_T : ∀ {R : Type u_11} [inst : CommSemiring R] {A : Type u_12} [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (n : ℤ),
  CoalgebraStruct.counit (LaurentPolynomial.T n) = 1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.continuous_integral_boundedContinuousFunction : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X ℝ), Continuous fun μ => ∫ (x : X), f x ∂↑μ
-- Mathlib.GroupTheory.Goursat
AddSubgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)},
  Function.Surjective (Prod.fst ∘ ⇑I.subtype) →
    Function.Surjective (Prod.snd ∘ ⇑I.subtype) → ∀ {x y : G × H}, x ∈ I → y ∈ I → (↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_symm_apply_fst : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A] (x : A × A),
  (Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
-- Mathlib.Tactic.NormNum.LegendreSymbol
_private.Mathlib.Tactic.NormNum.LegendreSymbol.0.Mathlib.Meta.NormNum.mkRawIntLit' : ℤ → Q(ℤ)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.heq_measurableSpace_Iic_pi : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)] {a b : ℕ}, a = b → inferInstance ≍ inferInstance
-- Init.Data.UInt.Lemmas
USize.toUInt32_add : ∀ (a b : USize), (a + b).toUInt32 = a.toUInt32 + b.toUInt32
-- Lean.Meta.GeneralizeTelescope
/-- Given expressions `es := #[e_1, e_2, ..., e_n]`, execute `k` with the
free variables `(x_1 : A_1) (x_2 : A_2 [x_1]) ... (x_n : A_n [x_1, ... x_{n-1}])`.
Moreover,
- type of `e_1` is definitionally equal to `A_1`,
- type of `e_2` is definitionally equal to `A_2[e_1]`.
- ...
- type of `e_n` is definitionally equal to `A_n[e_1, ..., e_{n-1}]`.

This method tries to avoid the creation of new free variables. For example, if `e_i` is a
free variable `x_i` and it is not a let-declaration variable, and its type does not depend on
previous `e_j`s, the method will just use `x_i`.

The telescope `x_1 ... x_n` can be used to create lambda and forall abstractions.
Moreover, for any type correct lambda abstraction `f` constructed using `mkForall #[x_1, ..., x_n] ...`,
The application `f e_1 ... e_n` is also type correct.

The `kabstract` method is used to "locate" and abstract forward dependencies.
That is, an occurrence of `e_i` in the of `e_j` for `j > i`.

The method checks whether the abstract types `A_i` are type correct. Here is an example
where `generalizeTelescope` fails to create the telescope `x_1 ... x_n`.
Assume the local context contains `(n : Nat := 10) (xs : Vec Nat n) (ys : Vec Nat 10) (h : xs = ys)`.
Then, assume we invoke `generalizeTelescope` with `es := #[10, xs, ys, h]`
A type error is detected when processing `h`'s type. At this point, the method had successfully produced
```
  (x_1 : Nat) (xs : Vec Nat n) (x_2 : Vec Nat x_1)
```
and the type for the new variable abstracting `h` is `xs = x_2` which is not type correct.  -/
Lean.Meta.generalizeTelescope : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Topology.DiscreteSubset
Topology.IsEmbedding.image_mem_codiscreteWithin_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → ∀ {s : Set X}, f '' s ∈ Filter.codiscreteWithin (Set.range f) ↔ s ∈ Filter.codiscrete X
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Construct an element of the additive monoid algebra `R[M]`
from its coefficients `M →₀ R`.  -/
AddMonoidAlgebra.ofCoeff : {R : Type u_8} → {M : Type u_9} → [inst : Semiring R] → (M →₀ R) → AddMonoidAlgebra R M
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a...b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a`, the statement holds for the empty range `a...b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, if the
statement holds for `a...b`, it also holds for the larger range `a...(b + 1)`.

The following is an example reproving `length_toList_rco`.

```
example (a b : Nat) : (a...b).toList.length = b - a := by
  induction a, b using Nat.induct_rco_right
  case base =>
    simp only [Nat.toList_rco_eq_nil, List.length_nil, Nat.sub_eq_zero_of_le, *]
  case step a b hle ih =>
    rw [Nat.toList_rco_eq_append (by omega),
      List.length_append, List.length_singleton, Nat.add_sub_cancel, ih]
    omega
``` -/
Nat.induct_rco_right : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a → motive a b) → (∀ (a b : ℕ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℕ), motive a b
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instFunLike_1 : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → FunLike (A →ₛₙₐ[φ] B) A B
-- Mathlib.Data.Fintype.Perm
MulEquiv.instFintype.eq_1 : ∀ {α : Type u_4} {β : Type u_5} [inst : Mul α] [inst_1 : Mul β] [inst_2 : DecidableEq α] [inst_3 : DecidableEq β]
  [inst_4 : Fintype α] [inst_5 : Fintype β],
  MulEquiv.instFintype =
    {
      elems :=
        Finset.filterMap
          (fun e => if h : ∀ (a b : α), e (a * b) = e a * e b then some { toEquiv := e, map_mul' := h } else none)
          Fintype.elems ⋯,
      complete := ⋯ }
-- Init.Data.BEq
BEq.congr_left : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b c : α}, (a == b) = true → (a == c) = (b == c)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.decidable : {σ : Type u_1} →
  {m : MonomialOrder σ} →
    {R : Type u_2} → [inst : CommSemiring R] → [DecidableEq R] → (f : MvPolynomial σ R) → Decidable (m.Monic f)
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.withNewLocals : {α : Type} → Array Lean.Name → Lean.Elab.Term.Quotation.PrecheckM α → Lean.Elab.Term.Quotation.PrecheckM α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_int_mul_pi_sub : ∀ (x : ℂ) (n : ℤ), Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x
-- Mathlib.Data.Set.Prod
Set.EqOn.right_of_eqOn_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ},
  Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t) → s.Nonempty → Set.EqOn g g' t
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMulActionOreLocalization : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → MulAction (OreLocalization S R) (OreLocalization S X)
-- Mathlib.Algebra.Order.Monovary
antivary_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f⁻¹ g ↔ Monovary f g
-- Mathlib.Probability.UniformOn
/-- Given a set `s`, `uniformOn s` is the uniform measure on `s`, defined as the counting measure
conditioned by `s`. One should think of `uniformOn s t` as the proportion of `s` that is contained
in `t`.

This is a probability measure when `s` is finite and nonempty and is given by
`ProbabilityTheory.uniformOn_isProbabilityMeasure`.  -/
ProbabilityTheory.uniformOn : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Set Ω → MeasureTheory.Measure Ω
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mk : {R : Type u} →
  [toCommRing : CommRing R] →
    [toNontrivial : Nontrivial R] →
      (quotient : R → R → R) →
        (∀ (a : R), quotient a 0 = 0) →
          (remainder : R → R → R) →
            (∀ (a b : R), b * quotient a b + remainder a b = a) →
              (r : R → R → Prop) →
                WellFounded r →
                  (∀ (a : R) {b : R}, b ≠ 0 → r (remainder a b) b) →
                    (∀ (a : R) {b : R}, b ≠ 0 → ¬r (a * b) a) → EuclideanDomain R
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The isomorphism giving rise to the lax functoriality constraint  -/
CategoryTheory.LaxFunctor.PseudoCore.mapCompIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} →
          F.PseudoCore →
            {a b c : B} →
              (f : a ⟶ b) →
                (g : b ⟶ c) →
                  F.map (CategoryTheory.CategoryStruct.comp f g) ≅
                    CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)
-- Init.Data.UInt.Bitwise
UInt8.zero_shiftLeft : ∀ {a : UInt8}, 0 <<< a = 0
-- Mathlib.Order.Category.BoolAlg
/-- The underlying Boolean algebra.  -/
BoolAlg.carrier : BoolAlg → Type u_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))}
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J)),
  ↑↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J) a) = ↑a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskeringEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  CategoryTheory.Limits.Cocone.whiskeringEquivalence e =
    CategoryTheory.Equivalence.mk'' (CategoryTheory.Limits.Cocone.whiskering e.functor)
      ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
        (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv))
      (CategoryTheory.NatIso.ofComponents'
        (fun s =>
          CategoryTheory.Limits.Cocone.extInv
            (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
        ⋯)
      (CategoryTheory.NatIso.ofComponents'
        (fun s =>
          CategoryTheory.Limits.Cocone.extInv
            (CategoryTheory.Iso.refl
              ((((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
                          (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)).comp
                      (CategoryTheory.Limits.Cocone.whiskering e.functor)).obj
                  s).pt)
            ⋯)
        ⋯)
      ⋯
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which monovary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not monovary together. Stated by permuting the entries of `g`.  -/
Monovary.sum_mul_comp_perm_lt_sum_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Monovary f g → (∑ i, f i * g (σ i) < ∑ i, f i * g i ↔ ¬Monovary f (g ∘ ⇑σ))
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sum.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι],
  AdicCompletion.sum I M =
    DirectSum.toModule (AdicCompletion I R) ι (AdicCompletion I (DirectSum ι fun j => M j)) fun j =>
      AdicCompletion.map I (DirectSum.lof R ι M j)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.instStarRingEquivClass : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B], StarRingEquivClass (A ≃⋆ₐ[R] B) A B
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monotone_inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), Monotone fun P => P.inverseImage F
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toListRev_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Option γ},
  (Std.Iter.filterMap f it).toListRev = List.filterMap f it.toListRev
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq_ring_closure : ∀ {R : Type uR} {A : Type uA} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (s : Set A),
  (Algebra.adjoin R s).toSubring = Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)
-- Init.Data.String.Lemmas.Splits
/-- Given a position that splits `s` into `t₁ ++ t₂` and `t₃` with witness `h`, construct a position
`h.rotateLeft` that splits `s` into `t₁` and `t₂ ++ t₃`. Use `h.splits_rotateLeft` for the witness
that `h.rotateLEft` splits `s` as required.
 -/
String.Pos.Splits.rotateLeft : {s : String} → {p : s.Pos} → {t₁ t₂ t₃ : String} → p.Splits (t₁ ++ t₂) t₃ → s.Pos
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.id_apply : ∀ (M : SemiNormedGrp₁) (r : M.carrier), ↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.id M)) r = r
-- Mathlib.Algebra.Module.LinearMap.Defs
DistribMulActionHom.instSemilinearMapClass : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : Semiring S] [inst_5 : Module S M₂] {σ : R →+* S},
  SemilinearMapClass (M →ₑ+[↑σ] M₂) σ M M₂
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.reflectsFiniteCoproductsOfReflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.PreservesFiniteCoproducts F], CategoryTheory.Limits.ReflectsFiniteCoproducts F
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS.mk.injEq : ∀ (ref : Lean.Syntax) (fvarDecls : List Lean.LocalDecl) (patterns : List Lean.Meta.Match.Pattern) (ref_1 : Lean.Syntax)
  (fvarDecls_1 : List Lean.LocalDecl) (patterns_1 : List Lean.Meta.Match.Pattern),
  ({ ref := ref, fvarDecls := fvarDecls, patterns := patterns } =
      { ref := ref_1, fvarDecls := fvarDecls_1, patterns := patterns_1 }) =
    (ref = ref_1 ∧ fvarDecls = fvarDecls_1 ∧ patterns = patterns_1)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) (m₁ : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ D m₁).W =
    D.W ⊔ CategoryTheory.MorphismProperty.ofHoms fun x => CategoryTheory.CategoryStruct.id m₁
-- Mathlib.Algebra.Category.Ring.Limits
CommSemiRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommSemiRingCat
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a bifunctor `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂` to a category `C₂` which has pullbacks, the Leibniz
  pullback (pullback-power) of `f₁ : X₁ ⟶ Y₁` in `C₁` and `f₃ : X₃ ⟶ Y₃` in `C₃` is the map
  `(G.obj (op Y₁)).obj X₃ ⟶ pullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)` induced by
  the diagram
```
  `(G.obj (op Y₁)).obj X₃` ----> `(G.obj (op X₁)).obj X₃`
              |                              |
              |                              |
              v                              v
  `(G.obj (op Y₁)).obj Y₃` ----> `(G.obj (op X₁)).obj Y₃`
```
 -/
CategoryTheory.Functor.leibnizPullback : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂) →
              [CategoryTheory.Limits.HasPullbacks C₂] →
                CategoryTheory.Functor (CategoryTheory.Arrow C₁)ᵒᵖ
                  (CategoryTheory.Functor (CategoryTheory.Arrow C₃) (CategoryTheory.Arrow C₂))
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_add_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt (fun x => f x + c) f' s x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_X : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.X.roots = {0}
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.instNonemptyColimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [P.Nonempty],
  (P.colimitsClosure J).Nonempty
-- Std.Data.HashMap.Raw
/-- Returns a list of all values present in the hash map in some order.  -/
Std.HashMap.Raw.values : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → List β
-- Init.Data.SInt.Bitwise
ISize.toUSize_and : ∀ (a b : ISize), (a &&& b).toUSize = a.toUSize &&& b.toUSize
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.uniformContinuous_snd : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M], UniformContinuous TrivSqZeroExt.snd
-- Mathlib.Data.Finset.Insert
Finset.Nontrivial.exists_ne : ∀ {α : Type u_1} {s : Finset α}, s.Nontrivial → ∀ (a : α), ∃ b ∈ s, b ≠ a
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- The integrals of thickened indicators of a closed set against a finite measure tend to the
measure of the closed set if the thickening radii tend to zero.  -/
MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed : ∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {F : Set Ω},
  IsClosed F →
    ∀ {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n),
      Filter.Tendsto δs Filter.atTop (nhds 0) →
        Filter.Tendsto (fun n => ∫ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (nhds (μ.real F))
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.log_mul_self_monotoneOn : MonotoneOn (fun x => Real.log x * x) {x | 1 ≤ x}
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_def : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  s • t = Finset.image (fun p => p.1 • p.2) (s ×ˢ t)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'_mul : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x y : B) (hx : IsIntegral R x)
  (hy : IsIntegral R y), IsIntegralClosure.mk' A (x * y) ⋯ = IsIntegralClosure.mk' A x hx * IsIntegralClosure.mk' A y hy
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
AEMeasurable.apply_continuousLinearMap : ∀ {α : Type u_1} [inst : MeasurableSpace α] {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [BorelSpace E] {F : Type u_4}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E} {μ : MeasureTheory.Measure α},
  AEMeasurable φ μ → ∀ (v : F), AEMeasurable (fun a => (φ a) v) μ
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opEquivalence_unitIso : CategoryTheory.Cat.opEquivalence.unitIso =
  CategoryTheory.NatIso.ofComponents
    (fun x =>
      { hom := (CategoryTheory.opOp ↑x).toCatHom, inv := (CategoryTheory.unopUnop ↑x).toCatHom, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    @CategoryTheory.Cat.opEquivalence._proof_3
-- Mathlib.Topology.Order
discreteTopology_iff_isOpen_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (a : α), IsOpen {a}
-- Mathlib.RepresentationTheory.Rep.Basic
/-- A morphism in `Rep k G` has an underlying linear map attached to it hence induce a morphism in
`ModuleCat k`.  -/
Rep.Hom.toModuleCatHom : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] →
      [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → (A ⟶ B) → (ModuleCat.of k ↑A ⟶ ModuleCat.of k ↑B)