mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsDirectedOrderSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  IsDirectedOrder (Subtype J.PropSet)
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.z_zero₂ : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : CategoryTheory.HasShift D M] (self : CategoryTheory.CommShift₂Setup D M) (m₁ m₂ : M),
  self.z (m₁, 0) (m₂, 0) = 1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_inr : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : M),
  (TrivSqZeroExt.map f) (TrivSqZeroExt.inr x) = TrivSqZeroExt.inr (f x)
-- Mathlib.Order.Directed
directedOn_iff_directed : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, DirectedOn r s ↔ Directed r Subtype.val
-- Mathlib.AlgebraicGeometry.Noetherian
/-- If a scheme `X` has a cover by affine opens whose sections are Noetherian rings,
then `X` is locally Noetherian.  -/
AlgebraicGeometry.isLocallyNoetherian_of_affine_cover : ∀ {X : AlgebraicGeometry.Scheme} {ι : Sort u_1} {S : ι → ↑X.affineOpens},
  ⨆ i, ↑(S i) = ⊤ →
    (∀ (i : ι), IsNoetherianRing ↑(X.presheaf.obj (Opposite.op ↑(S i)))) → AlgebraicGeometry.IsLocallyNoetherian X
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The presieve associated to a set of sections.
This is a surjection, see `presieveOfSections_surjective`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections : {X : AlgebraicGeometry.Scheme} →
  (U : X.AffineZariskiSite) → Set ↑(X.presheaf.obj (Opposite.op U.toOpens)) → CategoryTheory.Presieve U
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [Nontrivial α] (s : Multiset α),
  s.lcm = 0 ↔ 0 ∈ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constInsertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {l : List α},
          (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t₁ l)).Equiv
            ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t₂ l)
-- Lean.Server.Rpc.Basic
Lean.Lsp.instToJsonRpcWireFormat : Lean.ToJson Lean.Lsp.RpcWireFormat
-- Mathlib.Data.NNRat.Floor
NNRat.ceil_coe : ∀ (q : ℚ≥0), ⌈↑q⌉₊ = ⌈q⌉₊
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.code : {α : Type u} → Lean.JsonRpc.ResponseError α → Lean.JsonRpc.ErrorCode
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.mk.sizeOf_spec : ∀ (errors : IO.Ref (Array Lean.Meta.RefinedDiscrTree.ImportFailure✝)), sizeOf { errors := errors } = 1 + sizeOf errors
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.isAddFundamentalDomain : ∀ {ι : Type u_3} {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] [inst_4 : IsZLattice ℝ L]
  [Finite ι] (b : Module.Basis ι ℤ ↥L) [inst_6 : MeasurableSpace E] [OpensMeasurableSpace E]
  (μ : MeasureTheory.Measure E),
  MeasureTheory.IsAddFundamentalDomain (↥L) (ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ L b)) μ
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensor_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).fst =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.fst Y.fst
-- Mathlib.GroupTheory.GroupAction.Basic
/-- A isomorphism between the stabilizers of two elements in the same orbit.  -/
AddAction.stabilizerEquivStabilizerOfOrbitRel : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        {a b : α} → (AddAction.orbitRel G α) a b → ↥(AddAction.stabilizer G a) ≃+ ↥(AddAction.stabilizer G b)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      h
-- Mathlib.Data.List.FinRange
List.ofFn_eq_map : ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, List.ofFn f = List.map f (List.finRange n)
-- Mathlib.Topology.Algebra.Field
IsTopologicalDivisionRing.toIsTopologicalRing : ∀ {K : Type u_1} {inst : DivisionRing K} {inst_1 : TopologicalSpace K} [self : IsTopologicalDivisionRing K],
  IsTopologicalRing K
-- Mathlib.Data.Fintype.Order
Finite.bddBelow_range : ∀ {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] (f : ι → α),
  BddBelow (Set.range f)
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the
image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.  -/
continuousAt_of_monotoneOn_of_image_mem_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α}, MonotoneOn f s → s ∈ nhds a → f '' s ∈ nhds (f a) → ContinuousAt f a
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.instInhabited = { default := ⊥ }
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.registerAlias : Lean.Name → Lean.PrettyPrinter.Formatter.FormatterAliasValue → IO Unit
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.mk.injEq : ∀ (isIncomplete : Bool) (items : Array Lean.Lsp.CompletionItem) (isIncomplete_1 : Bool)
  (items_1 : Array Lean.Lsp.CompletionItem),
  ({ isIncomplete := isIncomplete, items := items } = { isIncomplete := isIncomplete_1, items := items_1 }) =
    (isIncomplete = isIncomplete_1 ∧ items = items_1)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.endSection.sizeOf_spec : ∀ (stx : Lean.Syntax) (id? : Option Lean.Name) (danglingDot : Bool) (scopeNames : List String),
  sizeOf (Lean.Elab.CompletionInfo.endSection stx id? danglingDot scopeNames) =
    1 + sizeOf stx + sizeOf id? + sizeOf danglingDot + sizeOf scopeNames
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.map_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  (Monoid.Coprod.map f g).comp Monoid.Coprod.inl = Monoid.Coprod.inl.comp f
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- The identity morphism on an object.  -/
CategoryTheory.ReflQuiver.id : {obj : Type u} → [self : CategoryTheory.ReflQuiver obj] → (X : obj) → X ⟶ X
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.quotientFunc_smul : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [inst_1 : SlashInvariantFormClass F 𝒢 k] {h : GL (Fin 2) ℝ} (hh : h ∈ ℋ) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
  SlashAction.map k h (SlashInvariantForm.quotientFunc f q) = SlashInvariantForm.quotientFunc f (⟨h, hh⟩⁻¹ • q)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C}
  (h : (t.eTruncGE.obj j).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map f).app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ j).app X) h
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
/-- The canonical map from the base change of the cotangent space `T ⊗[R] I/I²` to the
cotangent space `(I · (T ⊗[R] S))/(I · (T ⊗[R] S))²` of the extended ideal.
This map is always surjective (`tensorCotangentHom_surjective`) and injective
if `T` is `R`-flat (`tensorCotangentHom_injective_of_flat`).  -/
Ideal.tensorCotangentHom : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                (I : Ideal S) →
                  TensorProduct R T I.Cotangent →ₗ[T]
                    (Ideal.map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent
-- Mathlib.Data.Finset.Basic
/-- **Alias** of the reverse direction of `Multiset.toFinset_nonempty`. -/
Multiset.Aesop.toFinset_nonempty_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s ≠ 0 → s.toFinset.Nonempty
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.monotone_shiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.ObjectProperty C} {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A], P ≤ Q → P.shiftClosure A ≤ Q.shiftClosure A
-- Mathlib.Tactic.Translate.Core
/-- Return the provided target name or autogenerate one if one was not provided.  -/
Mathlib.Tactic.Translate.targetName : Mathlib.Tactic.Translate.TranslateData → Mathlib.Tactic.Translate.Config → Lean.Name → Lean.CoreM Lean.Name
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticAt : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {x : (i : ι) → Em i}, AnalyticAt 𝕜 (⇑f) x
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.exists_pow_eq_iff : ∀ {n a : ℕ}, (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a
-- Mathlib.Data.NNRat.Defs
NNRat.divNat_mul_right : ∀ {a : ℕ}, a ≠ 0 → ∀ (n d : ℕ), NNRat.divNat (n * a) (d * a) = NNRat.divNat n d
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableOn.inv` -/
DifferentiableOn.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {S : Set E}, DifferentiableOn 𝕜 h S → (∀ x ∈ S, h x ≠ 0) → DifferentiableOn 𝕜 (fun i => (h i)⁻¹) S
-- Mathlib.Algebra.Algebra.Operations
Submodule.span_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A) (n : ℕ),
  Submodule.span R s ^ n = Submodule.span R (s ^ n)
-- Lean.Widget.Types
Lean.Widget.WidgetInstance.mk.sizeOf_spec : ∀ (id : Lean.Name) (javascriptHash : UInt64) (props : StateM Lean.Server.RpcObjectStore Lean.Json),
  sizeOf { id := id, javascriptHash := javascriptHash, props := props } = 1 + sizeOf id + sizeOf javascriptHash
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.domRestrict'_apply : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M)
  (x : ↥p), ((LinearMap.domRestrict' p) f) x = f ↑x
-- Mathlib.Order.Ideal
Order.Ideal.mem_sInf : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : OrderBot P] {x : P} {S : Set (Order.Ideal P)},
  x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type u_2}
  (U : ι → TopologicalSpace.Opens ↑X),
  F.IsSheaf → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Pairwise.diagram U).op F
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_subsingleton : ∀ (p : ℕ) (G : Type u_1) [inst : Group G] [Subsingleton G], IsPGroup p G
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_induction : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (p : β → Prop),
  (∀ (a b : β), p a → p b → p (a * b)) → p 1 → (∀ x ∈ s, p (f x)) → p (s.noncommProd f comm)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Any regular additive Haar measure is invariant under negation in an abelian group.  -/
MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_regular : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G]
  [μ.Regular], μ.IsNegInvariant
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.map_comp_comul_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] [inst_7 : FunLike F A B] [inst_8 : CoalgHomClass F R A B] (f : F) (x : A),
  (TensorProduct.map ↑f ↑f) (CoalgebraStruct.comul x) = CoalgebraStruct.comul (f x)
-- Mathlib.Data.NNReal.Basic
NNReal.finset_sup_mul : ∀ {α : Type u_3} (s : Finset α) (f : α → NNReal) (r : NNReal), s.sup f * r = s.sup fun a => f a * r
-- Std.Async.System
Std.Async.System.CPUInfo.mk.sizeOf_spec : ∀ (model : String) (speed : ℕ) (times : Std.Async.System.CPUTimes),
  sizeOf { model := model, speed := speed, times := times } = 1 + sizeOf model + sizeOf speed + sizeOf times
-- Mathlib.Algebra.Polynomial.Derivative
Finset.range.eq_1 : ∀ (n : ℕ), Finset.range n = { val := Multiset.range n, nodup := ⋯ }
-- Mathlib.Algebra.Divisibility.Prod
instDecompositionMonoidProd : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Semigroup G₁] [inst_1 : Semigroup G₂] [DecompositionMonoid G₁]
  [DecompositionMonoid G₂], DecompositionMonoid (G₁ × G₂)
-- Init.Data.String.Bootstrap
String.instInhabited : Inhabited String
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp_add : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [inst_4 : AddCommMonoid γ] [inst_5 : Preorder γ] [inst_6 : IsOrderedAddMonoid β]
  [inst_7 : IsOrderedAddMonoid γ] (g : β →+o γ) (f₁ f₂ : α →+o β), g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- A canonical functor from the free category on the refl quiver underlying a 2-truncated
simplicial set `V` to its homotopy category.  -/
SSet.Truncated.HomotopyCategory.quotientFunctor : (V : SSet.Truncated 2) → CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (SSet.OneTruncation₂ V)) V.HomotopyCategory
-- Init.Data.UInt.Lemmas
UInt32.ofNat_one : UInt32.ofNat 1 = 1
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is a subset `s` of an `R`-module such that `a • x + b • y ∈ s` whenever `a, b > 0`
and `x, y ∈ s`.  -/
ConvexCone : (R : Type u_2) → (M : Type u_4) → [Semiring R] → [PartialOrder R] → [AddCommMonoid M] → [SMul R M] → Type u_4
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.limitMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections],
  MonCat.limitMonoid F =
    {
      mul := fun x y =>
        (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections).symm.invFun
          ((equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections).symm.toFun x *
            (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections).symm.toFun y),
      mul_assoc := ⋯, one := (equivShrink ↑(F.comp (CategoryTheory.forget MonCat)).sections).symm.invFun 1,
      one_mul := ⋯, mul_one := ⋯, npow := fun n x => x ^ n, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindNatIso_inv_app : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G)
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (X : Rep.{max u w, u, v} k ↥S),
  (Rep.indCoindNatIso k S).inv.app X = X.indCoindIso.inv
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- A linear independent family of `finrank K V` vectors forms a basis.  -/
basisOfLinearIndependentOfCardEqFinrank : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {ι : Type u_1} →
            [inst_3 : Fintype ι] →
              [Nonempty ι] →
                {b : ι → V} → LinearIndependent K b → Fintype.card ι = Module.finrank K V → Module.Basis ι K V
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.withSynthesizeImp : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.Term.PostponeBehavior → Lean.Elab.TermElabM α
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal)
  (π₀ : BoxIntegral.Prepartition I),
  (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Submonoid M), s.saturation = sInf {t | s ≤ t.toSubmonoid}
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.fun_inv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X Y : D) (f : X ⟶ Y),
  e.functor.map (e.inverse.map f) =
    CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub.eq_3 : ∀ (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote),
  (e₁.oadd n₁ a₁).sub (e₂.oadd n₂ a₂) =
    match e₁.cmp e₂ with
    | Ordering.lt => 0
    | Ordering.gt => e₁.oadd n₁ a₁
    | Ordering.eq =>
      match ↑n₁ - ↑n₂ with
      | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
      | k.succ => e₁.oadd k.succPNat a₁
-- Mathlib.CategoryTheory.MorphismProperty.Descent
/-- Alternative constructor for `CodescendsAlong` using `HasPullback`.  -/
CategoryTheory.MorphismProperty.DescendsAlong.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.RespectsIso],
  (∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasPullback f g],
      Q f → P (CategoryTheory.Limits.pullback.fst f g) → P g) →
    P.DescendsAlong Q
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.ext : ∀ (𝕜 : Type u) (A : Type v) [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), a.toProd = b.toProd → a = b
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.instPartialOrderSubfunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} → PartialOrder (CategoryTheory.Subfunctor F)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.liftAux.smul : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ : MultilinearMap R s E} (r : R) (x : PiTensorProduct R fun i => s i),
  (PiTensorProduct.liftAux φ) (r • x) = r • (PiTensorProduct.liftAux φ) x
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_uIoo_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.uIoo (Fin.natAdd m i) (Fin.natAdd m j) = Set.uIoo i j
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.CheckCoverageResult.missing.injEq : ∀ (pos pos_1 : List ℕ),
  (Lean.Meta.Grind.CheckCoverageResult.missing pos = Lean.Meta.Grind.CheckCoverageResult.missing pos_1) = (pos = pos_1)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.opcyclesMap'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.opcyclesMap' φ h₁.right h₂.right = γ.right.φQ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_zpow_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {m n : ℤ}, 1 < a → (a ^ m ≤ a ^ n ↔ m ≤ n)
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
NormedRing.algEquivComplexOfComplete.congr_simp : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
  (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0), NormedRing.algEquivComplexOfComplete hA = NormedRing.algEquivComplexOfComplete hA
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowHom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (H : ∀ (j : ι), ∃ i, c.Rel i j),
  HomologicalComplex.homotopyCofiber.mapArrowHom φ φ H (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk φ)) =
    CategoryTheory.CategoryStruct.id (HomologicalComplex.homotopyCofiber φ)
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorZero_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_2) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).hom.app X =
    ((CategoryTheory.shiftFunctorZero C A).inv.app (Opposite.unop X)).op
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf'_product_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset β} {t : Finset γ}
  (h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).inf' h f = t.inf' ⋯ fun i' => s.inf' ⋯ fun i => f (i, i')
-- Mathlib.Data.PNat.Find
PNat.find_le : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] {n : ℕ+} {h : ∃ n, p n}, p n → PNat.find h ≤ n
-- Mathlib.CategoryTheory.Square
CategoryTheory.NatTrans.mapSquare_app_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C),
  ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₄ = τ.app sq.X₄