mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.tendsto_implicitFunction : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) {α : Type u_4} {l : Filter α}
  {g₁ : α → F} {g₂ : α → ↥(↑f').ker},
  Filter.Tendsto g₁ l (nhds (f a)) →
    Filter.Tendsto g₂ l (nhds 0) →
      Filter.Tendsto (fun t => HasStrictFDerivAt.implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (nhds a)
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.adapt.eq_1 : ∀ {ε ε' α : Type} (f : ε → ε') (m : EIO ε α) (s : Void IO.RealWorld),
  EIO.adapt f m s =
    match m s with
    | EST.Out.ok a s => EST.Out.ok a s
    | EST.Out.error e s => EST.Out.error (f e) s
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousLinearEquiv.toContinuousAffineEquiv_toContinuousAffineMap : ∀ {k : Type u_1} [inst : Ring k] {E : Type u_10} {F : Type u_11} [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module k F] [inst_6 : TopologicalSpace F]
  (L : E ≃L[k] F), L.toContinuousAffineEquiv.toContinuousAffineMap = (↑L).toContinuousAffineMap
-- Std.Sat.AIG.CachedGatesLemmas
/-- Encoding of implication as boolean expression in AIG form.
 -/
_private.Std.Sat.AIG.CachedGatesLemmas.0.Std.Sat.AIG.imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  Function.Injective ⇑I.incl
-- Init.Data.String.Substring
/-- Checks whether the Boolean predicate `p` returns `true` for every character in a substring.

Short-circuits at the first character for which `p` returns `false`.
 -/
Substring.Raw.all : Substring.Raw → (Char → Bool) → Bool
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
/-- If a functor `F` has a conical limit, so does any naturally isomorphic functor.  -/
CategoryTheory.Enriched.HasConicalLimit.of_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (V : Type u') [inst_1 : CategoryTheory.Category.{v', u'} V]
  [inst_2 : CategoryTheory.MonoidalCategory V] {C : Type u} [inst_3 : CategoryTheory.Category.{v, u} C]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F G : CategoryTheory.Functor J C}
  [CategoryTheory.Enriched.HasConicalLimit V F] (e : F ≅ G), CategoryTheory.Enriched.HasConicalLimit V G
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Formula.equivSentence_not : ∀ {L : FirstOrder.Language} {α : Type u'} (φ : L.Formula α),
  FirstOrder.Language.Formula.equivSentence φ.not =
    FirstOrder.Language.Formula.not (FirstOrder.Language.Formula.equivSentence φ)
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.instIsHomLiftIdMapFiberInclusion : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} (φ : a ⟶ b),
  p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.Functor.Fiber.fiberInclusion.map φ)
-- Mathlib.CategoryTheory.Sites.Types
/-- Given a sheaf `S`, construct an isomorphism `S ≅ [-, S(*)]`.  -/
CategoryTheory.equivYoneda : (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) →
  CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S →
    (S ≅ CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1})))
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  IsLocalizedModule (nonZeroDivisors ℤ) (↑ℤ (↑↑I).subtype)
-- Init.Data.BitVec.Lemmas
BitVec.concat_or_concat : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), x.concat a ||| y.concat b = (x ||| y).concat (a || b)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.add_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  [inst_3 : Preorder ι] {u : ι → α} {x : α}, CauchySeq u → CauchySeq fun n => u n + x
-- Plausible.Random
/-- `Random m α` gives us machinery to generate values of type `α` in the monad `m`.

Note that `m` is a parameter as some types may only be sampleable with access to a certain monad.  -/
Plausible.Random : (Type u → Type u_1) → Type u → Type (max (max 1 u) u_1)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.sub_apply : ∀ {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → SeminormedAddCommGroup (β i)] (x y : PiLp p β)
  (i : ι), (x - y).ofLp i = x.ofLp i - y.ofLp i
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.analyticWithinAt : ∀ {𝕜 : 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} {s : Set E} {x : E},
  AnalyticAt 𝕜 f x → AnalyticWithinAt 𝕜 f s x
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- The edge of `Λ[n, i]` with endpoints `a` and `b`.

This edge only exists if `{i, a, b}` has cardinality less than `n`.  -/
SSet.horn.edge : (n : ℕ) → (i a b : Fin (n + 1)) → a ≤ b → {i, a, b}.card ≤ n → (SSet.horn n i).toSSet.obj (Opposite.op { len := 1 })
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.mk.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving)
  (requestStream : Std.Http.Body.Stream) (keepAliveTimeout : Option Std.Time.Millisecond.Offset)
  (currentTimeout : Std.Time.Millisecond.Offset) (headerTimeout : Option Std.Time.Timestamp)
  (response : Std.Channel (Except IO.Error (Std.Http.Response β))) (respStream : Option β) (requiresData : Bool)
  (expectData : Option ℕ) (handlerDispatched : Bool) (pendingHead : Option Std.Http.Request.Head),
  sizeOf
      { machine := machine, requestStream := requestStream, keepAliveTimeout := keepAliveTimeout,
        currentTimeout := currentTimeout, headerTimeout := headerTimeout, response := response,
        respStream := respStream, requiresData := requiresData, expectData := expectData,
        handlerDispatched := handlerDispatched, pendingHead := pendingHead } =
    1 + sizeOf machine + sizeOf requestStream + sizeOf keepAliveTimeout + sizeOf currentTimeout + sizeOf headerTimeout +
                sizeOf response +
              sizeOf respStream +
            sizeOf requiresData +
          sizeOf expectData +
        sizeOf handlerDispatched +
      sizeOf pendingHead
-- Mathlib.CategoryTheory.Presentable.Directed
/-- The union of two `κ`-bounded diagrams.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ →
          CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ →
            CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instPatternModelForallCharPropOfDecidablePred : {p : Char → Prop} → [DecidablePred p] → String.Slice.Pattern.Model.PatternModel p
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_roo : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi (Std.Slice.size xs) - (lo + 1)
-- Mathlib.Order.Filter.CountableInter
/-- A filter `l` has the countable intersection property if for any countable collection
of sets `s ∈ l` their intersection belongs to `l` as well.  -/
CountableInterFilter : {α : Type u_2} → Filter α → Prop
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
StrongDual.coe_toWeakDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x' : StrongDual 𝕜 E), ⇑(StrongDual.toWeakDual x') = ⇑x'
-- Mathlib.Data.Ordmap.Ordset
Ordnode.eraseMax.valid : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α}, t.Valid → t.eraseMax.Valid
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.hasEigenvalue_of_isRoot : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} [IsDomain R] [Module.Finite R M], (minpoly R f).IsRoot μ → f.HasEigenvalue μ
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.reverse.reverse = t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → Option γ} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl =
    Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Let `s : Set ℝ≥0` be a compact set and consider pairs `(f, a) : (ℝ≥0 → ℝ≥0) × A` where `f` is
continuous on `s`, maps zero to itself, `spectrum ℝ≥0 a ⊆ s` and `0 ≤ a`.

Then `cfcₙ` is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on `s`.  -/
continuousOn_cfcₙ_nnreal_setProd : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ContinuousOn (fun fa => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ quasispectrum NNReal a ⊆ s})
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom (self.map f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom h))
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.instMulAction : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {G : Type u_5} →
              [inst_3 : Group G] →
                [inst_4 : DistribMulAction G M] → [SMulCommClass G R M] → MulAction G (Module.Basis ι R M)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
/-- `I⁻¹` is the inverse of `I` if `I` has an inverse.  -/
FractionalIdeal.right_inverse_eq : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1 → J = I⁻¹
-- Lean.Elab.App
Lean.Elab.Term.elabNamedPattern : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT3Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T3Space M], T3Space Mᵈᵃᵃ
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits an addition.  -/
AddSubgroup.add : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → Add ↥H
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_inf_eq : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) {s t : ClosedSubmodule R M},
  (ClosedSubmodule.mapEquiv f) (s ⊓ t) = (ClosedSubmodule.mapEquiv f) s ⊓ (ClosedSubmodule.mapEquiv f) t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.null.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.null = 1
-- Mathlib.Tactic.AdaptationNote
/-- Elaborator for adaptation notes.  -/
adaptationNoteTermElab : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Monad.Limits
/-- Any monadic functor creates limits.  -/
CategoryTheory.monadicCreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          [CategoryTheory.MonadicRightAdjoint R] → CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.continuous : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M], Continuous ↑f
-- Mathlib.Data.DFinsupp.Module
DFinsupp.isScalarTower : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : Type u_1} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → SMulZeroClass γ (β i)] [inst_2 : (i : ι) → SMulZeroClass δ (β i)] [inst_3 : SMul γ δ]
  [∀ (i : ι), IsScalarTower γ δ (β i)], IsScalarTower γ δ (Π₀ (i : ι), β i)
-- Mathlib.Analysis.Calculus.Deriv.Star
HasDerivWithinAt.star : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {f' : F} {x : 𝕜}
  [TrivialStar 𝕜] {s : Set 𝕜}, HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => star (f x)) (star f') s x
-- Mathlib.Data.DFinsupp.Module
DFinsupp.single_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → SMulZeroClass γ (β i)] {i : ι} (c : γ) (x : β i), (fun₀ | i => c • x) = c • fun₀ | i => x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t u : Finset α}, s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Icc : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.Icc i j = Set.Icc j.rev i.rev
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
/-- If `X` is `n`-coskeletal, then `Truncated.rightExtensionInclusion X n` is a terminal object in
the category `RightExtension (Truncated.inclusion n).op (Truncated.inclusion.op ⋙ X)`.  -/
CategoryTheory.SimplicialObject.IsCoskeletal.isUniversalOfIsRightKanExtension : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      (n : ℕ) →
        [X.IsCoskeletal n] →
          CategoryTheory.CostructuredArrow.IsUniversal
            (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of a limit along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsLimit_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimit K F],
  CategoryTheory.Limits.ReflectsLimit K G
-- Init.Data.BitVec.Bootstrap
BitVec.cons_induction : ∀ {motive : (w : ℕ) → BitVec w → Prop},
  motive 0 BitVec.nil →
    (∀ {w : ℕ} (b : Bool) (bv : BitVec w), motive w bv → motive (w + 1) (BitVec.cons b bv)) →
      ∀ {w : ℕ} (x : BitVec w), motive w x
-- Mathlib.Algebra.Category.Grp.AB
instHasExactLimitsOfShapeDiscreteAddCommGrpCat : ∀ {J : Type u}, CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) AddCommGrpCat
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusFunctorWhiskerLeftIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D)
  [inst_7 : ∀ (F : CategoryTheory.Functor D E) (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (F : CategoryTheory.Functor D E) (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (X : CategoryTheory.Functor D E), (J.plusFunctorWhiskerLeftIso P).inv.app X = (J.plusCompIso X P).inv
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The relation on the sigma type `(W : J) × (F.obj (op W)).obj W` used to construct explicit
coends in `Type`. Two terms `⟨j, x⟩` and `⟨j', x'⟩` are related if and only if there is a
morphism `f : j ⟶ j'` in `J` and an element `y : (F.obj (op j')).obj j` such that
`(F.map f.op).app j y = x` and `(F.obj _).map f y = x'`, see `coendRel_iff` below.  -/
CategoryTheory.Limits.Types.coendRel : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) →
      (j : J) × (F.obj (Opposite.op j)).obj j → (j : J) × (F.obj (Opposite.op j)).obj j → Prop
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (semiringInst : Lean.Expr)
  (addFn? mulFn? powFn? natCastFn? : Option Lean.Expr)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
  (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var) (id_1 : ℕ)
  (type_1 : Lean.Expr) (u_1 : Lean.Level) (semiringInst_1 : Lean.Expr)
  (addFn?_1 mulFn?_1 powFn?_1 natCastFn?_1 : Option Lean.Expr)
  (denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
  (vars_1 : Lean.PArray Lean.Expr) (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var),
  ({ id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?, powFn? := powFn?,
        natCastFn? := natCastFn?, denote := denote, vars := vars, varMap := varMap } =
      { id := id_1, type := type_1, u := u_1, semiringInst := semiringInst_1, addFn? := addFn?_1, mulFn? := mulFn?_1,
        powFn? := powFn?_1, natCastFn? := natCastFn?_1, denote := denote_1, vars := vars_1, varMap := varMap_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          semiringInst = semiringInst_1 ∧
            addFn? = addFn?_1 ∧
              mulFn? = mulFn?_1 ∧
                powFn? = powFn?_1 ∧ natCastFn? = natCastFn?_1 ∧ denote = denote_1 ∧ vars = vars_1 ∧ varMap = varMap_1)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.one_left_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ}, IsPrimitiveRoot 1 k ↔ k = 1
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_apply : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s →
    ∀ [inst_1 : DecidablePred fun x => x ∈ s],
      (ProbabilityTheory.bernoulliMeasure x y p) s =
        if x ∈ s then if y ∈ s then 1 else ↑(unitInterval.toNNReal p)
        else if y ∈ s then ↑(unitInterval.toNNReal (unitInterval.symm p)) else 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α}, s.Nonempty → ∀ {n : ℕ}, (n • s).Nonempty
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_unop_of_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasColimit F.unop
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_sub : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a b : M), -(a - b) = b - a
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.add_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommMonoid X] [inst_3 : Module R X] (y z : OreLocalization S R) (x : OreLocalization S X),
  (y + z) • x = y • x + z • x
-- Mathlib.Topology.Order.IsLUB
/-- The supremum of a bounded above, continuous function on a dense set is equal to the supremum on
the universe.  -/
Dense.ciSup : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLattice α]
  [ClosedIicTopology α] {f : γ → α} [inst_3 : TopologicalSpace γ] {S : Set γ},
  Dense S → Continuous f → BddAbove (Set.range f) → ⨆ s, f ↑s = ⨆ i, f i
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.instCharP : ∀ {R : Type u} [inst : Semiring R] (p : ℕ) [h : CharP R p], CharP (Polynomial R) p
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.find?_char_eq_find?_beq : ∀ {c : Char} {s : String.Slice}, s.find? c = s.find? fun x => x == c
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- The ring congruence of matrices with entries related by `c`.  -/
RingCon.matrix : {R : Type u_1} →
  (n : Type u_2) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : Fintype n] → RingCon R → RingCon (Matrix n n R)
-- Mathlib.Control.LawfulFix
Part.Fix.exists_fix_le_approx : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (x : α),
  ∃ i, Part.fix (⇑f) x ≤ Part.Fix.approx (⇑f) i x
-- Mathlib.Topology.VectorBundle.Basic
IsLinearMap.mk'.congr_simp : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (f f_1 : M → M₂) (e_f : f = f_1)
  (lin : IsLinearMap R f), IsLinearMap.mk' f lin = IsLinearMap.mk' f_1 ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {fallback : β}
  {f : Option β → Option β}, (t.alter k f).getD k fallback = (f t[k]?).getD fallback
-- Lean.Server.References
/-- Paths and module references for every module name. Loaded from `.ilean` files.  -/
Lean.Server.ILeanMap : Type
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isCyclic_of_card_le_three : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Nat.card α ≤ 3 → IsCyclic ↥(alternatingGroup α)