mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.ext_iff : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type w} {x y : Std.Iterators.PostconditionT m α},
  x = y ↔ ∃ (h : x.Property = y.Property), (fun p => ⟨↑p, ⋯⟩) <$> x.operation = y.operation
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : SizeOf C]
  (toPrecoverage : CategoryTheory.Precoverage C)
  (pullback :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f),
  sizeOf { toPrecoverage := toPrecoverage, pullback := pullback } = 1 + sizeOf toPrecoverage
-- Aesop.Tree.ExtractScript
Aesop.GoalRef.extractSafePrefixScriptCore : Aesop.GoalRef → Aesop.ExtractScriptM Unit
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_toQuadraticMap : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (B : LinearMap.BilinMap R M N) (x y : M),
  (((QuadraticMap.associatedHom S) B.toQuadraticMap) x) y = ⅟2 • ((B x) y + (B y) x)
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- A submonoid of an ordered cancellative monoid is an ordered cancellative monoid.  -/
SubmonoidClass.toIsOrderedCancelMonoid : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : CommMonoid M] [inst_2 : Preorder M]
  [IsOrderedCancelMonoid M] [inst_4 : SubmonoidClass S M] (s : S), IsOrderedCancelMonoid ↥s
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- The functor `(C₁ ⥤ C₂₃ ⥤ C₄) ⥤ (C₂ ⥤ C₃ ⥤ C₂₃) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` which
sends `F : C₁ ⥤ C₂₃ ⥤ C₄` and `G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃` to the
functor `bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄`.  -/
CategoryTheory.bifunctorComp₂₃Functor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₂₃ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] →
                    CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
                      (CategoryTheory.Functor (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃))
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))))
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Submodule.ClosedComplemented.of_finiteDimensional_of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {A B : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥A], A.ClosedComplemented → ∀ [T2Space ↥A], B ≤ A → B.ClosedComplemented
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.underToAlgebra_obj_A : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (f : CategoryTheory.Under X), ((CategoryTheory.underToAlgebra X).obj f).A = f.right
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Topology.Neighborhoods
lift'_nhds_interior : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).lift' interior = nhds x
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.lTensor_comp_δ : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u}
  [inst_1 : CommSemiring k] (f : X ⟶ Y),
  (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp
      (Representation.LinearizeMonoidal.δ Z X) =
    (Representation.LinearizeMonoidal.δ Z Y).comp
      (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.notReady.sizeOf_spec : sizeOf Lean.Meta.Grind.SplitStatus.notReady = 1
-- Init.Data.Array.Subarray
/-- Checks whether any of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that satisfies the predicate is found.
 -/
Subarray.any : {α : Type u} → (α → Bool) → Subarray α → Bool
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_comp_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  {T : Type u_2} [inst_3 : CommRing S] [inst_4 : CommRing T] (f : T →+* R) (g : R →+* S) (x : GL n T),
  ((Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)) x =
    (Matrix.GeneralLinearGroup.map g) ((Matrix.GeneralLinearGroup.map f) x)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Realization of a term of `Witness K ι X` as a section of `F` over `X`. By
construction, the sections will lie in the subsheaf `K.subsheafify 𝒮`.
This takes values in `Option`, because not every term constructed from
the `Witness.amalgamate` constructor corresponds to a compatible family.  -/
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) →
          (ι : C → Type (max u v)) →
            ((X : C) → ι X → F.obj (Opposite.op X)) →
              {X : C} → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι X → Option (F.obj (Opposite.op X))
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`.  -/
Real.binEntropy_neg_of_neg : ∀ {p : ℝ}, p < 0 → Real.binEntropy p < 0
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_eq_one_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α] (u : α), G.eccent u = 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v
-- Mathlib.Order.WithBot
WithBot.map_id : ∀ {α : Type u_1}, WithBot.map id = id
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (d : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d =
    ((CategoryTheory.Functor.Monoidal.εIso (CategoryTheory.Functor.id (CategoryTheory.Functor C C))).app d).symm
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) (i : n) (j : m), M.transpose i j = M j i
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.pi_apply_single : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (i : ι)
  (m : Mᵢ i), (QuadraticMap.pi Q) (Pi.single i m) = (Q i) m
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift.eq_3 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (val : α₂)
  (val_1 : β₁), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) (Sum.inl val_1) = ∅
-- Qq.Macro
Qq.Impl.MVarSynth.term : Lean.Expr → Lean.MVarId → Qq.Impl.MVarSynth
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.submodule_eq_span_le_iff_stable_ge : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M) (n₀ : ℕ),
  F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), PolynomialModule.single R i '' ↑(F.N i)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of `additive_of_symm_of_total`. -/
additive_of_symmetric_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β] (p r : α → α → Prop) [Std.Total r] (f : α → α → β) [Std.Symm p],
  (∀ {a b : α}, p a b → f a b + f b a = 0) →
    (∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b + f b c) →
      ∀ {a b c : α}, p a b → p b c → p a c → f a c = f a b + f b c
-- Mathlib.CategoryTheory.Abelian.Images
/-- An alternative formulation of the canonical map from the abelian coimage to the abelian image.
 -/
CategoryTheory.Abelian.coimageImageComparison' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel f] →
              [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
                [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
                  CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
CovariantDerivative.isMetricCompatible_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [inst_12 : IsContMDiffRiemannianBundle I 1 F V]
  [inst_13 : ContMDiffVectorBundle 1 F V I] [inst_14 : IsManifold I 1 M] [inst_15 : FiniteDimensional ℝ F],
  cov.IsMetricCompatible ↔
    ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
      MDiffAt (T% X) x →
        MDiffAt (T% σ) x →
          MDiffAt (T% τ) x →
            ((d% fun x => inner ℝ (σ x) (τ x)) x) (X x) =
              (fun x => inner ℝ ((fun x => (↑cov σ x) (X x)) x) (τ x)) x +
                (fun x => inner ℝ (σ x) ((fun x => (↑cov τ x) (X x)) x)) x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.command? : Lean.Lsp.InlayHintLabelPart → Option Lean.Lsp.Command
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_comp_ofLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y Z : CategoryTheory.Subobject B) (h₁ : X ≤ Y)
  (h₂ : Y ≤ Z), CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLE Z h₂) = X.ofLE Z ⋯
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_cWeight_const_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] (f : ι → 𝕜) (a : 𝕜),
  ⟪f, Function.const ι a⟫ₙ_[𝕜] = a * Finset.univ.expect fun i => (starRingEnd 𝕜) (f i)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.abs_omega : |Hyperreal.omega| = Hyperreal.omega
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_assoc : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.join (Lean.Order.join P Q) R = Lean.Order.join P (Lean.Order.join Q R)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  (f g : X ⟶ Y), f.left = g.left → f.right = g.right → f = g
-- Mathlib.Data.List.Perm.Basic
List.instSymmPerm_mathlib : ∀ {α : Type u_1}, Std.Symm List.Perm
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- `LiouvilleNumber.remainder` is the sum of the series of the terms in `liouvilleNumber m`
starting from `k+1`, i.e
$$
\sum_{i=k+1}^\infty\frac{1}{m^{i!}}.
$$
 -/
LiouvilleNumber.remainder : ℝ → ℕ → ℝ
-- Mathlib.Topology.Algebra.Group.Basic
discreteTopology_iff_isOpen_singleton_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G],
  DiscreteTopology G ↔ IsOpen {0}
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {F : CategoryTheory.Sheaf J A} {M : A}
  (f : F ⟶ Φ.skyscraperSheaf M),
  (Φ.skyscraperSheafAdjunction.homEquiv F M).symm f = Φ.skyscraperPresheafHomEquiv.symm f.hom
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c)).obj x))
      ⋯
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.mono : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {K L : ℝ} {A B : Set X},
  K ≤ L → CovBySMul M K A B → CovBySMul M L A B
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.reverse_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.mapLe h p).reverse = SimpleGraph.Walk.mapLe h p.reverse
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k fallback : α},
  m.contains k = true → m.getKeyD k fallback = k
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.of_add_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n₁ n₂ : N),
  TensorProduct.Eqv R M N (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) (FreeAddMonoid.of (m, n₁ + n₂))
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
right Kan extension at `Y` iff `E'` is.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E E' : L.RightExtension F} →
                  (E ≅ E') → (Y : D) → E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0}
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_7} [inst_1 : NormedAddCommGroup E]
  [inst_2 : PartialOrder E] [inst_3 : NormedSpace ℝ E] [IsOrderedModule ℝ E],
  MeasurableSet s → μ s ≠ ⊤ → ∀ (x : E), 0 ≤ x → 0 ≤ (MeasureTheory.condExpInd E hm μ s) x
-- Mathlib.Tactic.SetNotationForOrder
/-- Elaborator for `x ⊆ y` notation.  -/
Mathlib.Meta.SetNotationForOrder.elabSubsetStx' : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- Linear independent families are injective, even if you multiply either side.  -/
LinearIndependent.eq_of_smul_apply_eq_smul_apply : ∀ {ι : Type u'} {R : Type u_2} [inst : Semiring R] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M}, LinearIndependent R v → ∀ (c d : R) (i j : ι), c ≠ 0 → c • v i = d • v j → i = j
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.other.sizeOf_spec : ∀ (key : Lean.Name), sizeOf (Mathlib.Notation3.DelabKey.other key) = 1 + sizeOf key
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) =
          CategoryTheory.CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk e comm).inv.hom i = (e i).inv
-- Mathlib.Order.RelSeries
RelSeries.toList_snoc : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  (p.snoc newLast rel).toList = p.toList ++ [newLast]
-- Init.Data.Array.Attach
Array.pmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (H : ∀ a ∈ xs, p a),
  Array.pmap (fun a x => f a) xs H = Array.map f xs
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instInhabitedKey.default : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- If `f` and `g` are two torus integrable functions, then so is `f - g`.  -/
TorusIntegrable.sub : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] {f g : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ},
  TorusIntegrable f c R → TorusIntegrable g c R → TorusIntegrable (f - g) c R
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.shiftₗ_pow_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (k : ℕ) (y : M),
  (fwdDiff_aux.shiftₗ M G h ^ k) f y = f (y + k • h)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsSeparating →
    ∀ {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (α : C ≌ D), (P.strictMap α.functor).IsSeparating
-- Lean.Data.Trie
Lean.Data.Trie.instInhabited : {α : Type} → Inhabited (Lean.Data.Trie α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).keysArray =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keysArray.attach).unattach
-- Mathlib.Topology.Algebra.Order.Floor
continuousOn_ceil : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α] (n : ℤ),
  ContinuousOn (fun x => ↑⌈x⌉) (Set.Ioc (↑n - 1) ↑n)
-- Std.Internal.Do.Order.Basic
Lean.Order.le_top : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x : α), Lean.Order.PartialOrder.rel x Lean.Order.top
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_eq_one_iff : ∀ {z : ℤ}, UniqueFactorizationMonoid.radical z = 1 ↔ z.natAbs ≤ 1
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Lebesgue dominated convergence theorem for series.  -/
MeasureTheory.hasSum_setToFun_of_dominated_convergence : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {ι : Type u_7} [Countable ι]
  {F_1 : ι → α → E} {f : α → E} (bound : ι → α → ℝ),
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F_1 n) μ) →
    (∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F_1 n a‖ ≤ bound n a) →
      (∀ᵐ (a : α) ∂μ, Summable fun n => bound n a) →
        MeasureTheory.Integrable (fun a => ∑' (n : ι), bound n a) μ →
          (∀ᵐ (a : α) ∂μ, HasSum (fun n => F_1 n a) (f a)) →
            HasSum (fun n => MeasureTheory.setToFun μ T hT (F_1 n)) (MeasureTheory.setToFun μ T hT f)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_sup_comap_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f →
    ∀ (p q : Submodule R₂ M₂), Submodule.map f (Submodule.comap f p ⊔ Submodule.comap f q) = p ⊔ q
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- The domain of an initial functor is connected if and only if its codomain is connected.  -/
CategoryTheory.Functor.isConnected_iff_of_initial : ∀ {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.Initial], CategoryTheory.IsConnected C ↔ CategoryTheory.IsConnected D
-- Init.Data.UInt.Lemmas
UInt16.toNat_neg : ∀ (a : UInt16), (-a).toNat = (UInt16.size - a.toNat) % UInt16.size
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.isLinearMap_smul' : ∀ {R : Type u_14} {M : Type u_15} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : M),
  IsLinearMap R fun c => c • a
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.id_obj : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u₁)
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X : C), (CategoryTheory.EnrichedFunctor.id V C).obj X = X
-- Init.Dynamic
_private.Init.Dynamic.0.TypeName.data : {α : Type u} → [self : TypeName α] → (TypeNameData α).type
-- Mathlib.LinearAlgebra.Quotient.Basic
LinearMap.ker_le_range_iff : ∀ {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} {R₃ : Type u_5} {M₃ : Type u_6} [inst : Ring R]
  [inst_1 : Ring R₂] [inst_2 : Ring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommGroup M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} [inst_9 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃},
  g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0
-- Lean.DocString.Types
/-- The description itself.  -/
Lean.Doc.DescItem.desc : {α : Type u} → {β : Type v} → Lean.Doc.DescItem α β → Array β
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zpow_le_of_le_log : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhds_basis' : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X},
  (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.TransferEncoding.mk : (codings : Array String) → Std.Http.Header.TransferEncoding.Validate codings = true → Std.Http.Header.TransferEncoding