mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.instTransForallIsThetaIsLittleO : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (Asymptotics.IsTheta l) (Asymptotics.IsLittleO l) (Asymptotics.IsLittleO l)
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.mkLambda' : Lean.Name → Lean.BinderInfo → Lean.Expr → Lean.Expr → Bool → Lean.Expr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.fill_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α} {p : RBTree.RBNode.Path α}, (p.fill t).toList = p.withList t.toList
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An alternative constructor for `Hom`,
taking a morphism without a `[IsAddModHom]` instance, between objects with
an `AddModObj` instance (rather than bundled as `AddMod`),
as well as the relevant equality to put such an instance.  -/
CategoryTheory.AddMod.Hom.mk'' : {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 N : D} →
                  [inst_5 : CategoryTheory.AddModObj A M] →
                    [inst_6 : CategoryTheory.AddModObj A N] →
                      (f : M ⟶ N) →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                                CategoryTheory.AddModObj.vadd)
                            CategoryTheory.AddMod.Hom.mk''._auto_1 →
                          { X := M, addMod := inst_5 }.Hom { X := N, addMod := inst_6 }
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.id_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.Comonad.id C).obj X = X
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIsoSelf.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι}
  (h : ¬c.Rel (c.prev j) j), C.xPrevIsoSelf h = C.xPrevIsoSelf h
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.trans : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ L₃ → FreeAddGroup.Red L₁ L₃
-- Init.Core
eq_iff_true_of_subsingleton : ∀ {α : Sort u_1} [Subsingleton α] (x y : α), x = y ↔ True
-- Mathlib.Analysis.Complex.Circle
/-- If `z` is a nonzero complex number, then `conj z / z` belongs to the unit circle.  -/
Circle.ofConjDivSelf : (z : ℂ) → z ≠ 0 → Circle
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toContinuousLinearEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ↑e.symm = (↑e).symm
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonTextDocumentChangeRegistrationOptions : Lean.FromJson Lean.Lsp.TextDocumentChangeRegistrationOptions
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isAffine_Spec : ∀ (R : CommRingCat), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Spec R)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.norm : ∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially fun x => ‖f x‖
-- Init.Data.Dyadic.Basic
Dyadic.le_total : ∀ (x y : Dyadic), x ≤ y ∨ y ≤ x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
ZeroHom.withTopMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), ⇑f.withTopMap = WithTop.map ⇑f
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- A variant of `DirichletCharacter.norm_LSeries_product_ge_one` in terms of the L-functions.  -/
DirichletCharacter.norm_LFunction_product_ge_one : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {x : ℝ},
  0 < x →
    ∀ (y : ℝ),
      ‖DirichletCharacter.LFunctionTrivChar N (1 + ↑x) ^ 3 *
              DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y) ^ 4 *
            DirichletCharacter.LFunction (χ ^ 2) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥
        1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_or_lt_of_div_lt_div : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b c d : α},
  a / d < b / c → a < b ∨ c < d
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_apply_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) {x : β} {y : α}, e.symm x = y ↔ x = e y
-- Init.Data.Array.MinMax
_private.Init.Data.Array.MinMax.0.Array.max?.eq_1 : ∀ {α : Type u_1} [inst : Max α] (arr : Array α), arr.max? = if h : arr ≠ #[] then some (arr.max h) else none
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantFormClass.mk : ∀ {F : Type u_1} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} [inst : FunLike F UpperHalfPlane ℂ],
  (∀ (f : F), ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f) → SlashInvariantFormClass F Γ k
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.continuous_of_dual_apply_continuous : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {α : Type u_5} [inst_10 : TopologicalSpace α] {g : α → E →SWOT[σ] F},
  (∀ (x : E) (y : StrongDual 𝕜₂ F), Continuous fun a => y ((g a) x)) → Continuous g
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason : Type
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsRestriction.isRestriction_removeLoops : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → ∀ [N.Loopless], N.IsRestriction M.removeLoops
-- Mathlib.RingTheory.Polynomial.RationalRoot
exists_integer_of_is_root_of_monic : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [IsDomain A] [UniqueFactorizationMonoid A] [inst_3 : Field K]
  [inst_4 : Algebra A K] [IsFractionRing A K] {p : Polynomial A},
  p.Monic → ∀ {r : K}, (Polynomial.aeval r) p = 0 → ∃ r', r = (algebraMap A K) r' ∧ r' ∣ p.coeff 0
-- Mathlib.FieldTheory.Fixed
/-- `MulSemiringAction.toAlgAut` is surjective.  -/
FixedPoints.toAlgAut_surjective : ∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G],
  Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- The isomorphism `(Φ.iterationFunctor J).obj ⊥ ≅ Φ.X₀`.  -/
CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjBotIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] → (Φ.iterationFunctor J).obj ⊥ ≅ Φ.X₀
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.orderTop : {α : Type u_1} → [inst : LE α] → [OrderTop α] → OrderTop (Additive α)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- The typeclass `Least? α` optionally provides a smallest element of `α`, `least? : Option α`.

The main use case of this typeclass is to use it in combination with `UpwardEnumerable` to
obtain a (possibly infinite) ascending enumeration of all elements of `α`.
 -/
Std.PRange.Least? : Type u → Type u
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrictHom`.

---

A version of `MonoidHom.domRestrict` as a homomorphism.  -/
MonoidHom.restrictHom : {M : Type u_1} →
  [inst : MulOneClass M] →
    {S : Type u_5} →
      [inst_1 : SetLike S M] →
        [inst_2 : SubmonoidClass S M] → (M' : S) → (A : Type u_6) → [inst_3 : CommMonoid A] → (M →* A) →* ↥M' →* A
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.range_toContinuousMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal},
  (Set.range fun α => ODE.FunSpace.toContinuousMap α) = {α | LipschitzWith L ⇑α ∧ α t₀ ∈ Metric.closedBall x₀ ↑r}
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.fromCostructuredArrow_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D}
  (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)),
  (CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).pt = X
-- Mathlib.Order.FixedPoints
/-- Next fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
`x` is a point such that `x ≤ f x`, then `f.nextFixed x hx` is the least fixed point of `f`
that is greater than or equal to `x`.  -/
OrderHom.nextFixed : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → (x : α) → x ≤ f x → ↑(Function.fixedPoints ⇑f)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.instIsPreimmersionFromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), AlgebraicGeometry.IsPreimmersion (X.fromSpecStalk x)
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.ext : ∀ {α : Type u_5} {ι : Type u_6} {x y : Combinatorics.Line α ι}, x.idxFun = y.idxFun → x = y
-- Init.Data.List.Count
List.count_flatMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {l : List α} {f : α → List β} {x : β},
  List.count x (List.flatMap f l) = (List.map (List.count x ∘ f) l).sum
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_zero : ∀ {n : ℕ}, n >>> 0 = n
-- Mathlib.Algebra.Star.LinearMap
/-- The intrinsic star additive monoid structure on linear maps.  -/
LinearMap.intrinsicStarAddMonoid : {R : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : InvolutiveStar R] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : StarAddMonoid E] →
                [StarModule R E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module R F] →
                      [inst_8 : StarAddMonoid F] → [StarModule R F] → StarAddMonoid (WithConv (E →ₗ[R] F))
-- Mathlib.Analysis.Convex.Function
ConvexOn.sub_strictConcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, ConvexOn 𝕜 s f → StrictConcaveOn 𝕜 s g → StrictConvexOn 𝕜 s (f - g)
-- Mathlib.Analysis.Distribution.Support
Distribution.mem_dsupport_iff_not_isVanishingOn : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} (x : α),
  x ∈ Distribution.dsupport f ↔ ∀ (s : Set α), x ∈ s → IsOpen s → ¬Distribution.IsVanishingOn f s
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.smul_congr : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {a b : 𝕜}, Balanced 𝕜 s → ‖a‖ = ‖b‖ → a • s = b • s
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addCongrTable.swapCgrRepr : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.mk : Lean.Grind.Linarith.Poly → Bool → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Lean.Meta.Grind.Arith.Linear.IneqCnstr
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.hasImage_iso_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasImage g],
  CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Fourier.AddCircle
hasDerivAt_fourier_neg : ∀ (T : ℝ) (n : ℤ) (x : ℝ),
  HasDerivAt (fun y => (fourier (-n)) ↑y) (-2 * ↑Real.pi * Complex.I * ↑n / ↑T * (fourier (-n)) ↑x) x
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add_of_distinct_val : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v x ≠ v y → v (x + y) = min (v x) (v y)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isIndepSet_iff_isAntichain_adj : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsIndepSet s ↔ IsAntichain G.Adj s
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.eval₂ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  {φ : MvPolynomial σ R} {m n : ℕ},
  φ.IsHomogeneous m →
    ∀ (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S),
      (∀ (r : R), (f r).IsHomogeneous 0) →
        (∀ (i : σ), (g i).IsHomogeneous n) → (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
-- Mathlib.Data.Quot
Trunc.ind : ∀ {α : Sort u_1} {β : Trunc α → Prop}, (∀ (a : α), β (Trunc.mk a)) → ∀ (q : Trunc α), β q
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.toMon ⟶ B.toMon), (CategoryTheory.Grp.homMk' f).hom = f
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance.val : Lean.Meta.SynthInstance.Instance → Lean.Expr
-- Mathlib.Algebra.Order.Field.Basic
half_lt_self_iff : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  a / 2 < a ↔ 0 < a
-- Mathlib.RingTheory.Teichmuller
_private.Mathlib.RingTheory.Teichmuller.0.Perfection.teichmullerAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.Algebra.Pi
Pi.algHom_comp : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {B : Type u_4} {C : Type u_5} [inst_3 : Semiring B] [inst_4 : Algebra R B]
  [inst_5 : Semiring C] [inst_6 : Algebra R C] (g : (i : ι) → C →ₐ[R] A i) (h : B →ₐ[R] C),
  (Pi.algHom R A g).comp h = Pi.algHom R A fun i => (g i).comp h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `X` represents a presheaf of additive groups `F`, then `Hom(-, X)` is isomorphic to `F` as
a presheaf of additive groups.  -/
CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) →
          (α : (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X) → CategoryTheory.yonedaAddGrpObj X ≅ F
-- Init.Data.String.Defs
String.instHAddRawSlice : HAdd String.Pos.Raw String.Slice String.Pos.Raw
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_interior_eq_interior_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' interior s = interior (f ⁻¹' s)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.sub.sizeOf_spec : ∀ (a b : Lean.Grind.Linarith.Expr), sizeOf (a.sub b) = 1 + sizeOf a + sizeOf b
-- Init.Control.Lawful.MonadLift.Instances
instLawfulMonadLiftT : ∀ (m : Type u → Type v) [inst : Monad m], LawfulMonadLiftT m m
-- Init.Data.List.Basic
List.Lex.brecOn : ∀ {α : Type u} {r : α → α → Prop} {motive : (as bs : List α) → List.Lex r as bs → Prop} {as bs : List α}
  (t : List.Lex r as bs),
  (∀ (as bs : List α) (t : List.Lex r as bs), List.Lex.below t → motive as bs t) → motive as bs t
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A)
      (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)))
      (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ))
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_add_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (μ κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsSFiniteKernel μ] [ProbabilityTheory.IsSFiniteKernel κ],
  (μ + κ).compProd η = μ.compProd η + κ.compProd η
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], ↑0 = 0
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instHashableStained.hash : Mathlib.Linter.Flexible.Stained✝ → UInt64
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_mul_of_one_le : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
  [ExistsAddOfLE R] [inst_5 : Sub R] [OrderedSub R] {x : R},
  1 ≤ x → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β],
  MeasureTheory.SimpleFunc.instAdd = { add := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 + x2) f).seq g }
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.minDegree_eq_zero_iff_support_ne : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  G.minDegree = 0 ↔ G.support ≠ Set.univ
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] (x x_1 : C) (x_2 : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2 =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x_2 { unmop := x_1 } { unmop := x }
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Module.End.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial : {K : Type u_1} →
  {V : Type u_2} →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [IsAlgClosed K] → [FiniteDimensional K V] → [Nontrivial V] → (f : Module.End K V) → Inhabited f.Eigenvalues
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The interior of a fundamental domain, those
points of the domain not lying in any translate.  -/
MeasureTheory.addFundamentalInterior : (G : Type u_1) → {α : Type u_3} → [inst : AddGroup G] → [AddAction G α] → Set α → Set α
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instPreorder : {M : Type u_1} → [inst : CommMonoid M] → Preorder (Associates M)
-- Mathlib.Analysis.Convex.Intrinsic
/-- **Alias** of `AffineIsometry.intrinsicFrontier_image`. -/
AffineIsometry.image_intrinsicFrontier : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P),
  intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.eq_5 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
        (CategoryTheory.WithTerminal.of _Z))
  (h_2 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star)
  (h_3 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x)
  (h_4 :
    (x : CategoryTheory.WithTerminal C) →
      (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y))
  (h_5 :
    Unit → motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => h_2 _X x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => h_3 _X x
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => h_4 x _Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star => h_5 ()) =
    h_5 ()
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_of_le_right : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {K L : AddSubgroup G},
  K ≤ L → ∀ [H.IsFiniteRelIndex L], H.IsFiniteRelIndex K
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}},
  forM t f = forM t.toList f
-- Init.Data.SInt.Lemmas
USize.toISize_ofNat' : ∀ {n : ℕ}, (USize.ofNat n).toISize = ISize.ofNat n
-- Mathlib.LinearAlgebra.Ray
/-- The images of two vectors under a linear equivalence are on the same ray if and only if the
original vectors are on the same ray.  -/
SameRay.sameRay_map_iff : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {x y : M} (e : M ≃ₗ[R] N), SameRay R (e x) (e y) ↔ SameRay R x y
-- Mathlib.Data.List.MinMax
List.min_le_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] {l : List α} {a x : α},
  x ∈ l → x ≤ a → List.foldr min ⊤ l ≤ a
-- Mathlib.Topology.MetricSpace.Holder
/-- A Hölder continuous function is uniformly continuous  -/
HolderWith.uniformContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → 0 < r → UniformContinuous f