mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.quotient_obj_obj_as : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CochainComplex.Plus C), ((HomotopyCategory.Plus.quotient C).obj X).obj.as = X.obj
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.inv_smul_set_distrib : ∀ {α : Type u_2} [inst : Group α] (a : α) (s : Set α), (a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
-- Mathlib.FieldTheory.Galois.Abelian
/-- The class of abelian extensions,
defined as galois extensions whose galois group is commutative.  -/
IsAbelianGalois : (K : Type u_4) → (L : Type u_5) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Prop
-- Std.Sat.CNF.Basic
Std.Sat.CNF.eval_congr : ∀ {α : Type u_1} (a1 a2 : α → Bool) (f : Std.Sat.CNF α),
  (∀ (v : α), Std.Sat.CNF.VarMem v f → a1 v = a2 v) → Std.Sat.CNF.eval a1 f = Std.Sat.CNF.eval a2 f
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots : ∀ {X : Type u_1} (self : DiffeologicalSpace.CorePlotsOn X) {u : Set X},
  TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), self.isPlot p → IsOpen (p ⁻¹' u)
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- The regular action of a group on itself is transitive.  -/
AddAction.Regular.isPretransitive : ∀ {G : Type u_2} [inst : AddGroup G], AddAction.IsPretransitive G G
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_smul_integral_map : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]
  [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ* G),
  MeasureTheory.mulEquivHaarChar φ • ∫ (a : G), f a ∂MeasureTheory.Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ
-- Mathlib.Dynamics.Ergodic.Action.Regular
instErgodicSMulOfIsMulLeftInvariant : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant], ErgodicSMul G G μ
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} A]
  [inst_2 : CategoryTheory.MonoidalCategory A] [inst_3 : CategoryTheory.MonoidalClosed A] {M : A}
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y : C} (f : X ⟶ Y)
  [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G]
  (y :
    ((CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G).comp
          (CategoryTheory.coyoneda.obj (Opposite.op M))).obj
      (Opposite.op Y)),
  (CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv M F G X)
      (CategoryTheory.CategoryStruct.comp y
        (CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' A (CategoryTheory.Under.map f.op)
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Under.map f.op).comp ((CategoryTheory.Under.forget (Opposite.op Y)).comp F)))
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Under.map f.op).comp ((CategoryTheory.Under.forget (Opposite.op Y)).comp G))))) =
    (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.presheafHom
              (CategoryTheory.MonoidalCategoryStruct.tensorObj F ((CategoryTheory.Functor.const Cᵒᵖ).obj M)) G).map
          f.op))
      ((CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv M F G Y) y)
-- Mathlib.Testing.Plausible.Functions
/-- Apply a total function to an argument.  -/
Plausible.InjectiveFunction.apply : {α : Type u} → [DecidableEq α] → Plausible.InjectiveFunction α → α → α
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a left lift along `g : c ⟶ a` from a left lift along `𝟙 c ≫ g`.  -/
CategoryTheory.Bicategory.LeftLift.ofIdComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          CategoryTheory.Bicategory.LeftLift f
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g) →
            CategoryTheory.Bicategory.LeftLift f g
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_le_blsub : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), o.bsup f ≤ o.blsub f
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Ordered.mem_inner_iff_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (sz : ℕ) (a : α) (v : β a) (l r : Std.DTreeMap.Internal.Impl α β)
  (k : α), compare k a = Ordering.gt → (k ∈ Std.DTreeMap.Internal.Impl.inner sz a v l r ↔ k ∈ r)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_natCast : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (n : ℕ), Polynomial.evalEval x y ↑n = ↑n
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_eq_support_sub : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), f.neLocus g = (f - g).support
-- Lean.Data.Json.Basic
Lean.Json.instCoeBool : Coe Bool Lean.Json
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a `G`-representation `A` and a normal subgroup `S ≤ G`, the map
`H₁(G, A) ⟶ H₁(G ⧸ S, A_S)` induced by the quotient maps `G →* G ⧸ S` and `A →ₗ A_S` is an
epimorphism.  -/
groupHomology.instEpiModuleCatGH1CoresCoinf : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  CategoryTheory.Epi (groupHomology.H1CoresCoinf A S).g
-- Mathlib.Topology.Order.Bornology
Bornology.IsBounded.subset_Icc_sInf_sSup : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : ConditionallyCompleteLattice α] [IsOrderBornology α] {s : Set α},
  Bornology.IsBounded s → s ⊆ Set.Icc (sInf s) (sSup s)
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_pos_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → (0 < a ^ n ↔ 0 < a)
-- Mathlib.Data.Nat.Log
Nat.pow_log_le_add_one : ∀ (b x : ℕ), b ^ Nat.log b x ≤ x + 1
-- Mathlib.Algebra.GCDMonoid.Nat
/-- **Alias** of `Int.strongNormalizationMonoid`. -/
Int.normalizationMonoid : StrongNormalizationMonoid ℤ
-- Mathlib.Topology.Order
closure.mono : ∀ {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α}, t₁ ≤ t₂ → closure s ⊆ closure s
-- Mathlib.Order.Filter.CardinalInter
/-- Every CountableInterFilter is a CardinalInterFilter with c = ℵ₁  -/
CountableInterFilter.toCardinalInterFilter : ∀ {α : Type u} (l : Filter α) [CountableInterFilter l], CardinalInterFilter l (Cardinal.aleph 1)
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
matPolyEquiv_coeff_apply_aux_2 : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n)
  (p : Polynomial R) (k : ℕ), (matPolyEquiv (Matrix.single i j p)).coeff k = Matrix.single i j (p.coeff k)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidalStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.AddMon C)
-- Mathlib.Data.Num.Basic
instInhabitedPosNum : Inhabited PosNum
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tsum_measure_le_measure_univ : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) → ∑' (i : ι), μ (s i) ≤ μ Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      t.isEmpty = true → ∀ {fallback : α}, (Std.DTreeMap.Internal.Impl.insert! k v t).minKeyD fallback = k
-- Lean.Util.Trace
Lean.instMonadAlwaysExceptReaderT : {m : Type → Type} → {ε ρ : Type} → [always : Lean.MonadAlwaysExcept ε m] → Lean.MonadAlwaysExcept ε (ReaderT ρ m)
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.symmMeasurableEquiv_apply : ∀ (a : ↑unitInterval), unitInterval.symmMeasurableEquiv a = unitInterval.symm a
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instStarRing : {n : Type u_2} →
  {A : Type u_5} → [inst : Fintype n] → [inst_1 : NonUnitalSemiring A] → [StarRing A] → StarRing (CStarMatrix n n A)
-- Mathlib.GroupTheory.Nilpotent
/-- Any ascending central series for a group is bounded above by the upper central series.  -/
Subgroup.ascending_central_series_le_upper : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsAscendingCentralSeries H → ∀ (n : ℕ), H n ≤ Subgroup.upperCentralSeries G n
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ_comp_liftRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m)
  (n : ℕ), (↑(AdicCompletion.evalₐ I n)).comp (AdicCompletion.liftRingHom I f ⋯) = f n
-- Mathlib.Analysis.Convex.Caratheodory
Caratheodory.minCardFinsetOfMemConvexHull_subseteq : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} (hx : x ∈ (convexHull 𝕜) s),
  ↑(Caratheodory.minCardFinsetOfMemConvexHull hx) ⊆ s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- The condition that a commutative square is a pullback square.  -/
CategoryTheory.Square.IsPullback : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → Prop
-- Lean.Parser.Command
Lean.Parser.Command.printEqns : Lean.Parser.Parser
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α},
  t.size ≤ (t.insertMany l).size
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.ι₂_ι_assoc : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {Z : SSet}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.unionProd.ι₂ S T)
      (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight S.ι Y) h
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The equivalence between connected components, induced by an isomorphism of graphs,
itself defines an equivalence on the supports of each connected component.
 -/
SimpleGraph.ConnectedComponent.isoEquivSupp : {V : Type u} →
  {V' : Type v} →
    {G : SimpleGraph V} →
      {G' : SimpleGraph V'} → (φ : G ≃g G') → (C : G.ConnectedComponent) → ↑C.supp ≃ ↑(φ.connectedComponentEquiv C).supp
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_subgroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ (H : Subgroup G), IsPGroup p ↥H
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.lift_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)) (a : R),
  (IsLocalization.Away.lift x hg) ((algebraMap R S) a) = g a
-- Mathlib.Topology.Category.LightProfinite.Basic
lightProfiniteToLightDiagram_obj : ∀ (X : LightProfinite), lightProfiniteToLightDiagram.obj X = X.toLightDiagram
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.disjointBase`. -/
Topology.CWComplex.disjointBase : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Disjoint (Topology.RelCWComplex.openCell n i) D
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_ofSubtype : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] (f : Equiv.Perm (Subtype p)),
  (Equiv.Perm.ofSubtype f).subtypePerm ⋯ = f
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- For level `N = 1`, the gamma sets are all equivalent; this is the equivalence.  -/
EisensteinSeries.gammaSet_one_equiv : (r : ℕ) → (a a' : Fin 2 → ZMod 1) → ↑(EisensteinSeries.gammaSet 1 r a) ≃ ↑(EisensteinSeries.gammaSet 1 r a')
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For an additive Lie group `G` and open sets `U ⊆ V` in `N`, the 'restriction'
group homomorphism from `C^n⟮I, V; I', G⟯` to `C^n⟮I, U; I', G⟯`.  -/
ContMDiffMap.restrictAddMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    (G : Type u_10) →
                                      [inst_9 : AddMonoid G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [inst_12 : ContMDiffAdd I' n G] →
                                              {U V : TopologicalSpace.Opens N} →
                                                U ≤ V → ContMDiffMap I I' (↥V) G n →+ ContMDiffMap I I' (↥U) G n
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.buckets_size_withComputedSize : ∀ {α : Type u} {β : α → Type v} {self : Array (Std.DHashMap.Internal.AssocList α β)},
  (Std.DHashMap.Internal.withComputedSize self).buckets.size = self.size
-- Init.Data.String.Defs
/-- The past-the-end position of `s`, as an `s.Pos`.  -/
String.Slice.endPos : (s : String.Slice) → s.Pos
-- Mathlib.Algebra.Ring.BooleanRing
OrderIso.asBoolAlgAsBoolRing_apply : ∀ (α : Type u_4) [inst : BooleanAlgebra α] (a : AsBoolAlg (AsBoolRing α)),
  (OrderIso.asBoolAlgAsBoolRing α) a = ofBoolRing (ofBoolAlg a)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.diagram.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j k : J} (f f_1 : j ⟶ k),
  (CategoryTheory.BiconeHom.diagram f = CategoryTheory.BiconeHom.diagram f_1) = (f = f_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_toSubtype_subtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C}
  (h : ⨁ Subtype.restrict p f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j) h
-- Init.Omega.Coeffs
/-- Shim for `IntList.dot`.  -/
Lean.Omega.Coeffs.dot : Lean.Omega.Coeffs → Lean.Omega.Coeffs → ℤ
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.isPlot_generatedFrom_of_mem : ∀ {X : Type u_1} {g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))} {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  ⟨n, p⟩ ∈ g → Diffeology.IsPlot p
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₁₂_nonneg : ∀ {p t x : ℝ}, 1 < p → 0 ≤ t → 0 ≤ x → 0 ≤ p.rpowIntegrand₁₂ t x
-- Init.Data.SInt.Lemmas
Int8.le_refl : ∀ (a : Int8), a ≤ a
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_or_le_inf_aux_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f q
-- Mathlib.Topology.Maps.Strict.Basic
Topology.IsStrictMap.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Topology.IsStrictMap f = Topology.IsQuotientMap (Set.rangeFactorization f)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_prod_nonempty_of_submultiplicative : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β), (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (s : Multiset α), s ≠ ∅ → f s.prod ≤ (Multiset.map f s).prod
-- Mathlib.FieldTheory.IsSepClosed
/-- Typeclass for an extension being a separable closure.  -/
IsSepClosure : (k : Type u) → [inst : Field k] → (K : Type v) → [inst_1 : Field K] → [Algebra k K] → Prop
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- `extendToSucc`, on morphisms.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSucc.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            ¬IsMax j →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} →
                  (F.obj ⟨j, ⋯⟩ ⟶ X) →
                    (i₁ i₂ : J) →
                      (hi : i₁ ≤ i₂) →
                        (hi₂ : i₂ ≤ Order.succ j) →
                          CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨i₁, ⋯⟩ ⟶
                            CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨i₂, hi₂⟩
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X')
  {n : ℕ} (i : Fin (n + 2)) {Z : C} (h : X'.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (f.app { len := n + 1 }) h) =
    CategoryTheory.CategoryStruct.comp (f.app { len := n }) (CategoryTheory.CategoryStruct.comp (X'.δ i) h)
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WithWF.instWellFoundedRelation : (α : Type w) →
  (m : Type w → Type w') →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
            (hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep) →
              WellFoundedRelation (Std.IteratorLoop.WithWF α m PlausibleForInStep hwf)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.hasToOmit : Lean.Name → Lean.Name → Lean.Elab.ConfigEval.M✝ Bool
-- Std.Time.Date.Unit.Month
Std.Time.Month.Ordinal.cumulativeDays_le : ∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.cumulativeDays leap month ≥ 0 ∧
    Std.Time.Month.Ordinal.cumulativeDays leap month ≤ 334 + if leap = true then 1 else 0
-- Lean.Meta.Tactic.Grind.Internalize
/-- Internalizes the `MatchCond` gadget.  -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeMatchCond : Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Init.Data.UInt.BasicAux
/-- Converts a `UInt64` into the corresponding `Fin UInt64.size`.  -/
UInt64.toFin : UInt64 → Fin UInt64.size
-- Init.Data.List.Sort.Basic
/-- A stable merge sort.

This function is a simplified implementation that's designed to be easy to reason about, rather than
for efficiency. In particular, it uses the non-tail-recursive `List.merge` function and traverses
lists unnecessarily.

It is replaced at runtime by an efficient implementation that has been proven to be equivalent.
 -/
List.mergeSort : {α : Type u_1} → List α → autoParam (α → α → Bool) List.mergeSort._auto_1 → List α
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_whiskerRight' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.inv f) Z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Mathlib.Order.Heyting.Basic
/-- `p ∧ (p → q) → q`  -/
inf_himp_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ (a ⇨ b) ≤ b
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_mono : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁ ≤ π₂ → π₁.iUnion ⊆ π₂.iUnion
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.Functor.Final.exists_coeq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c),
  ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsCoseparator G ↔ (CategoryTheory.preadditiveYonedaObj G).Faithful
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.isClosedEmbedding`.

---

**Alias** of `AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding`. -/
AlgebraicGeometry.IsClosedImmersion.base_closed : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsClosedImmersion f],
  Topology.IsClosedEmbedding ⇑f
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Adjunction.fromKleisli_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) {x Y : CategoryTheory.Kleisli T}
  (f : x ⟶ Y),
  (CategoryTheory.Kleisli.Adjunction.fromKleisli T).map f =
    CategoryTheory.CategoryStruct.comp (T.map f.of) (T.μ.app Y.of)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd_dual_comp_forget_to_partOrd : FinPartOrd.dual.comp (CategoryTheory.forget₂ FinPartOrd PartOrd) =
  (CategoryTheory.forget₂ FinPartOrd PartOrd).comp PartOrd.dual
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_uIcc : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.uIcc i j = Set.uIcc i.succ j.succ
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instInhabited : Inhabited CompactlyGenerated
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α} {f : Option β → Option β},
  (m.alter k f).getKey! k' = if (k == k') = true then if (f m[k]?).isSome = true then k else default else m.getKey! k'
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.lt_sInf_add_pos : ∀ {s : Set ℝ}, s.Nonempty → ∀ {ε : ℝ}, 0 < ε → ∃ a ∈ s, a < sInf s + ε
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Find the minimum element, and return a data structure `FindMin` with information
needed to reconstruct the rest of the binomial heap.
 -/
Batteries.BinomialHeap.Imp.Heap.findMin : {α : Type u_1} →
  (α → α → Bool) →
    (Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α) →
      Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Batteries.BinomialHeap.Imp.FindMin α