mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at most some nonnegative number `a` to show that `sSup s ≤ a`.

See also `csSup_le`.  -/
Real.sSup_le : ∀ {s : Set ℝ} {a : ℝ}, (∀ x ∈ s, x ≤ a) → 0 ≤ a → sSup s ≤ a
-- Mathlib.Data.Part
Part.coe_none : ∀ {α : Type u_1}, ↑none = Part.none
-- Mathlib.Order.Interval.Finset.DenselyOrdered
WithBot.denselyOrdered_set_iff_subsingleton : ∀ {X : Type u_1} [inst : LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithBot X)}, DenselyOrdered ↑s ↔ s.Subsingleton
-- Mathlib.Algebra.GCDMonoid.Nat
Int.instStrongNormalizedGCDMonoid : StrongNormalizedGCDMonoid ℤ
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.instFullIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithTerminal.incl.Full
-- Mathlib.Order.SupIndep
PartialOrder.toPreorder.hcongr_2 : ∀ (α α' : Type u_2),
  α = α' → ∀ (self : PartialOrder α) (self' : PartialOrder α'), self ≍ self' → self.toPreorder ≍ self'.toPreorder
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_app_snd_apply : ∀ {X : SSet} {m : ℕ} (x : X.obj (Opposite.op { len := m })) (k : Fin (m + 1)),
  ((CategoryTheory.ConcreteCategory.hom (SSet.ι₁.app (Opposite.op { len := m }))) x).2 k = 1
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃Functor_obj_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₃) (H : C₂) (K : C₁),
  (((CategoryTheory.Functor.flip₁₃Functor.obj F).obj G).obj H).obj K = ((F.obj K).obj H).obj G
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revEquivalence_unitIso : SimplexCategory.revEquivalence.unitIso = SimplexCategory.revCompRevIso.symm
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filter : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it : Std.IterM m β} [inst_1 : Monad m]
  [LawfulMonad m] {f : β → Bool},
  (Std.IterM.filter f it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        if h' : f out = true then pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filter f it') out ⋯))
        else pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filter f it') ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filter f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toNatCast : {α : Type u_1} → [self : NonAssocRing α] → NatCast α
-- Mathlib.Combinatorics.Hindman
Hindman.FP.below.cons' : ∀ {M : Type u_1} [inst : Semigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FP a a_1 → Prop} (a : Stream' M)
  (m : M) (h : Hindman.FP a.tail m), Hindman.FP.below h → motive a.tail m h → Hindman.FP.below ⋯
-- Lean.Syntax
Lean.unreachIsNodeIdent : {β : Sort u_1} →
  {info : Lean.SourceInfo} →
    {rawVal : Substring.Raw} →
      {val : Lean.Name} →
        {preresolved : List Lean.Syntax.Preresolved} → Lean.IsNode (Lean.Syntax.ident info rawVal val preresolved) → β
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalInterior_vadd : ∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α)
  [inst_2 : AddGroup H] [inst_3 : AddAction H α] [VAddCommClass H G α] (g : H),
  MeasureTheory.addFundamentalInterior G (g +ᵥ s) = g +ᵥ MeasureTheory.addFundamentalInterior G s
-- Lean.Modifiers
Lean.mkPrivateName : Lean.Environment → Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Equivalence.mapAction_functor : ∀ {V : Type u_2} {W : Type u_3} [inst : CategoryTheory.Category.{v_2, u_2} V]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} W] (G : Type u_4) [inst_2 : Monoid G] (E : V ≌ W),
  (CategoryTheory.Equivalence.mapAction G E).functor = E.functor.mapAction G
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.lt_power_cof_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c < c ^ c.ord.cof
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.loop.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive __do_lift
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `Real.sinh` as a `Homeomorph`.  -/
Real.sinhHomeomorph : ℝ ≃ₜ ℝ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.instInhabitedCoalgebraId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Inhabited C] → Inhabited (CategoryTheory.Endofunctor.Coalgebra (CategoryTheory.Functor.id C))
-- Std.Time.Time.Unit.Minute
/-- Converts an `Ordinal` to an `Offset`.
 -/
Std.Time.Minute.Ordinal.toOffset : Std.Time.Minute.Ordinal → Std.Time.Minute.Offset
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_combine : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (p₁.combine p₂) =
    Int.Internal.Linear.Poly.denote ctx p₁ + Int.Internal.Linear.Poly.denote ctx p₂
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.ofHom_id : ∀ (R : Type u) [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : Algebra R X],
  AlgCat.ofHom (AlgHom.id R X) = CategoryTheory.CategoryStruct.id (AlgCat.of R X)
-- Mathlib.Topology.Order.LawsonTopology
Topology.scottHausdorff_le_isLawson : ∀ {α : Type u_1} [inst : Preorder α] (L : TopologicalSpace α) [Topology.IsLawson α],
  Topology.scottHausdorff α Set.univ ≤ L
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPSorrySource : Lean.Options → Bool
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_insert_left : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a < b → insert a (Finset.Ioo a b) = Finset.Ico a b
-- Mathlib.Data.Ordmap.Ordset
Ordnode.valid'_singleton : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.nil.Bounded o₁ ↑x → Ordnode.nil.Bounded (↑x) o₂ → Ordnode.Valid' o₁ {x} o₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' : α} [hi : Inhabited β] {f : β → β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.modify k f t) k' =
        if compare k k' = Ordering.eq then (Option.map f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
        else Std.DTreeMap.Internal.Impl.Const.get! t k'
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Two families of seminorms `p` and `q` on the same space generate the same topology
if each `p i` is bounded by some `C • Finset.sup s q` and vice-versa.

We formulate these boundedness assumptions as `Seminorm.IsBounded q p LinearMap.id` (and
vice-versa) to reuse the API. Furthermore, we don't actually state it as an equality of topologies
but as a way to deduce `WithSeminorms q` from `WithSeminorms p`, since this should be more
useful in practice.  -/
WithSeminorms.congr : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} {ι' : Type u_10} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} [t : TopologicalSpace E],
  WithSeminorms p → Seminorm.IsBounded p q LinearMap.id → Seminorm.IsBounded q p LinearMap.id → WithSeminorms q
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.instCategory : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Category.{max (max u_2 u_3) u_4, max (max (max u_4 u_3) u_2) u_1}
            (CategoryTheory.Abelian.SpectralObject C ι)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f),
  CategoryTheory.Epi f
-- Lean.Elab.Tactic.Omega.Core
/-- Is a Fourier-Motzkin elimination empty (i.e. there are no relevant constraints).  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.isEmpty : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → Bool
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.ret.injEq : ∀ (a : Turing.ToPartrec.Cont) (a_1 : List ℕ) (a_2 : Turing.ToPartrec.Cont) (a_3 : List ℕ),
  (Turing.ToPartrec.Cfg.ret a a_1 = Turing.ToPartrec.Cfg.ret a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.continuousAt_iff' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Topology.IsInducing f → ∀ {x : X}, Set.range f ∈ nhds (f x) → (ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, Std.TreeMap.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_eq_zero : ∀ {x : Cardinal.{u_1}}, x.toENatAux = 0 ↔ x = 0
-- Batteries.Data.MLList.Basic
/-- The infinite monadic lazy list of natural numbers. -/
MLList.range : {m : Type → Type} → [Monad m] → MLList m ℕ
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : SemilatticeSup β] [inst_1 : OrderBot β] {P : β → Prop} (Pbot : P ⊥)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)), ⇑(SupBotHom.subtypeVal Pbot Psup) = Subtype.val
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.of_sublist : ∀ {basis basis' : Tactic.ComputeAsymptotics.Basis},
  List.Sublist basis basis' →
    Tactic.ComputeAsymptotics.WellFormedBasis basis' → Tactic.ComputeAsymptotics.WellFormedBasis basis
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_div_of_mul_eq : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, c ≠ 0 → a * c = b → a = b / c
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_le_of_forall_lt : ∀ {o a : Ordinal.{u}} {s : Set Ordinal.{u}}, a ∈ s → (∀ b < o, Ordinal.enumOrd s b < a) → Ordinal.enumOrd s o ≤ a
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm : ∀ {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} (self : D₁.Hom D₂)
  (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 (self.hom i₂))) =
    CategoryTheory.CategoryStruct.comp (self.hom i₁) (D₂.hom i₁ i₂)
-- Lean.Elab.WhereFinally
Lean.Elab.instInhabitedWhereFinallyView.default : Lean.Elab.WhereFinallyView
-- Mathlib.Data.Finset.Insert
/-- Split the added element of insert off a Pi type.  -/
Finset.insertPiProd : {α : Type u_1} →
  [inst : DecidableEq α] →
    {s : Finset α} → {a : α} → (f : α → Type u_3) → ((i : α) → i ∈ insert a s → f i) → f a × ((i : α) → i ∈ s → f i)
-- Aesop.Forward.SlotIndex
Aesop.instHashableSlotIndex : Hashable Aesop.SlotIndex
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.mk.injEq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A}
  (hom : (a : A) → F.functor a ⟶ G.functor a)
  (comm :
    autoParam
      (∀ (n a a' : A) (ha' : n + a = a'),
        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom a) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (hom a') (CategoryTheory.shiftFunctor D n))
            (G.shiftIso n a a' ha').hom)
      CategoryTheory.SingleFunctors.Hom.comm._autoParam)
  (hom_1 : (a : A) → F.functor a ⟶ G.functor a)
  (comm_1 :
    autoParam
      (∀ (n a a' : A) (ha' : n + a = a'),
        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom_1 a) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (hom_1 a') (CategoryTheory.shiftFunctor D n))
            (G.shiftIso n a a' ha').hom)
      CategoryTheory.SingleFunctors.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Lean.Elab.Tactic.Simp
/-- Add all definitions from the current file to unfold.  -/
Lean.Elab.Tactic.elabSimpLocals : Lean.Meta.SimpTheorems → Lean.Elab.Tactic.SimpKind → Lean.MetaM Lean.Meta.SimpTheorems
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P) (m : M),
  LinearMap.lTensor M f ∘ₗ (TensorProduct.mk R M N) m = (TensorProduct.mk R M P) m ∘ₗ f
-- Init.System.IO
/-- Inherit environment variables from the spawning process.  -/
IO.Process.SpawnArgs.inheritEnv : IO.Process.SpawnArgs → Bool
-- Init.Data.UInt.Bitwise
USize.and_comm : ∀ (a b : USize), a &&& b = b &&& a
-- Lean.Data.Lsp.Internal
/-- Converts `repr` to `RefIdent`.  -/
Lean.Lsp.RefIdent.fromJsonRepr : Lean.Lsp.RefIdent.RefIdentJsonRepr → Lean.Lsp.RefIdent
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_functor_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).functor.map f).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Convex.BetweenList
List.exists_map_eq_of_sorted_nonempty_iff_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {l : List P} (hl : l ≠ []),
  (∃ l', l'.SortedLE ∧ List.map (⇑(AffineMap.lineMap (l.head hl) (l.getLast hl))) l' = l) ↔ List.Wbtw R l
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = false ↔ ¬t = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.map f g) =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl
-- Mathlib.Algebra.GroupWithZero.Action.Basic
/-- Scalar multiplication as a monoid homomorphism with zero.  -/
smulMonoidWithZeroHom : {M₀ : Type u_5} →
  {N₀ : Type u_6} →
    [inst : MonoidWithZero M₀] →
      [inst_1 : MulZeroOneClass N₀] →
        [inst_2 : MulActionWithZero M₀ N₀] → [IsScalarTower M₀ N₀ N₀] → [SMulCommClass M₀ N₀ N₀] → M₀ × N₀ →*₀ N₀
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_eq_top : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S : Subsemiring R}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
tendsto_pow_div_pow_atTop_atTop : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : ℕ},
  q < p → Filter.Tendsto (fun x => x ^ p / x ^ q) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_inl_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : C} {c₁ c₂ : CategoryTheory.Limits.BinaryCofan A B}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂),
  CategoryTheory.Mono c₁.inl ↔ CategoryTheory.Mono c₂.inl
-- Init.Data.SInt.Float
/-- Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int32` (including `Inf`), returns the maximum
value of `Int32` (i.e. `Int32.maxValue`). If it is smaller than the minimum value for `Int32`
(including `-Inf`), returns the minimum value of `Int32` (i.e. `Int32.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float.toInt32 : Float → Int32
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_div_mul_left : ∀ {α : Type u} [inst : DivisionCommMonoid α] {c : α}, IsUnit c → ∀ (a b : α), c * a / (c * b) = a / b
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph0_le_beth : ∀ (o : Ordinal.{u_1}), Cardinal.aleph0 ≤ Cardinal.beth o
-- Mathlib.Combinatorics.Schnirelmann
le_schnirelmannDensity_iff : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {x : ℝ},
  x ≤ schnirelmannDensity A ↔ ∀ (n : ℕ), 0 < n → x ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n
-- Lean.Widget.InteractiveGoal
/-- Information about the term whose type is the term-mode goal.  -/
Lean.Widget.InteractiveTermGoal.term : Lean.Widget.InteractiveTermGoal → Lean.Server.WithRpcRef Lean.Elab.TermInfo
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv_left`. -/
Monovary.of_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f⁻¹ g → Antivary f g
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_smul : ∀ {n : Type u_3} {α : Type u_5} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] [inst_2 : DistribSMul α R]
  (r : α) (A : Matrix n n R), (r • A).trace = r • A.trace
-- Mathlib.Data.Set.Finite.Lattice
Set.finite_iUnion_of_subsingleton : ∀ {α : Type u} {ι : Sort u_1} [Subsingleton ι] {s : ι → Set α}, (⋃ i, s i).Finite ↔ ∀ (i : ι), (s i).Finite
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.aux_summable_sub : ∀ {k : ℕ}, 1 ≤ k → ∀ (x : ℂ), Summable fun n => (x - (↑n + 1)) ^ (-1 - ↑k)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.of_subsingleton : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal}, s.Subsingleton → Metric.IsSeparated ε s
-- Init.Data.Prod
Prod.exists : ∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∃ x, p x) ↔ ∃ a b, p (a, b)
-- Std.Data.HashMap.Lemmas
Std.HashMap.length_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.length = m.size
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_neg_right`. -/
Antivary.neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β}, Antivary f g → Monovary f (-g)
-- Mathlib.Condensed.Discrete.Characterization
CondensedSet.isDiscrete_tfae : ∀ (X : CondensedSet),
  [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (Condensed.discrete (Type (u + 1))).essImage X, CondensedSet.LocallyConstant.functor.essImage X,
      CategoryTheory.IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X),
      CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op))].TFAE
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given an type class instance type `instType`, returns true if free variables in input parameters
1- are not in `thmVars`, or
2- are in `fvarsFound`.
Remark: `fvarsFound` is a subset of `thmVars`
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.canBeSynthesized : Lean.FVarIdSet → Lean.FVarIdSet → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Setoid.Basic
/-- Given a map `f : N → M` and an equivalence relation `r` on `β`, the equivalence relation
induced on `α` by `f` equals the kernel of `r`'s quotient map composed with `f`.  -/
Setoid.comap_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {r : Setoid β}, Setoid.comap f r = Setoid.ker (Quotient.mk'' ∘ f)
-- Mathlib.Tactic.AdaptationNote
/-- `#adaptation_note /-- comment -/` adds an adaptation note to the current file.
Adaptation notes are comments that are used to indicate that a piece of code
has been changed to accommodate a change in Lean core.
They typically require further action/maintenance to be taken in the future.

This syntax works as a command, or inline in tactic or term mode.
 -/
«tactic#adaptation_note_» : Lean.ParserDescr
-- Batteries.Data.RunningStats
/-- Mean of data points.  -/
Batteries.RunningStats.mean : Batteries.RunningStats → Float
-- Lean.Compiler.IR.Format
Lean.IR.instToStringExpr : ToString Lean.IR.Expr
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.functionField_isFractionRing_of_affine : ∀ (R : CommRingCat) [inst : IsDomain ↑R], IsFractionRing ↑R ↑(AlgebraicGeometry.Spec R).functionField
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical.eq_1 : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a : M), UniqueFactorizationMonoid.radical a = (UniqueFactorizationMonoid.primeFactors a).prod id
-- Mathlib.Order.Fin.Basic
Fin.OrderEmbedding.default_def : ∀ {n : ℕ}, default = Fin.valOrderEmb n
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.weakEquivalence_homMk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] [inst_5 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : C}
  [inst_6 : HomotopicalAlgebra.IsCofibrant X] [inst_7 : HomotopicalAlgebra.IsFibrant X]
  [inst_8 : HomotopicalAlgebra.IsCofibrant Y] [inst_9 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.BifibrantObject.homMk f) ↔ HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.instIsPretransitiveObjFiniteObjFintypeCatOfIsConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] (G : Type u_1) [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X],
  MulAction.IsPretransitive G (F.obj X).obj