mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.PullbackCone.combine_pt_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H)
  (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X))
  (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) (X : D),
  (CategoryTheory.Limits.PullbackCone.combine f g c hc).pt.obj X = (c X).pt
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [h : MeasurableSpace.CountablySeparated ↑s],
  HasCountableSeparatingOn α MeasurableSet s
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubOfPoint_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (v : V),
  (s.weightedVSubOfPoint (v +ᵥ p) b) w = (s.weightedVSubOfPoint p (-v +ᵥ b)) w
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)] (X : D),
  adj.toEquivalence.counitIso.hom.app X = adj.counit.app X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerLeft_comp_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ φ' φ'' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') (θ' : φ' ⟶ φ'')
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ.comp φ'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.comp θ θ')) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ') h)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_eq_one_iff₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → (μ sᶜ = 1 ↔ μ s = 0)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_revSkipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos} {h : pos.revSkipWhile P ≠ s.startPos},
  ¬P (((pos.revSkipWhile P).prev h).get ⋯)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The additive subsemigroup of elements `x : M` such that `f x = g x`  -/
AddHom.eqLocus : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → (M →ₙ+ N) → AddSubsemigroup M
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.pushNot : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fstₗ_comp_inlₗ : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], (OrderAddMonoidHom.fstₗ α β).comp (OrderAddMonoidHom.inlₗ α β) = OrderAddMonoidHom.id α
-- Mathlib.Topology.Connected.Basic
Function.Surjective.connectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [ConnectedSpace α] [inst_2 : TopologicalSpace β] {f : α → β},
  Function.Surjective f → Continuous f → ConnectedSpace β
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_toPartialEquiv : ∀ {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) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').toPartialEquiv = e.trans e'.toPartialEquiv
-- Mathlib.CategoryTheory.Shift.Basic
/-- shifting an object `X` by `n` is obtained by the notation `X⟦n⟧`  -/
CategoryTheory.«term_⟦_⟧» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Meromorphic.Order
/-- Helper lemma for `meromorphicOrderAt_add_of_ne`.
 -/
meromorphicOrderAt_add_eq_right_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f₁ x →
    meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x → meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₂ x
-- Mathlib.CategoryTheory.Preadditive.LeftExact
CategoryTheory.Limits.parallelPair.eqOfHomEq.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y} (hf : f = f') (hg : g = g'),
  CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg = CategoryTheory.Limits.parallelPair.eqOfHomEq hf hg
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The addition of two nonsingular Jacobian points on a Weierstrass curve `W`.

Given two nonsingular Jacobian points `P` and `Q` on `W`, use `P + Q` instead of `add P Q`.  -/
WeierstrassCurve.Jacobian.Point.add : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → W.Point → W.Point → W.Point
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.partialOrder : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} →
      [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → PartialOrder { P // IsLprojection X P }
-- Mathlib.Topology.NhdsKer
mem_nhdsKer_singleton : ∀ {X : Type u_2} [inst : TopologicalSpace X] {x y : X}, x ∈ nhdsKer {y} ↔ x ⤳ y
-- Mathlib.Topology.Constructions.SumProd
Continuous.prodMk_right : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X),
  Continuous fun y => (x, y)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for strict monotonicity of multiplication by positive elements on the right,
namely `a₁ < a₂ → a₁ * b < a₂ * b` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
MulPosStrictMono : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.characteristic_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic],
  (AddSubgroup.centralizer ↑H).Characteristic
-- Mathlib.Algebra.GCDMonoid.Nat
gcd_eq_nat_gcd : ∀ (m n : ℕ), gcd m n = m.gcd n
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ.injEq : ∀ {n : Q(ℕ)} (n' : Q(ℕ)) (pf : «$n» =Q «$n'».succ) (n'_1 : Q(ℕ)) (pf_1 : «$n» =Q «$n'_1».succ),
  (Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n' pf = Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n'_1 pf_1) =
    (n' = n'_1)
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
FiberBundle.trivializationAt_continuousAlternatingMap_baseSet : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (x₀ : B),
  (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀).baseSet =
    (trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet
-- Lean.Expr
Lean.FVarIdSet.insert : Lean.FVarIdSet → Lean.FVarId → Lean.FVarIdSet
-- Mathlib.Data.Set.Image
Subtype.image_preimage_coe : ∀ {α : Type u_1} (s t : Set α), Subtype.val '' Subtype.val ⁻¹' t = s ∩ t
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.lift_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : D ⟶ (CategoryTheory.Functor.const J).obj X) (j : J),
  (CategoryTheory.Over.lift D s).obj j = CategoryTheory.Over.mk (s.app j)
-- Init.Notation
/-- `a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`. -/
«term_•_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R], Lagrange.nodal s v ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the left type  -/
CategoryTheory.Limits.MultispanShape.L : CategoryTheory.Limits.MultispanShape → Type w
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.Const.get? (m₁.union! m₂) k =
          (Std.DTreeMap.Internal.Impl.Const.get? m₂ k).or (Std.DTreeMap.Internal.Impl.Const.get? m₁ k)
-- Mathlib.RingTheory.Extension.Generators
/-- Extend generators by more variables.  -/
Algebra.Generators.extend : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {ι' : Type u_1} → Algebra.Generators R S ι → (ι' → S) → Algebra.Generators R S (ι ⊕ ι')
-- Lean.CoreM
Lean.compileDecl : Lean.Declaration → optParam Bool true → Lean.CoreM Unit
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_one_self : ∀ {m : Type u_2} {α : Type u_12} [inst : DecidableEq m] [inst_1 : Zero α] [inst_2 : One α] (p : m → Prop),
  Matrix.toBlock 1 p p = 1
-- Mathlib.Data.Set.Image
Set.disjoint_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ {s t : Set α}, Disjoint s t → Disjoint (f '' s) (f '' t)
-- Mathlib.Algebra.MvPolynomial.Monad
/-- `bind₁` is the "left-hand side" bind operation on `MvPolynomial`, operating on the variable type.
Given a polynomial `p : MvPolynomial σ R` and a map `f : σ → MvPolynomial τ R` taking variables
in `p` to polynomials in the variable type `τ`, `bind₁ f p` replaces each variable in `p` with
its value under `f`, producing a new polynomial in `τ`. The coefficient type remains the same.
This operation is an algebra hom.
 -/
MvPolynomial.bind₁ : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_3} → [inst : CommSemiring R] → (σ → MvPolynomial τ R) → MvPolynomial σ R →ₐ[R] MvPolynomial τ R
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.withComputedSize.eq_1 : ∀ {α : Type u} {β : α → Type v} (self : Array (Std.DHashMap.Internal.AssocList α β)),
  Std.DHashMap.Internal.withComputedSize self = { size := Std.DHashMap.Internal.computeSize self, buckets := self }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Inv_insert : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (expr : Std.Tactic.BVDecide.BVExpr w) (refs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    (∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get idx hidx }⟧ =
          (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx) →
      Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig (cache.insert expr refs)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranCounit_app_app_ranAdjunction_unit_app_app_assoc : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H) (X : C)
  {Z : H} (h : G.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X))
      (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app (L.comp G)).app X) h) =
    h
-- Mathlib.GroupTheory.CoprodI
/-- Each element of the free product corresponds to a unique reduced word.  -/
Monoid.CoprodI.Word.equiv : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → Monoid.CoprodI M ≃ Monoid.CoprodI.Word M
-- Init.Data.Array.Lemmas
Array.replace_push : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : Array α} {a b c : α},
  (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if (b == a) = true then c else a)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn G g l s → TendstoLocallyUniformlyOn (F / G) (f / g) l s
-- Mathlib.Analysis.Convex.Between
sbtw_iff_left_ne_and_right_mem_image_Ioi : ∀ {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] {x y z : P},
  Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.self_comp_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), ⇑h ∘ ⇑h.symm = id
-- Mathlib.Order.TypeTags
WithTop.coe.eq_1 : ∀ {α : Type u_1}, WithTop.coe = { coe := WithTop.some }
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_add_le' : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (p : ENNReal),
        MeasureTheory.eLpNorm (f + g) p μ ≤ p.LpAddConst * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_le_iff : ∀ {u : ℕ → EReal} {a : EReal}, LinearGrowth.linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * ↑n
-- Mathlib.Topology.Bornology.Basic
Bornology.ext : ∀ {α : Type u_2} (t t' : Bornology α), Bornology.cobounded α = Bornology.cobounded α → t = t'
-- Mathlib.Topology.UniformSpace.Basic
inf_uniformity : ∀ {α : Type ua} {u v : UniformSpace α}, uniformity α = uniformity α ⊓ uniformity α
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Given a cocontinuous functor `F : C ⥤ D` between sites `(C, J)` and `(D, K)`,
`P` a presheaf on `D`, this is the (colimit) cocone which expresses
`(Φ.map F K).presheafFiber.obj P` as a colimit of `P.obj (op (F.obj X))`
for `X : C`, `x : Φ.fiber.obj X`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [F.IsCocontinuous J K] →
                  [CategoryTheory.LocallySmall.{w, v', u'} D] →
                    {A : Type u''} →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Dᵒᵖ A) →
                            CategoryTheory.Limits.Cocone
                              ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp (F.op.comp P))
-- Mathlib.Data.Ordmap.Ordset
Ordnode.mem.congr_simp : ∀ {α : Type u_1} [inst : LE α] {inst_1 : DecidableLE α} [inst_2 : DecidableLE α] (x x_1 : α),
  x = x_1 → ∀ (a a_1 : Ordnode α), a = a_1 → Ordnode.mem x a = Ordnode.mem x_1 a_1
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of an endomorphism independent of basis.

If there is no finite basis on `M`, the result is `1` instead.
 -/
LinearMap.det : {M : Type u_7} →
  [inst : AddCommGroup M] → {A : Type u_8} → [inst_1 : CommRing A] → [inst_2 : Module A M] → (M →ₗ[A] M) →* A
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.isoMk_toNatIso : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G),
  CategoryTheory.Cat.Hom.isoMk (CategoryTheory.Cat.Hom.toNatIso e) = e
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fmod.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (m = 0 → False) →
    (match Int.ofNat m, Int.ofNat n with
      | 0, x => h_1 x
      | Int.ofNat m, Int.ofNat n => h_2 m n
      | Int.ofNat m.succ, Int.negSucc n => h_3 m n
      | Int.negSucc m, Int.ofNat n => h_4 m n
      | Int.negSucc m, Int.negSucc n => h_5 m n) =
      h_2 m n
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.values.go : {α : Type} → Lean.Data.Trie α → StateM (Array α) Unit
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Construct a bundled `Grpd` from the underlying type and the typeclass `Groupoid`.  -/
CategoryTheory.Grpd.of : (C : Type u) → [CategoryTheory.Groupoid C] → CategoryTheory.Grpd
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_const : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (a : α),
  (s.sup' H fun x => a) = a
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.comp_app : ∀ {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C),
  (CategoryTheory.CategoryStruct.comp α β).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp (α.toNatTrans.app X) (β.toNatTrans.app X)
-- Lean.Server.References
Lean.Server.References.DocumentRefInfo.mk.inj : ∀ {location : Lean.Lsp.Location} {module : Lean.Name} {parentInfo? : Option Lean.Server.References.ParentDecl}
  {location_1 : Lean.Lsp.Location} {module_1 : Lean.Name} {parentInfo?_1 : Option Lean.Server.References.ParentDecl},
  { location := location, module := module, parentInfo? := parentInfo? } =
      { location := location_1, module := module_1, parentInfo? := parentInfo?_1 } →
    location = location_1 ∧ module = module_1 ∧ parentInfo? = parentInfo?_1
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.hurwitzZeta.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.hurwitzZeta a s = HurwitzZeta.hurwitzZetaEven a s + HurwitzZeta.hurwitzZetaOdd a s
-- Mathlib.Order.Category.LinOrd
LinOrd.forget_map : ∀ {X Y : LinOrd} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget LinOrd).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto_of_frequently : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : β → α}
  {a b : α} {x : Filter β}, Filter.Tendsto f x (nhds a) → (∃ᶠ (c : β) in x, f c ≤ b) → a ≤ b
-- Mathlib.Order.CompleteLattice.Defs
sInf_le_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux.eq_2 : ∀ {l w : ℕ} (x : BitVec (l * w)) (acc : BitVec w) (s_1 : ℕ),
  BitVec.addRecAux✝ x s_1.succ acc = BitVec.addRecAux✝ x s_1 (acc + BitVec.extractLsb' (s_1 * w) w x)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
/-- Sign of the first non-zero exponent of a unit monomial.  -/
Tactic.ComputeAsymptotics.UnitMonomial.sign : Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.UnitMonomial.Sign
-- Mathlib.Order.Hom.Basic
OrderIso.ofRelIsoLT_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  (e : (fun x1 x2 => x1 < x2) ≃r fun x1 x2 => x1 < x2) (x : α), (OrderIso.ofRelIsoLT e) x = e x
-- Mathlib.Order.Interval.Set.Image
StrictAnti.mapsTo_Ioi : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictAnti f → Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} [inst_1 : SizeOf C]
  (toNatTrans : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor)
  (app_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam)
  (app_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X))) (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam),
  sizeOf { toNatTrans := toNatTrans, app_η := app_η, app_μ := app_μ } = 1 + sizeOf toNatTrans
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.of_mulHom : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
  (∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d) → ∀ [UniqueProds G], UniqueProds H
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of the 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Atom₁.tgt : Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupCohomology.cocycles₁ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 1)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ) h)