mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂ : ∀ (X : CategoryTheory.Cat), (CategoryTheory.Nerve.nerveFunctor₂.obj X).IsStrictSegal
-- Mathlib.Topology.Basic
isClosed_iInter : ∀ {X : Type u} {ι : Sort v} [inst : TopologicalSpace X] {f : ι → Set X},
  (∀ (i : ι), IsClosed (f i)) → IsClosed (⋂ i, f i)
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.ring : {I : Type u_5} → {B : I → Type u_6} → [inst : (i : I) → NormedRing (B i)] → Ring (PreLp B)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.toTake.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Std.Iterators.Finite α m]
  (it it_1 : Std.IterM m β), it = it_1 → it.toTake = it_1.toTake
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_if : ∀ {n : ℕ}, (*...n).toArray = if 0 < n then (*...n - 1).toArray.push (n - 1) else #[]
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.Hom.ext : ∀ {X Y : TopCat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `a : X → A` is continuous at `x₀`, and
eventually `a x` satisfies the predicate `p` associated to `𝕜` and has spectrum contained in `s`,
then `fun x ↦ cfc f (a x)` is continuous at `x₀`.  -/
ContinuousAt.cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X},
      ContinuousAt a x₀ →
        (∀ᶠ (x : X) in nhds x₀, spectrum 𝕜 (a x) ⊆ s) →
          (∀ᶠ (x : X) in nhds x₀, p (a x)) →
            autoParam (ContinuousOn f s) ContinuousAt.cfc._auto_1 → ContinuousAt (fun x => cfc f (a x)) x₀
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.congrDefault : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Aesop.Frontend.Attribute
Aesop.Frontend.Parser.«attr_rules[_]» : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_mapWithPostcondition : ∀ {m : Type w → Type w'} {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.mapWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let c ← liftM (f b).run
        g d c)
      init it
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.sub_singleton_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  spectrum R a - {r} = spectrum R (a - (algebraMap R A) r)
-- Mathlib.Data.List.MinMax
List.minimum_of_length_pos_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {b : α} (h : 0 < l.length),
  List.minimum_of_length_pos h ≤ b ↔ l.minimum ≤ ↑b
-- Init.SimpLemmas
Or.imp_right : ∀ {b c a : Prop}, (b → c) → a ∨ b → a ∨ c
-- Mathlib.GroupTheory.Focal
Subgroup.map_focalSubgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Subgroup.map H.subtype H.focalSubgroupOf = H.focalSubgroup
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
hasDerivAt_of_tendstoUniformlyOnFilter : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g : 𝕜 → G} {f' : ι → 𝕜 → G} {g' : 𝕜 → G}
  {x : 𝕜} [IsRCLikeNormedField 𝕜] [l.NeBot],
  TendstoUniformlyOnFilter f' g' l (nhds x) →
    (∀ᶠ (n : ι × 𝕜) in l ×ˢ nhds x, HasDerivAt (f n.1) (f' n.1 n.2) n.2) →
      (∀ᶠ (y : 𝕜) in nhds x, Filter.Tendsto (fun n => f n y) l (nhds (g y))) → HasDerivAt g (g' x) x
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_pi : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {X : ι → Type u_6}
  [inst_1 : (i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) → X i} {s : Set α} {x : α},
  ContinuousWithinAt f s x ↔ ∀ (i : ι), ContinuousWithinAt (fun y => f y i) s x
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.subtype_val_preimage : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {C : SubMulAction G X},
  MulAction.IsBlock G B → MulAction.IsBlock G (Subtype.val ⁻¹' B)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The Dirichlet character mod `1` corresponds to the constant function `1`.  -/
DirichletCharacter.modOne_eq_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {χ : DirichletCharacter R 1}, (fun x => χ ↑x) = 1
-- Mathlib.MeasureTheory.Group.Arithmetic
IsUnit.measurable_const_smul_iff : ∀ {M : Type u_4} {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  [inst_2 : Monoid M] [inst_3 : MulAction M β] [MeasurableConstSMul M β] {c : M},
  IsUnit c → ((Measurable fun x => c • f x) ↔ Measurable f)
-- Mathlib.Data.List.Duplicate
List.not_duplicate_nil : ∀ {α : Type u_1} (x : α), ¬List.Duplicate x []
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_inter : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s t : Set α), Finsupp.supported M R (s ∩ t) = Finsupp.supported M R s ⊓ Finsupp.supported M R t
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd : {α : Type} → Lean.Meta.Grind.Arith.CommRing.RingM α → Lean.Meta.Grind.Arith.CommRing.RingM α
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps.msg : ProofWidgets.InteractiveMessageProps → Lean.Server.WithRpcRef Lean.MessageData
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive ↔ (↑T).IsSymmetric ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x
-- Lean.Elab.PreDefinition.WF.PackMutual
/-- Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker`
module.
 -/
Lean.Elab.WF.packMutual : Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Array Lean.Elab.PreDefinition → Lean.MetaM Lean.Elab.PreDefinition
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- If `M` multiplicatively acts on `α`, then `DomMulAct M` acts on `α → β` as well as some
bundled maps from `α`. This is a type synonym for `MulOpposite M`, so this corresponds to a right
action of `M`.  -/
DomMulAct : Type u_1 → Type u_1
-- Lean.ProjFns
/-- `true` if the child structure is a class.  -/
Lean.AuxParentProjectionInfo.fromClass : Lean.AuxParentProjectionInfo → Bool
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` is a right cancel semigroup if `β` is a
right cancel semigroup.  -/
FunLike.rightCancelSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] → [inst_2 : RightCancelSemigroup β] → [IsMulApply F α β] → RightCancelSemigroup F
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasEqualizer_precomp_of_hasEqualizer : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g]
  [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.equalizer.ι f g) h],
  CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The intersection of `Uᵢ ×[Z] Y` and `Uⱼ ×[Z] Y` is given by (Uᵢ ×[Z] Y) ×[X] Uⱼ  -/
AlgebraicGeometry.Scheme.Pullback.v : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          𝒰.I₀ → 𝒰.I₀ → AlgebraicGeometry.Scheme
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mker_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mker (AddMonoid.Coprod.swap M N) = ⊥
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasFDerivWithinAt.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {s : Set E}
  {x : E},
  HasFDerivWithinAt f f' s x →
    f x ∈ Complex.slitPlane → HasFDerivWithinAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') s x
-- Mathlib.Analysis.Normed.Module.Bases
/-- The sequence of the constructed basis corresponds to the input data `D.e`.  -/
SchauderBasis.RankOneDecomposition.basis_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (D : SchauderBasis.RankOneDecomposition 𝕜 X), ↑D.basis = D.e
-- Mathlib.RingTheory.RingHom.OpenImmersion
/-- A standard open immersion is one that is a localization map away from some element.  -/
RingHom.IsStandardOpenImmersion : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.coeff_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f pf s x r → ∀ (v : Fin 0 → E), (pf 0) v = f x
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_empty_right : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s : Finset α), G.edgeDensity s ∅ = 0
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K]
  {F : CategoryTheory.Functor K C}
  [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj],
  CategoryTheory.Limits.PreservesColimit F J.yoneda
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.IsGalois.toIsConnected : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C} {X : C}
  [self : CategoryTheory.PreGaloisCategory.IsGalois X], CategoryTheory.PreGaloisCategory.IsConnected X
-- Mathlib.GroupTheory.QuotientGroup.Basic
AddSubgroup.Characteristic.comap_quotient_mk : ∀ {G : Type u} [inst : AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic] {K : AddSubgroup (G ⧸ H)},
  K.Characteristic → (AddSubgroup.comap (QuotientAddGroup.mk' H) K).Characteristic
-- Mathlib.RingTheory.Ideal.Maps
RingEquiv.map_primeCompl_comap_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S) (p : Ideal S) [inst_2 : p.IsPrime],
  Submonoid.map e (Ideal.comap e p).primeCompl = p.primeCompl
-- Aesop.Stats.Basic
Aesop.RuleStats.mk.sizeOf_spec : ∀ (rule : Aesop.DisplayRuleName) (elapsed : Aesop.Nanos) (successful : Bool),
  sizeOf { rule := rule, elapsed := elapsed, successful := successful } =
    1 + sizeOf rule + sizeOf elapsed + sizeOf successful
-- Mathlib.Topology.JacobsonSpace
instJacobsonSpaceOfT1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], JacobsonSpace X
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.hasStrictFDerivAt : ∀ {𝕜 : 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 : E →ᴬ[𝕜] F)
  {x : E}, HasStrictFDerivAt (⇑f) f.contLinear x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by the sup norm of the iterated derivatives.
In the scope `Distributions.Seminorm`, we denote them by `N[𝕜; F]_{K, n, i}`
(or `N[𝕜]_{K, n, i}`), or simply by `N[𝕜; F]_{K, i}` (or `N[𝕜; F]_{K, i}`) when `n = ∞`.  -/
ContDiffMapSupportedIn.seminorm : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n : ℕ∞) → (K : TopologicalSpace.Compacts E) → ℕ → Seminorm 𝕜 (ContDiffMapSupportedIn E F n K)
-- Mathlib.Data.List.Triplewise
List.Triplewise.map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {p : α → α → α → Prop} {f : α → β} {p' : β → β → β → Prop},
  (∀ {a b c : α}, p a b c → p' (f a) (f b) (f c)) → List.Triplewise p l → List.Triplewise p' (List.map f l)
-- Init.Data.Array.Basic
/-- Creates an array that contains `n` repetitions of `v`.

The corresponding `List` function is `List.replicate`.

Examples:
* `Array.replicate 2 true = #[true, true]`
* `Array.replicate 3 () = #[(), (), ()]`
* `Array.replicate 0 "anything" = #[]`
 -/
Array.replicate : {α : Type u} → ℕ → α → Array α
-- Mathlib.CategoryTheory.Endomorphism
/-- Endomorphisms of an object form a monoid  -/
CategoryTheory.End.monoid : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → Monoid (CategoryTheory.End X)
-- Mathlib.Data.Seq.Defs
/-- Bisimilarity relation over `Option` of `Seq1 α`  -/
Stream'.Seq.BisimO : {α : Type u} → (Stream'.Seq α → Stream'.Seq α → Prop) → Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Prop
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.setCurr.match_1.splitter : (motive : String.Legacy.Iterator → Char → Sort u_1) →
  (x : String.Legacy.Iterator) →
    (x_1 : Char) → ((s : String) → (i : String.Pos.Raw) → (c : Char) → motive { s := s, i := i } c) → motive x x_1
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.measurable_resolvent : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace 𝕜] {a : A}
  [OpensMeasurableSpace 𝕜] [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] [CompleteSpace A]
  [inst_6 : MeasurableSpace A] [BorelSpace A], Measurable (resolvent a)
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Assume that a measure `μ` is `IsAddLeftInvariant`, that the action of `Γ` on `G` has a
measurable fundamental domain `s` with positive finite volume, and that there is a single measurable
set `V ⊆ G ⧸ Γ` along which the pullback of `μ` and `ν` agree (so the scaling is right). Then
`μ` satisfies `AddQuotientMeasureEqMeasurePreimage`. The main tool of the proof is the uniqueness of
left invariant measures, if normalized by a single positive finite-measured set.  -/
MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsAddLeftInvariant] [Countable ↥Γ] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsAddLeftInvariant]
  [MeasureTheory.SigmaFinite μ] {s : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) s ν →
    ∀ {V : Set (G ⧸ Γ)},
      MeasurableSet V →
        μ V ≠ 0 →
          μ V = ν (QuotientAddGroup.mk ⁻¹' V ∩ s) → μ V ≠ ⊤ → MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
-- Init.Data.Vector.MapIdx
_private.Init.Data.Vector.MapIdx.0.Vector.toArray_mapFinIdxM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {f : (i : ℕ) → α → i < n → m β} (i j : ℕ) (inv : i + j = n) (bs : Vector β (n - i)),
  Vector.toArray <$> Vector.mapFinIdxM.map xs f i j inv bs =
    Array.mapFinIdxM.map xs.toArray (fun i x h => f i x ⋯) i j ⋯ bs.toArray
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimit'_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I Cᵒᵖ) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.leftOp.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.leftOp.comp CategoryTheory.yoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitYonedaHomIsoLimit' D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (D.obj i)))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.leftOp.comp CategoryTheory.yoneda) (Opposite.op i)).app (D.obj i)))
            (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }
-- Mathlib.Order.DirectedInverseSystem
/-- For a family of types `X` indexed by a preorder `ι` and an element `i : ι`,
`piLT X i` is the product of all the types indexed by elements below `i`.  -/
InverseSystem.piLT : {ι : Type u_1} → [Preorder ι] → (ι → Type u_6) → ι → Type (max u_1 u_6)
-- Mathlib.Algebra.Ring.ULift
ULift.addCommMonoidWithOne : {R : Type u} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne (ULift.{u_1, u} R)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The identity morphism on an additive module object.  -/
CategoryTheory.AddMod.id : {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.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.AddMonObj A] → (M : CategoryTheory.AddMod D A) → M.Hom M
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_case : ∀ (f g : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp (f.case g) k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.case g) k) ∪
      (Turing.PartrecToTM2.codeSupp f k ∪ Turing.PartrecToTM2.codeSupp g k)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.toLinearMap_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E ≃ₗ[𝕜] E}, (↑T).IsPositive → (↑T.symm).IsPositive
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instBot : {α : Type u_2} → [inst : TopologicalSpace α] → Bot (TopologicalSpace.Clopens α)
-- Init.Data.List.ToArray
List.findIdx?_toArray : ∀ {α : Type u_1} (p : α → Bool) (l : List α), Array.findIdx? p l.toArray = List.findIdx? p l
-- Mathlib.Data.List.Sort
/-- `l.SortedGE` means that the list is antitonic.  -/
List.SortedGE : {α : Type u_1} → [Preorder α] → List α → Prop
-- Mathlib.Algebra.DirectSum.Ring
/-- Successor powers behave as expected  -/
DirectSum.GSemiring.gnpow_succ' : ∀ {ι : Type u_1} {A : ι → Type u_2} {inst : AddMonoid ι} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  [self : DirectSum.GSemiring A] (n : ℕ) (a : GradedMonoid A),
  GradedMonoid.mk (n.succ • a.fst) (DirectSum.GSemiring.gnpow n.succ a.snd) =
    ⟨n • a.fst, DirectSum.GSemiring.gnpow n a.snd⟩ * a
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      (toAddHom : M →ₙ+ M₂) →
                        (∀ (m : R) (x : M), toAddHom.toFun (m • x) = σ m • toAddHom.toFun x) → M →ₛₗ[σ] M₂
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- **Alias** of `AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map`. -/
AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map : ∀ {X : AlgebraicGeometry.Scheme} (F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat)
  (α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F)
  (H : CategoryTheory.NatTrans.Coequifibered α) {U : X.AffineZariskiSite} (r : ↑(X.presheaf.obj (Opposite.op ↑U))),
  AlgebraicGeometry.Scheme.Hom.opensRange
      ((AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData H).functor.map (CategoryTheory.homOfLE ⋯)) =
    PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) r)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.dualEquiv_functor : FinPartOrd.dualEquiv.functor = FinPartOrd.dual
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Helper function for throwing exceptions with respect to the main goal.  -/
Mathlib.Tactic.Coherence.exception' : Lean.MessageData → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.exp_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Module Rᵐᵒᵖ M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] [inst_5 : TopologicalSpace R] [inst_6 : TopologicalSpace M]
  [inst_7 : IsTopologicalRing R] [inst_8 : IsTopologicalAddGroup M] [inst_9 : ContinuousSMul R M]
  [inst_10 : ContinuousSMul Rᵐᵒᵖ M] [Algebra ℚ R] [Module ℚ M] [T2Space R] [T2Space M] (m : M),
  NormedSpace.exp (TrivSqZeroExt.inr m) = 1 + TrivSqZeroExt.inr m
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.top_coe : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Shift.Localization
/-- The localization functor `L : C ⥤ D` is compatible with the shift.  -/
CategoryTheory.Functor.CommShift.localized : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] →
              (A : Type w) →
                [inst_3 : AddMonoid A] →
                  [inst_4 : CategoryTheory.HasShift C A] → [inst_5 : W.IsCompatibleWithShift A] → L.CommShift A
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) (m₁ a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ D m₁).P a = (D.P a ∨ m₁ = a)
-- Init.Meta.Defs
Lean.Syntax.isIdOrAtom? : Lean.Syntax → Option String
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.smul_coe : ∀ (n : Type u_1) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type u_2) [inst_2 : CommRing R] (m : R)
  (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m), ↑(g • A) = ↑g * ↑A
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.w_assoc : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ) {Z : SSet} (h : ((SSet.skeletonOfMono i) (d + 1)).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.t i d)
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.r i d) h) =
    CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.l i d)
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.b i d) h)