mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.lintegral_iInf_posterior_le_avgRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ],
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [inst_2 : ProbabilityTheory.IsFiniteKernel P]
      (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (π : MeasureTheory.Measure Θ)
      [inst_4 : MeasureTheory.IsFiniteMeasure π],
      ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂π.bind ⇑P ≤
        ProbabilityTheory.avgRisk ℓ P κ π
-- Mathlib.Order.Defs.Unbundled
IsEquiv.mk : ∀ {α : Sort u_1} {r : α → α → Prop} [toIsPreorder : IsPreorder α r] [toSymm : Std.Symm r], IsEquiv α r
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_mul_exp_iff_le : ∀ {x y : WithZero (Multiplicative ℤ)}, y ≠ 0 → (x < y * WithZero.exp 1 ↔ x ≤ y)
-- Init.Data.Bool
Bool.and_or_inj_right : ∀ {m x y : Bool}, (x && m) = (y && m) → (x || m) = (y || m) → x = y
-- Mathlib.NumberTheory.FactorisationProperties
/-- There exists infinitely many deficient numbers  -/
Nat.infinite_deficient : {n | n.Deficient}.Infinite
-- Init.Data.UInt.Bitwise
UInt16.shiftLeft_eq_shiftLeft_mod : ∀ (a b : UInt16), a <<< b = a <<< (b % 16)
-- Mathlib.Topology.VectorBundle.Hom
/-- Topology on the total space of the continuous `σ`-semilinear maps between two "normable" vector
bundles over the same base.  -/
Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace : {𝕜₁ : Type u_1} →
  [inst : NontriviallyNormedField 𝕜₁] →
    {𝕜₂ : Type u_2} →
      [inst_1 : NontriviallyNormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {B : Type u_3} →
            (F₁ : Type u_4) →
              [inst_2 : NormedAddCommGroup F₁] →
                [inst_3 : NormedSpace 𝕜₁ F₁] →
                  (E₁ : B → Type u_5) →
                    [inst_4 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)] →
                        [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          (F₂ : Type u_6) →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜₂ F₂] →
                                (E₂ : B → Type u_7) →
                                  [inst_9 : (x : B) → AddCommGroup (E₂ x)] →
                                    [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] →
                                      [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                        [inst_12 : TopologicalSpace B] →
                                          [inst_13 : (x : B) → TopologicalSpace (E₁ x)] →
                                            [inst_14 : FiberBundle F₁ E₁] →
                                              [VectorBundle 𝕜₁ F₁ E₁] →
                                                [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                  [inst_17 : FiberBundle F₂ E₂] →
                                                    [VectorBundle 𝕜₂ F₂ E₂] →
                                                      [∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                        [∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] →
                                                          [RingHomIsometric σ] →
                                                            TopologicalSpace
                                                              (Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x =>
                                                                E₁ x →SL[σ] E₂ x)
-- Mathlib.CategoryTheory.Sites.Point.Conservative
/-- [Stacks Tag 00YL](https://stacks.math.columbia.edu/tag/00YL) ((3)) -/
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints →
    ∀ (A : Type u') [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
      [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
      [inst_4 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory A FC]
      [(CategoryTheory.forget A).ReflectsIsomorphisms]
      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
      [hJ : J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.AB5OfSize.{w, w, v', u'} A]
      [CategoryTheory.Limits.HasFiniteLimits A], CategoryTheory.JointlyFaithful fun Φ => Φ.obj.sheafFiber
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toAddSubgroup_injective : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M},
  Function.Injective Submodule.toAddSubgroup
-- Mathlib.Algebra.GradedMonoid
/-- `GMonoid` implies a `Monoid (GradedMonoid A)`.  -/
GradedMonoid.GMonoid.toMonoid : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddMonoid ι] → [GradedMonoid.GMonoid A] → Monoid (GradedMonoid A)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.norm_sub_le_of_mem_A : ∀ {𝕜 : 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}
  {c : 𝕜},
  1 < ‖c‖ →
    ∀ {r ε : ℝ},
      0 < ε →
        0 < r →
          ∀ {x : E} {L₁ L₂ : E →L[𝕜] F},
            x ∈ FDerivMeasurableAux.A f L₁ r ε → x ∈ FDerivMeasurableAux.A f L₂ r ε → ‖L₁ - L₂‖ ≤ 4 * ‖c‖ * ε
-- Mathlib.Analysis.Fourier.ZMod
DirichletCharacter.fourierTransform_eq_gaussSum_mulShift : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (k : ZMod N),
  ZMod.dft (⇑χ) k = gaussSum χ (ZMod.stdAddChar.mulShift (-k))
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.mk : Lean.ConstantInfo →
  Lean.ConstantInfo →
    Array Lean.EnvExtensionState → Lean.VisibilityMap✝ Lean.AsyncConsts✝ → Lean.Environment.ConstPromiseVal✝
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If `S : Finset (Fin (n + 1))` is order isomorphic to `Fin (m + 1)`,
then the face `face S` of `Δ[n]` is representable by `m`,
i.e. `face S` is isomorphic to `Δ[m]`, see `stdSimplex.isoOfRepresentableBy`.  -/
SSet.stdSimplex.faceRepresentableBy : {n : ℕ} →
  (S : Finset (Fin (n + 1))) →
    (m : ℕ) → Fin (m + 1) ≃o ↥S → CategoryTheory.Functor.RepresentableBy (SSet.stdSimplex.face S).toSSet { len := m }
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofIntLE : ∀ (x : ℤ) (h₁ : Int8.minValue.toInt ≤ x) (h₂ : x ≤ Int8.maxValue.toInt),
  (Int8.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 8 x
-- Mathlib.Data.FinEnum
FinEnum.instBitVec : (n : ℕ) → FinEnum (BitVec n)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (toEquiv : α ≃ β)
  (measurable_toFun : autoParam (Measurable ⇑toEquiv) MeasurableEquiv.measurable_toFun._autoParam)
  (measurable_invFun : autoParam (Measurable ⇑toEquiv.symm) MeasurableEquiv.measurable_invFun._autoParam)
  (toEquiv_1 : α ≃ β)
  (measurable_toFun_1 : autoParam (Measurable ⇑toEquiv_1) MeasurableEquiv.measurable_toFun._autoParam)
  (measurable_invFun_1 : autoParam (Measurable ⇑toEquiv_1.symm) MeasurableEquiv.measurable_invFun._autoParam),
  ({ toEquiv := toEquiv, measurable_toFun := measurable_toFun, measurable_invFun := measurable_invFun } =
      { toEquiv := toEquiv_1, measurable_toFun := measurable_toFun_1, measurable_invFun := measurable_invFun_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y), CategoryTheory.Limits.Cofork.π c.inrCokernelCofork = c.fst
-- Mathlib.Topology.Irreducible
irreducibleComponent_mem_irreducibleComponents : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), irreducibleComponent x ∈ irreducibleComponents X
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- The public constructor for `ConvexSpace`.  -/
Convexity.ConvexSpace.mk : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_9} →
          (sConvexComb : Convexity.StdSimplex R M → M) →
            (∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) →
              (∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)),
                  sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb (Convexity.sConvexComb f)) →
                Convexity.ConvexSpace R M
-- Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
/-- The functor `ComposableArrows (CochainComplex C ℤ) 1 ⥤ CochainComplex C ℤ` which
sends a morphism of cochain complexes to its mapping cone.  -/
HomotopyCategory.composableArrowsFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        CategoryTheory.Functor (CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1) (CochainComplex C ℤ)
-- Std.Time.Format.Basic
/-- Whether to allow leap seconds, such as `2016-12-31T23:59:60Z`.
Default is `false`.
 -/
Std.Time.FormatConfig.allowLeapSeconds : Std.Time.FormatConfig → Bool
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {δ : Type u_5} [inst_3 : PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ),
  (h.comp g).comp f = h.comp (g.comp f)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.mk.inj : ∀ {γ : Type} {defn : Lean.KeyedDeclsAttribute.Def γ} {tableRef : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)}
  {ext : Lean.KeyedDeclsAttribute.Extension γ} {defn_1 : Lean.KeyedDeclsAttribute.Def γ}
  {tableRef_1 : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)} {ext_1 : Lean.KeyedDeclsAttribute.Extension γ},
  { defn := defn, tableRef := tableRef, ext := ext } = { defn := defn_1, tableRef := tableRef_1, ext := ext_1 } →
    defn = defn_1 ∧ tableRef = tableRef_1 ∧ ext = ext_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α} {v : β},
  (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Mathlib.Analysis.Complex.Basic
Complex.isometry_conj : Isometry ⇑(starRingEnd ℂ)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instZero : {α : Type u} → Zero (WithZero α)
-- Mathlib.Analysis.Complex.Tietze
/-- **Alias** of `BoundedContinuousFunction.exists_norm_eq_domRestrict_eq`.

---

**Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If `e : C(X, Y)` is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ` of the same norm such that `g ∘ e = f`.  -/
BoundedContinuousFunction.exists_norm_eq_restrict_eq : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X},
  IsClosed s →
    ∀ (𝕜 : Type v) [inst_2 : RCLike 𝕜] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
      [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E), ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_id : ∀ {R : Type u} [inst : CommRing R] {A : CommAlgCat R},
  CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.id A) = AlgHom.id R ↑A
-- Mathlib.Tactic.Widget.LibraryRewrite
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.ExtState.default : Mathlib.Tactic.LibraryRewrite.ExtState✝
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp_lift_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : PerfectRing N p] [inst_11 : IsPRadical j p] (x : L),
  (PerfectRing.lift j k p) ((PerfectRing.lift i j p) x) = (PerfectRing.lift i k p) x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Having wide pullback at any universe level implies having binary pullbacks.  -/
CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks : ∀ (D : Type u) [inst : CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasWidePullbacks D],
  CategoryTheory.Limits.HasPullbacks D
-- Mathlib.Order.Fin.Basic
Fin.zero_eq_top : ∀ {n : ℕ} [inst : NeZero n], 0 = ⊤ ↔ n = 1
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- The incenter of a simplex bisects the angle at a point shared between two faces, as measured
between the incenter and its touchpoints on those faces.  -/
Affine.Simplex.angle_incenter_touchpoint_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {p : P} {i₁ i₂ : Fin (n + 1)},
  p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points) →
    p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) →
      EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₁) =
        EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₂)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.reduceOp : Lean.Name → ℕ → (f : ℕ → ℕ) → ({n : ℕ} → Fin n → Fin (f n)) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.HasSheafify.isLeftExact : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} A} [self : CategoryTheory.HasSheafify J A],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoHomologyι_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h).inv (K.homologyι i) =
    CategoryTheory.CategoryStruct.id (K.opcycles i)
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherian_univ_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.NoetherianSpace ↑Set.univ ↔ TopologicalSpace.NoetherianSpace α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.E2.eq_1 : EisensteinSeries.E2 = (1 / (2 * riemannZeta 2)) • EisensteinSeries.G2
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.trace_traceDual_mul : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι K L) (i j : ι), (Algebra.trace K L) (b.traceDual i * b j) = if j = i then 1 else 0
-- Lean.Meta.Tactic.Grind.Util
/-- If the target is not `False`, applies `byContradiction`.
 -/
Lean.MVarId.byContra? : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Lean.Attributes
Lean.Attribute.Builtin.ensureNoArgs : Lean.Syntax → Lean.AttrM Unit
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme on a metric space has vanishing diameter if diameter approaches 0 along each branch.  -/
CantorScheme.VanishingDiam : {β : Type u_1} → {α : Type u_2} → (List β → Set α) → [PseudoMetricSpace α] → Prop
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.vcgenDischargeGrind : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.OplaxTrans.Modification η θ → CategoryTheory.Oplax.OplaxTrans.Hom η θ
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_strictMono : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R],
  1 < a → b / (1 - a) < u₀ → StrictMono (arithGeom a b u₀)
-- Mathlib.Data.Part
Part.instNeg : {α : Type u_1} → [Neg α] → Neg (Part α)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Std.TransCmp cmp] {k : α}, t.keys.contains k = t.contains k
-- Mathlib.Topology.Path
Path.extend_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ Set.Icc 0 1),
  γ.extend t = γ ⟨t, ht⟩
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
/-- Given a simplicial object `E` in the category `FormalCoproduct C`, this is the
functor `(Cᵒᵖ ⥤ A) ⥤ CosimplicialObject A` which sends `P : Cᵒᵖ ⥤ A` to the
cosimplicial object which sends `⦋n⦌` to the "evaluation" of `P` on `E _⦋n⦌`.  -/
CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [CategoryTheory.Limits.HasProducts A] →
          CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C) →
            CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.CosimplicialObject A)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.getEntryLT! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited (Sigma β)] → Std.DTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_mapPullbackAdj_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  (U : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f).counit.app U =
    CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst U.left X) ⋯
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
mul_inf₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : SemilatticeInf G₀] [PosMulReflectLT G₀] {c : G₀},
  0 ≤ c → ∀ (a b : G₀), c * (a ⊓ b) = c * a ⊓ c * b
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_union_add_inter₀' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (t : Set α), μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_ind : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  {motive : Std.HashMap.Raw α β → Prop} (m : Std.HashMap.Raw α β) {l : ρ},
  motive m → (∀ (m : Std.HashMap.Raw α β) (a : α) (b : β), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- `localCohomology.ofDiagram I i` is the functor sending a module `M` over a commutative
ring `R` to the direct limit of `Ext^i(R/J, M)`, where `J` ranges over a collection of ideals
of `R`, represented as a functor `I`.  -/
localCohomology.ofDiagram : {R : Type (max u v)} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D (Ideal R) → ℕ → CategoryTheory.Functor (ModuleCat R) (ModuleCat R)
-- Lean.Meta.Match.SolveOverlap
/-- Try applying `injection` to a local declaration that is not in `forbidden`.

We use `forbidden` because the `injection` tactic might fail to clear the variable if there are forward dependencies.
See `proveSubgoalLoop` for additional details.
 -/
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.injectionAny : Lean.MVarId → optParam Lean.FVarIdSet ∅ → Lean.MetaM Lean.Meta.Match.InjectionAnyResult✝
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap.eq_4 : ∀ (x : ℤ), Lean.Grind.IntInterval.ii.wrap x = x
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (E : ℰ) {X Y : C} (f : X ⟶ Y)
  (g : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
  {Z : ℰ} (h : E ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv g).down h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.uliftYonedaEquiv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.map f) g)).down
      h
-- Mathlib.Analysis.Convex.Between
Wbtw.left_ne_right_of_ne_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Wbtw R x y z → y ≠ z → x ≠ z
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.instAddCommGroup : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (F G : CochainComplex C ℤ) → (n : ℤ) → AddCommGroup (CochainComplex.HomComplex.Cochain F G n)
-- Mathlib.Data.Finsupp.SMul
Finsupp.module : (α : Type u_1) →
  (M : Type u_3) → {R : Type u_6} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module R (α →₀ M)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.coe_inf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), ↑(I ⊓ J) = ↑I ∩ ↑J
-- Mathlib.MeasureTheory.PiSystem
IsPiSystem.insert_empty : ∀ {α : Type u_1} {S : Set (Set α)}, IsPiSystem S → IsPiSystem (insert ∅ S)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), Set.range ⇑I.subschemeι = ↑I.support
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.instNonemptyStrongNormalizationMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α], Nonempty (StrongNormalizationMonoid α)
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.span_singleton_sup_ker_eq_top : ∀ {K : Type u_3} {V : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (f : V →ₗ[K] K)
  {x : V}, f x ≠ 0 → K ∙ x ⊔ f.ker = ⊤
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_le_embedding : ∀ (α : Type u) (β' : Type v), Cardinal.mk (α ≃ β') ≤ Cardinal.mk (α ↪ β')