mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_homothety_self : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.isEmpty_iff_subsingleton : ∀ {R : Type u} [inst : CommSemiring R], IsEmpty (PrimeSpectrum R) ↔ Subsingleton R
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.restrictTopIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  X.restrictTopIso.hom = CategoryTheory.InducedCategory.homMk (X.ofRestrict ⋯)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.nil : ∀ {α : Type u_1} {le : α → α → Bool} {n : ℕ},
  Batteries.BinomialHeap.Imp.Heap.WF le n Batteries.BinomialHeap.Imp.Heap.nil
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.univ_id : Ordinal.univ.{u, u + 1} = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.nonempty_hom_iff_exists_le_comap : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  Nonempty (H →g G) ↔ ∃ f, H ≤ SimpleGraph.comap f G
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mk.injEq : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (carrier : Set M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier) (carrier_1 : Set M)
  (smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ carrier_1 → c • x ∈ carrier_1),
  ({ carrier := carrier, smul_mem' := smul_mem' } = { carrier := carrier_1, smul_mem' := smul_mem'_1 }) =
    (carrier = carrier_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite product of functions antitone on `u` is antitone on `u`.  -/
AntitoneOn.finsetProd' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [MulLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {u : Set γ} {f : ι → γ → N},
  (∀ i ∈ s, AntitoneOn (f i) u) → AntitoneOn (fun x => ∏ i ∈ s, f i x) u
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
/-- The functor `SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)` which maps
`X` to the formal direct factor of `K[X]` defined by `PInfty`.  -/
AlgebraicTopology.DoldKan.N₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- The morphism `mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃` when `f₁ ≫ f₂ = f₁₂`.  -/
CategoryTheory.ComposableArrows.threeδ₁Toδ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {i j k l : C} →
      (f₁ : i ⟶ j) →
        (f₂ : j ⟶ k) →
          (f₃ : k ⟶ l) →
            (f₁₂ : i ⟶ k) →
              autoParam (CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
                  CategoryTheory.ComposableArrows.threeδ₁Toδ₀._auto_1 →
                (CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₂ f₃)
-- Mathlib.NumberTheory.GaussSum
/-- The Gauss sum of a nontrivial character on a finite field does not vanish.  -/
gaussSum_ne_zero_of_nontrivial : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R'],
  ↑(Fintype.card R) ≠ 0 → ∀ {χ : MulChar R R'}, χ ≠ 1 → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_neg_one : Real.arccos (-1) = Real.pi
-- Init.System.ST
EST.Out.error.sizeOf_spec : ∀ {ε σ α : Type} [inst : SizeOf ε] [inst_1 : SizeOf σ] [inst_2 : SizeOf α] (a : ε) (a_1 : Void σ),
  sizeOf (EST.Out.error a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Int.Basic
/-- Converts an integer into a natural number. Negative numbers are converted to `0`.

Examples:
* `(7 : Int).toNat = 7`
* `(0 : Int).toNat = 0`
* `(-7 : Int).toNat = 0`
 -/
Int.toNat : ℤ → ℕ
-- Mathlib.Algebra.Star.Subalgebra
/-- The difference with `StarSubalgebra.adjoin_induction` is that this acts on the subtype.  -/
StarAlgebra.adjoin_induction_subtype : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A}
  {p : ↥(StarAlgebra.adjoin R s) → Prop} (a : ↥(StarAlgebra.adjoin R s)),
  (∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) →
    (∀ (r : R), p ((algebraMap R ↥(StarAlgebra.adjoin R s)) r)) →
      (∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x + y)) →
        (∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x * y)) →
          (∀ (x : ↥(StarAlgebra.adjoin R s)), p x → p (star x)) → p a
-- Mathlib.Data.Set.Card
Set.encard_image_le : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), (f '' s).encard ≤ s.encard
-- Mathlib.Order.OrderDual
OrderDual.ofDual_toDual : ∀ {α : Type u_1} (a : α), OrderDual.ofDual (OrderDual.toDual a) = a
-- Mathlib.Algebra.GroupWithZero.Divisibility
dvdNotUnit_of_dvd_of_not_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a b : α}, a ∣ b → ¬b ∣ a → DvdNotUnit a b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  s.leadingExp =
    match s.head with
    | none => ⊥
    | some (exp, snd) => ↑exp
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Constructor for functors from `FreeRefl`.
(See also `lift` for which the data is bundled.)  -/
CategoryTheory.Cat.FreeRefl.lift' : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        (obj : V → D) →
          (map : {v w : V} → (v ⟶ w) → (obj v ⟶ obj w)) →
            (∀ (v : V), map (CategoryTheory.ReflQuiver.id v) = CategoryTheory.CategoryStruct.id (obj v)) →
              CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) D
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_mono : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousAdd G]
  {H K : OpenNormalAddSubgroup G}, H ≤ K → H.toFiniteIndexNormalAddSubgroup ≤ K.toFiniteIndexNormalAddSubgroup
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- Let `X` be a light condensed set. We define a topology on `X(*)` as the quotient topology of
all the maps from light profinite sets `S` to `X(*)`, corresponding to elements of `X(S)`.
In other words, the topology coinduced by the map `LightCondSet.coinducingCoprod` above.  -/
LightCondSet.underlyingTopologicalSpace : (X : LightCondSet) → TopologicalSpace (X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.contains (t.min he) = true
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instNoNatZeroDivisorsQOfAddRightCancel : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [Lean.Grind.AddRightCancel α] [Lean.Grind.NoNatZeroDivisors α],
  Lean.Grind.NoNatZeroDivisors (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.GroupTheory.DoubleCoset
/-- **Alias** of `DoubleCoset.iUnion_quotToDoubleCoset`. -/
DoubleCoset.union_quotToDoubleCoset : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), ⋃ q, DoubleCoset.quotToDoubleCoset H K q = Set.univ
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_mul_I : ∀ (x : ℂ), Complex.cosh (x * Complex.I) = Complex.cos x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_lineMap_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder 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} (y : P), x ∈ s → ∀ {t : R}, t ≤ 0 → s.WOppSide y ((AffineMap.lineMap x y) t)
-- Mathlib.Data.PNat.Interval
PNat.card_fintype_Ioo : ∀ (a b : ℕ+), Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_star : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] (f : R → R) (a : A),
  autoParam (ContinuousOn f (star '' spectrum R a)) cfc_comp_star._auto_1 →
    autoParam (p a) cfc_comp_star._auto_3 → cfc (fun x => f (star x)) a = cfc f (star a)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.mem_pure : ∀ {α : Type u} {a : α} {s : Set α}, s ∈ pure a ↔ a ∈ s
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.mul_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Mul γ] [MeasurableMul γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => f x * c) (fun x => g x * c) μ ν
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_injective : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A),
  Function.Injective HomogeneousLocalization.val
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K`  -/
NumberField.RingOfIntegers.equiv : {K : Type u_1} →
  [inst : Field K] →
    (R : Type u_3) →
      [inst_1 : CommRing R] → [inst_2 : Algebra R K] → [IsIntegralClosure R ℤ K] → NumberField.RingOfIntegers K ≃+* R
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_of_tendsto_zero : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop (nhds 0) → (Hyperreal.ofSeq f).Infinitesimal
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.Skeleton.toSkeleton_tensorObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.toSkeleton (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) =
    CategoryTheory.toSkeleton X * CategoryTheory.toSkeleton Y
-- Mathlib.Analysis.Calculus.FDeriv.Const
Set.Subsingleton.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set E}, s.Subsingleton → DifferentiableOn 𝕜 f s
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.muFun.eq_1 : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a x : α),
  IncidenceAlgebra.muFun✝ 𝕜 a x =
    if a = x then 1
    else
      -∑ x_1 ∈ (Finset.Ico a x).attach,
          have h := ⋯;
          have this := ⋯;
          IncidenceAlgebra.muFun✝ 𝕜 a ↑x_1
-- Mathlib.Analysis.Complex.Trigonometric
Real.cot_eq_cos_div_sin : ∀ (x : ℝ), x.cot = Real.cos x / Real.sin x
-- Init.Data.List.Find
List.idxOf_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {y : α} [inst : BEq α],
  List.idxOf y (x :: xs) = bif x == y then 0 else List.idxOf y xs + 1
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instDecidableEqUnitVal.decEq : {α : ℚ} → (x x_1 : Std.Time.Internal.UnitVal α) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumLift_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom G) (g : F.Hom G)
  (x : (E.sum F).I₀),
  (CategoryTheory.PreZeroHypercover.sumLift f g).h₀ x =
    match x with
    | Sum.inl i => f.h₀ i
    | Sum.inr i => g.h₀ i
-- Mathlib.NumberTheory.FLT.Basic
/-- A relaxed variant of Fermat's Last Theorem over a given commutative semiring with a specific
exponent, allowing nonzero solutions of units and their common multiples.

1. The variant `FermatLastTheoremWith' R` is weaker than `FermatLastTheoremWith R` in general.
   In particular, it holds trivially for `[Field R]`.
2. This variant is equivalent to the original `FermatLastTheoremWith R` for `R = ℕ` or `ℤ`.
   In general, they are equivalent if there is no solutions of units to the Fermat equation.
3. For a polynomial ring `R = k[X]`, the original `FermatLastTheoremWith R` is false but the weaker
   variant `FermatLastTheoremWith' R` is true. This polynomial variant of Fermat's Last Theorem
   can be shown elementarily using Mason--Stothers theorem.
 -/
FermatLastTheoremWith' : (R : Type u_2) → [CommSemiring R] → ℕ → Prop
-- Mathlib.Topology.Gluing
TopCat.GlueData.toGlueData : TopCat.GlueData → CategoryTheory.GlueData TopCat
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_minKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {km kmm : α} (hkm : t.minKey? = some km), (t.modify k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.instTopologicalSpaceUnitDisc : TopologicalSpace Complex.UnitDisc
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.quasiIso_unopFunctor_map_iff : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L)
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i],
  QuasiIso ((HomologicalComplex.unopFunctor V c).map φ.op) ↔ QuasiIso φ
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.mem_iff : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : StarAddMonoid R] {x : R}, x ∈ skewAdjoint R ↔ star x = -x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Two right Kan extensions are (canonically) isomorphic.  -/
CategoryTheory.Functor.rightKanExtensionUnique : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] →
                      (F'' : CategoryTheory.Functor D H) →
                        (α' : L.comp F'' ⟶ F) → [F''.IsRightKanExtension α'] → F' ≅ F''
-- Mathlib.Algebra.Star.Unitary
/-- **Alias** of the reverse direction of `IsUnit.mem_unitary_iff_star_mul_self`. -/
IsUnit.mem_unitary_of_star_mul_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, IsUnit u → star u * u = 1 → u ∈ unitary R
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_empty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f ∅
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_algebraMap : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : R},
  IsIntegral R ((algebraMap R A) x)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasColimits : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R], CategoryTheory.Limits.HasColimits (TopModuleCat R)
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The product of the `m` first objects of `M` and the rest of the rest of `N`  -/
CategoryTheory.Limits.SequentialProduct.functorObj : {C : Type u_1} →
  (ℕ → C) →
    (ℕ → C) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Limits.HasCountableProducts C] → ℕ → C
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.equivMapOfInjective_coe_addEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) (e : M ≃+ N),
  S.equivMapOfInjective ↑e ⋯ = e.addSubmonoidMap S
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- Given a pseudofunctor `F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat` and a family
of morphisms `f i : X i ⟶ S` in `C`, this is the category of descent data for `F`
relative to the morphisms `f i` where the objects are defined as coalgebras:
the morphisms relating the various objects `obj i` over `X i` are of the
form `obj i₁ ⟶ (f i₁)^* (f i₂)_* (obj i₂)`. This category can be compared
to the corresponding category `DescentData` when suitable pullbacks exist
and certain base change morphisms are isomorphisms (TODO).  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
        (CategoryTheory.Bicategory.Adj CategoryTheory.Cat) →
      {ι : Type t} → {S : C} → {X : ι → C} → ((i : ι) → X i ⟶ S) → Type (max (max t u') v')
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Composition of two equivariant maps.  -/
AddActionHom.comp : {M : Type u_2} →
  {N : Type u_3} →
    {P : Type u_4} →
      {φ : M → N} →
        {ψ : N → P} →
          {χ : M → P} →
            {X : Type u_5} →
              [inst : VAdd M X] →
                {Y : Type u_6} →
                  [inst_1 : VAdd N Y] →
                    {Z : Type u_7} →
                      [inst_2 : VAdd P Z] → (Y →ₑ[ψ] Z) → (X →ₑ[φ] Y) → [κ : CompTriple φ ψ χ] → X →ₑ[χ] Z
-- Std.Do.SPred.SPred
/-- Universal quantifier in `SPred`.  -/
Std.Do.SPred.forall : {α : Sort u} → {σs : List (Type v)} → (α → Std.Do.SPred σs) → Std.Do.SPred σs
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.commRingNorm c e p) = 1 + sizeOf c + sizeOf e + sizeOf p
-- Mathlib.NumberTheory.LSeries.Deriv
/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
the `m`th derivative of this L-series is `(-1)^m` times the L-series of `log^m * f`.  -/
LSeries_iteratedDeriv : ∀ {f : ℕ → ℂ} (m : ℕ) {s : ℂ},
  LSeries.abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (LSeries.logMul^[m] f) s
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- Harder inclusion: at a point in `D f K`, the function `f` has a derivative, in `K`.  -/
RightDerivMeasurableAux.D_subset_differentiable_set : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {K : Set F},
  IsComplete K →
    RightDerivMeasurableAux.D f K ⊆ {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K}
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.comp_neg : ∀ {M : Type u_2} {G : Type u_5} {H : Type u_6} [inst : AddZeroClass M] [inst_1 : AddCommGroup G]
  [inst_2 : AddCommGroup H] (φ : G →+ H) (ψ : M →+ G), φ.comp (-ψ) = -φ.comp ψ
-- Mathlib.RingTheory.Perfection
Perfection.coeff_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n : ℕ), (Perfection.coeff R p (n + 1)) ((frobenius (Perfection R p) p) f) = (Perfection.coeff R p n) f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.insert k v).get k ⋯ = v
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
/-- If `T` is a flat `R`-module, the base change of the cotangent space of `I` is linearly
equivalent to the cotangent space of the extended ideal `I · (T ⊗[R] S)`.  -/
Ideal.tensorCotangentEquiv : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                (I : Ideal S) →
                  [Module.Flat R T] →
                    TensorProduct R T I.Cotangent ≃ₗ[T]
                      (Ideal.map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.compl_isIndContained_compl`. -/
SimpleGraph.IsIndContained.compl : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, G.IsIndContained H → Gᶜ.IsIndContained Hᶜ
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $((X_i)_{i \in \iota}, (Y_j)_{j \in \kappa})$ is Gaussian, then $(X_i)_{i \in \iota}$ and
$(Y_j)_{j \in \kappa}$ are independent if for all $i \in \iota, j \in \kappa$,
$\mathrm{Cov}(X_i, Y_j) = 0$.  -/
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_4} {κ : Type u_5} [Finite ι]
  [Finite κ] {X : ι → Ω → ℝ} {Y : κ → Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω => (fun i => X i ω, fun j => Y j ω)) P →
    (∀ (i : ι) (j : κ), ProbabilityTheory.covariance (X i) (Y j) P = 0) →
      ProbabilityTheory.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) P
-- Mathlib.Order.UpperLower.Closure
lowerClosure_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} (f : α ≃o β),
  lowerClosure (⇑f '' s) = (LowerSet.map f) (lowerClosure s)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.formallySmooth_stalkMap_iff : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (V : X.Opens) (hV : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
      (hx : x ∈ V),
      (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth ↔
        hV.primeIdealOf ⟨x, hx⟩ ∈
          Algebra.smoothLocus ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op V))
-- Init.Data.List.Lemmas
List.eraseDupsBy.loop.eq_1 : ∀ {α : Type u_1} (r : α → α → Bool) (a : List α), List.eraseDupsBy.loop r [] a = a.reverse
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.category : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) → CategoryTheory.Category.{v_1, u_1} (CategoryTheory.Quotient r)
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.findLeadingSpacesSize.consumeSpaces : {s : String} → s.Pos → ℕ → ℕ → ℕ
-- Lean.Meta.Sorry
/-- Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
If it is, then the `sorry` takes the first three arguments, and the tag is at argument 3.
 -/
Lean.Meta.isLabeledSorry? : Lean.Expr → Option Lean.Meta.SorryLabelView
-- Mathlib.Order.CompleteLattice.Basic
sSup_eq_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Proposition that `toFun` is continuous  -/
ContinuousMonoidHom.continuous_toFun : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A →ₜ* B), Continuous (↑self.toMonoidHom).toFun
-- Mathlib.Order.Filter.Defs
Filter.instSupSet : {α : Type u_1} → SupSet (Filter α)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Prime.deficient : ∀ {n : ℕ}, Nat.Prime n → n.Deficient