mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift_unique : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂)
  (Φ : CategoryTheory.Functor (CategoryTheory.Quotient r) D),
  (CategoryTheory.Quotient.functor r).comp Φ = F → Φ = CategoryTheory.Quotient.lift r F H
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_id : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R),
  NonUnitalSubsemiring.map (NonUnitalRingHom.id R) s = s
-- Mathlib.Order.Category.Semilat
SemilatSupCat.of.injEq : ∀ (X : Type u) [isSemilatticeSup : SemilatticeSup X] [isOrderBot : OrderBot X] (X_1 : Type u)
  (isSemilatticeSup_1 : SemilatticeSup X_1) (isOrderBot_1 : OrderBot X_1),
  ({ X := X, isSemilatticeSup := isSemilatticeSup, isOrderBot := isOrderBot } =
      { X := X_1, isSemilatticeSup := isSemilatticeSup_1, isOrderBot := isOrderBot_1 }) =
    (X = X_1 ∧ isSemilatticeSup ≍ isSemilatticeSup_1 ∧ isOrderBot ≍ isOrderBot_1)
-- Std.Http.Data.Chunk
/-- The extension name string.
 -/
Std.Http.Chunk.ExtensionName.value : Std.Http.Chunk.ExtensionName → String
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  (Std.DHashMap.Const.insertMany m l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.OplaxTrans.Modification η θ → CategoryTheory.Lax.OplaxTrans.Hom η θ
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.free_map : ∀ {X Y : Type u} (f : X ⟶ Y),
  AddCommGrpCat.free.map f = AddCommGrpCat.ofHom (FreeAbelianGroup.map ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Mathlib.Algebra.Group.Units.Basic
/-- A subsingleton `Monoid` has a unique unit.  -/
instUniqueUnitsOfSubsingleton : {M : Type u_1} → [inst : Monoid M] → [Subsingleton M] → Unique Mˣ
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.Context.mk.inj : ∀ {level₂ level₁ level₀ : Lean.Level} {B : Q(Type level₀)} {instBicategory : Q(CategoryTheory.Bicategory «$B»)}
  {level₂_1 level₁_1 level₀_1 : Lean.Level} {B_1 : Q(Type level₀_1)}
  {instBicategory_1 : Q(CategoryTheory.Bicategory «$B_1»)},
  { level₂ := level₂, level₁ := level₁, level₀ := level₀, B := B, instBicategory := instBicategory } =
      { level₂ := level₂_1, level₁ := level₁_1, level₀ := level₀_1, B := B_1, instBicategory := instBicategory_1 } →
    level₂ = level₂_1 ∧ level₁ = level₁_1 ∧ level₀ = level₀_1 ∧ B = B_1 ∧ instBicategory = instBicategory_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ofHom_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq) =
    CochainComplex.mappingCone.liftCochain φ (↑α) β ⋯
-- Mathlib.Data.Num.ZNum
PosNum.mod'_to_nat : ∀ (n d : PosNum), ↑(n.mod' d) = ↑n % ↑d
-- Mathlib.Data.ENat.BigOperators
/-- A product of finite numbers is still finite.  -/
ENat.prod_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, (∀ a ∈ s, f a ≠ ⊤) → ∏ a ∈ s, f a ≠ ⊤
-- Mathlib.Analysis.Calculus.TaylorIntegral
ContDiffAt.deriv_fderiv_add_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x y : E}
  {t : 𝕜} {n : ℕ},
  ContDiffAt 𝕜 (↑n + 1) f (x + t • y) →
    deriv (fun s => (iteratedFDeriv 𝕜 n f (x + s • y)) fun x => y) t =
      (iteratedFDeriv 𝕜 (n + 1) f (x + t • y)) fun x => y
-- Init.Data.SInt.Lemmas
Int32.toInt_toBitVec : ∀ (x : Int32), x.toBitVec.toInt = x.toInt
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.revMatchAt?_cast : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {startPos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? pat (startPos.cast hst) =
    Option.map (fun x => x.cast hst) (String.Slice.Pattern.Model.revMatchAt? pat startPos)
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- Induce the lawfulness of the monoidal structure along a faithful functor of (plain) categories,
where the operations are already defined on the destination type `D`.

The functor `F` must preserve all the data parts of the monoidal structure between the two
categories.
 -/
CategoryTheory.Monoidal.induced : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategoryStruct D] →
            (F : CategoryTheory.Functor D C) →
              [F.Faithful] → CategoryTheory.Monoidal.InducingFunctorData F → CategoryTheory.MonoidalCategory D
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_top : ∀ {V : Type u} {u v : V}, (SimpleGraph.completeGraph V).Reachable u v
-- Mathlib.Order.Filter.Basic
Filter.iSup_sets_eq : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α}, (iSup f).sets = ⋂ i, (f i).sets
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instCompleteDistribLattice : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → CompleteDistribLattice (π i)] → CompleteDistribLattice ((i : ι) → π i)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.monotoneOn_rpow_Ici_of_exponent_nonneg : ∀ {r : ℝ}, 0 ≤ r → MonotoneOn (fun x => x ^ r) (Set.Ici 0)
-- Mathlib.Topology.Separation.NotNormal
/-- Let `s` be a closed set in a separable space. If the induced topology on `s` is discrete and `s`
has cardinality at least continuum, then the ambient space is not a normal space.  -/
IsClosed.not_normal_of_continuum_le_mk : ∀ {X : Type u} [inst : TopologicalSpace X] [TopologicalSpace.SeparableSpace X] {s : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], Cardinal.continuum ≤ Cardinal.mk ↑s → ¬NormalSpace X
-- Mathlib.Topology.Maps.Strict.Basic
Topology.isStrictMap_iff_isQuotientMap_rangeFactorization : ∀ {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.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z), (e.transHomeomorph f').source = e.source
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.topEquiv_apply : ∀ {M : Type u_1} [inst : Mul M] (x : ↥⊤), Subsemigroup.topEquiv x = ↑x
-- Init.Control.Lawful.Instances
OptionT.pure.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α), OptionT.pure a = OptionT.mk (pure (some a))
-- Std.Http.Data.Request
Std.Http.Request.mk.inj : ∀ {t : Type} {line : Std.Http.Request.Head} {body : t} {extensions : Std.Http.Extensions}
  {line_1 : Std.Http.Request.Head} {body_1 : t} {extensions_1 : Std.Http.Extensions},
  { line := line, body := body, extensions := extensions } =
      { line := line_1, body := body_1, extensions := extensions_1 } →
    line = line_1 ∧ body = body_1 ∧ extensions = extensions_1
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.instIsPretransitiveProjGenLinGroupFinOfNatNatReal : MulAction.IsPretransitive (Matrix.ProjGenLinGroup (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : LocallyCompactSpace X] [inst_6 : LocallyCompactSpace Y] (f : C(X × Y, R)),
  ((AbstractMeasure.prodMk μ) ν) f = ν ((AbstractMeasure.contractFst μ) f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).getKey! a = default
-- Mathlib.Order.Defs.LinearOrder
_private.Mathlib.Order.Defs.LinearOrder.0.Ordering.Compares.match_1.eq_1 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.lt, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_1 a b
-- Mathlib.Order.Filter.Basic
Filter.compl_notMem : ∀ {α : Type u} {f : Filter α} {s : Set α} [f.NeBot], s ∈ f → sᶜ ∉ f
-- Init.Data.Bool
Bool.if_false_right : ∀ (p : Prop) [h : Decidable p] (t : Bool), (if p then t else false) = (decide p && t)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Lean.Meta.Instances
Lean.Meta.PrioritySet : Type
-- Std.Http.Data.Body.Full
/-- Creates a `Full` body from a `ByteArray`.
 -/
Std.Http.Body.Full.ofByteArray : ByteArray → Std.Async.Async Std.Http.Body.Full
-- Mathlib.Tactic.CategoryTheory.Monoidal.Basic
/-- Use the coherence theorem for monoidal categories to solve equations in a monoidal category,
where the two sides only differ by replacing strings of monoidal structural morphisms
(that is, associators, unitors, and identities)
with different strings of structural morphisms with the same source and target.

That is, `monoidal` can handle goals of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `monoidal_coherence`.
 -/
Mathlib.Tactic.Monoidal.tacticMonoidal : Lean.ParserDescr
-- Mathlib.Order.Preorder.Chain
/-- A chain in a partial order is a linear order.  -/
IsChain.linearOrder : {α : Type u_1} →
  [inst : PartialOrder α] → [DecidableLE α] → {s : Set α} → IsChain (fun x1 x2 => x1 ≤ x2) s → LinearOrder ↑s
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.symm_mk : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃+* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)),
  { toRingEquiv := e, map_star' := h₁ }.symm = { toRingEquiv := e.symm, map_star' := ⋯ }
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.toOpenPartialHomeomorph.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f f_1 : E → F)
  (e_f : f = f_1) {f' f'_1 : E ≃L[𝕜] F} (e_f' : f' = f'_1) {a a_1 : E} (e_a : a = a_1) [inst_5 : CompleteSpace E]
  (hf : HasStrictFDerivAt f (↑f') a),
  HasStrictFDerivAt.toOpenPartialHomeomorph f hf = HasStrictFDerivAt.toOpenPartialHomeomorph f_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.abelianImageToKernel
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι S.f) h
-- Lean.Elab.AssertExists
/-- `addAssertExistsEntry isDecl declName mod` extends the `AssertExists` environment extension
with the data `isDecl, declName, mod`.
This information is used to capture declarations and modules that are forbidden from
existing/being imported at some point, but should eventually exist/be imported.
 -/
Lean.Elab.Command.addAssertExistsEntry : Bool → Lean.Name → Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The image of a `Submonoid` along a `MonoidHom` is a `Submonoid`.  -/
Submonoid.map : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : MonoidHomClass F M N] → F → Submonoid M → Submonoid N
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Meta.TryThis
/-- Get the input width specified in the options  -/
Lean.Meta.Tactic.TryThis.getInputWidth : Lean.Options → ℕ
-- Init.Data.String.PosRaw
String.instDecidableLeRaw : (p₁ p₂ : String.Pos.Raw) → Decidable (p₁ ≤ p₂)
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.full_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.MonoOver.map f).Full
-- Mathlib.Data.NNReal.Defs
NNReal.instLinearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero NNReal
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.insertAtCollisionNodeAux : {α : Type u_1} →
  {β : Type u_2} →
    [BEq α] → Lean.PersistentHashMap.CollisionNode α β → ℕ → α → β → Lean.PersistentHashMap.CollisionNode α β
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] [inst_4 : HasDerivedCategory C]
  [inst_5 : HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] {Z : DerivedCategory D}
  (h :
    (CategoryTheory.shiftFunctor (DerivedCategory D) 1).obj ((DerivedCategory.singleFunctor D 0).obj (F.obj S.X₁)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁))
          h)) =
    CategoryTheory.CategoryStruct.comp ⋯.singleδ h
-- Std.Internal.Parsec.Basic
/-- Fails if `p` succeeds, otherwise succeeds without consuming input.
 -/
Std.Internal.Parsec.notFollowedBy : {α ι : Type} → Std.Internal.Parsec ι α → Std.Internal.Parsec ι Unit
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instIsEmpty : ∀ {α : Type u_1} [inst : LE α] [IsEmpty α], IsEmpty (NonemptyInterval α)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.singleton_inj : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α}, {x} = {y} ↔ x = y
-- Init.Prelude
/-- A hash function for names, which is stored inside the name itself as a
computed field.  -/
Lean.Name.hash : Lean.Name → UInt64
-- Mathlib.Order.SupIndep
iSupIndep_def' : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.mk_desc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (s : CategoryTheory.Limits.Cofan f)
  (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j)
      CategoryTheory.Limits.Cofan.IsColimit.mk._auto_1)
  (uniq :
    autoParam
      (∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt ⟶ t.pt),
        (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t)
      CategoryTheory.Limits.Cofan.IsColimit.mk._auto_3)
  (t : CategoryTheory.Limits.Cofan f), (CategoryTheory.Limits.Cofan.IsColimit.mk s desc fac uniq).desc t = desc t
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.comp_reflectsFiniteProducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsFiniteProducts F]
  [CategoryTheory.Limits.ReflectsFiniteProducts G], CategoryTheory.Limits.ReflectsFiniteProducts (F.comp G)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.ι_colimitIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G] (X : C) {Z : E}
  (h : CategoryTheory.Limits.colimit (F.comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Final.colimitIso F G).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X) h
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.of_isOpenCover : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U →
    (∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s)) → Topology.IsLocallyConstructible s
-- Mathlib.Data.PNat.Xgcd
/-- We will apply the above step recursively.  The following result
is used to ensure that the process terminates.  -/
PNat.XgcdType.step_wf : ∀ (u : PNat.XgcdType), u.r ≠ 0 → sizeOf u.step < sizeOf u
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- The additivity of a functor, as a property of objects in `C ⥤ D`.  -/
CategoryTheory.additiveFunctor : (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] →
        [CategoryTheory.Preadditive C] →
          [CategoryTheory.Preadditive D] → CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.Barrier.lock : Std.Barrier → Std.Mutex Std.BarrierState✝
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [IsDomain S] {φ : R →+* S},
  Function.Injective ⇑φ → ∀ {f : Polynomial R}, f.IsPrimitive → (IsUnit f ↔ IsUnit (Polynomial.map φ f))
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_tsum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Type u_4} {f : ι → α → ENNReal},
  (∀ (i : ι), LowerSemicontinuousOn (f i) s) → LowerSemicontinuousOn (fun x' => ∑' (i : ι), f i x') s
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.forget₂_map_ofHom : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Group Y] (f : X →* Y),
  (CategoryTheory.forget₂ GrpCat MonCat).map (GrpCat.ofHom f) = MonCat.ofHom f
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_inverse : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀}, IsUnit a → Ring.inverse (Ring.inverse a) = a
-- Mathlib.Lean.MessageData.ForExprs
/-- A wrapper structure for `MessageData` to enable `for (ppCtx, e) in msg.exprs do` notation.  -/
Lean.MessageData.Exprs : Type
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : AddCommMonoid S]
  (p : SkewMonoidAlgebra k G) (f g : G → k → S), (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_x : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt = X
-- Init.Data.List.SplitOn.Lemmas
List.splitOn_ne_nil : ∀ {α : Type u_1} [inst : BEq α] (a : α) (xs : List α), List.splitOn a xs ≠ []
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.hoFunctor.instIsLeftAdjointSSetCatHoFunctor : SSet.hoFunctor.IsLeftAdjoint
-- Init.Data.Array.Subarray
/-- Tests each element in a subarray with a Boolean predicate in reverse order, stopping at the first
element that satisfies the predicate. The element that satisfies the predicate is returned, or
`none` if no element satisfies the predicate.

Examples:
 * `#["red", "green", "blue"].toSubarray.findRev? (·.length ≠ 4) = some "green"`
 * `#["red", "green", "blue"].toSubarray.findRev? (fun _ => true) = some "blue"`
 * `#["red", "green", "blue"].toSubarray 0 0 |>.findRev? (fun _ => true) = none`
 -/
Subarray.findRev? : {α : Type} → Subarray α → (α → Bool) → Option α
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.not_inseparable_infty_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, ¬Inseparable OnePoint.infty ↑x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_toReal : ∀ {θ : Real.Angle}, θ ≠ ↑Real.pi → SignType.sign θ.toReal = θ.sign
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_induction : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {p : (x : A) → x ∈ Algebra.adjoin R s → Prop},
  (∀ (x : A) (hx : x ∈ s), p x ⋯) →
    (∀ (r : R), p ((algebraMap R A) r) ⋯) →
      (∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) →
          ∀ {x : A} (hx : x ∈ Algebra.adjoin R s), p x hx
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_pos_of_lt' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, 0 < a → b < c → b < a + c
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.preimage_of_equiv : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group H]
  [inst_2 : MulAction G α] [inst_3 : MeasurableSpace α] [inst_4 : MulAction H β] [inst_5 : MeasurableSpace β]
  {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β},
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ {f : β → α},
      MeasureTheory.Measure.QuasiMeasurePreserving f ν μ →
        ∀ {e : G → H},
          Function.Bijective e →
            (∀ (g : G), Function.Semiconj f (fun x => e g • x) fun x => g • x) →
              MeasureTheory.IsFundamentalDomain H (f ⁻¹' s) ν