mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ofSubsingleton_apply_apply : ∀ (R : Type uR) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : Subsingleton ι] (i : ι)
  (f : M₂ →ₗ[R] M₃) (x : ι → M₂), ((MultilinearMap.ofSubsingleton R M₂ M₃ i) f) x = f (x i)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_hom_rel : ∀ {ι : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset ι)
  {r : M → N → Prop} {f : ι → M} {g : ι → N},
  r 1 1 → (∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)) → r (Multiset.map f s).prod (Multiset.map g s).prod
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.nhds_zero_eq_map_ofPre : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Zero (R i)]
  [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (R i)],
  (∀ (i : ι), IsOpen ↑(B i)) →
    ∀ (hT : Filter.cofinite ≤ Filter.principal T),
      nhds (RestrictedProduct.inclusion R (fun i => ↑(B i)) hT 0) =
        Filter.map (RestrictedProduct.inclusion R (fun i => ↑(B i)) hT) (nhds 0)
-- Init.Data.UInt.Lemmas
UInt64.add_eq_right : ∀ {a b : UInt64}, a + b = b ↔ a = 0
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_top : nhds ⊤ = ⨅ a, ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.ofMulHom_coe : ∀ {α : Type u} [inst : Monoid α], ⇑FreeAbelianGroup.ofMulHom = FreeAbelianGroup.of
-- Std.Time.Zoned.Database.TZdb
/-- Represents a Time Zone Database (TZdb) configuration with paths to local and general timezone data.
 -/
Std.Time.Database.TZdb : Type
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The coercion from the rationals to its completion along an infinite place is `Rat.cast`.  -/
NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv : ∀ (v : NumberField.InfinitePlace ℚ) (x : WithAbs ↑v), ↑((WithAbs.equiv ↑v) x) = { toCompletion := ↑x }
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.mkHomFromDouble_f₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁) {K : HomologicalComplex C c} (φ₀ : X₀ ⟶ K.X i₀) (φ₁ : X₁ ⟶ K.X i₁)
  (comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
  (hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0),
  (HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁ =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₁ f hi₀₁ h).hom φ₁
-- Lean.Parser.Types
Lean.Parser.ParserInfo.collectTokens : Lean.Parser.ParserInfo → List Lean.Parser.Token → List Lean.Parser.Token
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {S : CategoryTheory.Sieve X} {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows},
  x.Compatible → x.SieveCompatible
-- Mathlib.RingTheory.Polynomial.RationalRoot
/-- **Integral root theorem**:
if `r : f.codomain` is a root of a monic polynomial over the ufd `A`,
then `r` is an integer  -/
isInteger_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 → IsLocalization.IsInteger A r
-- Mathlib.Data.ENat.Lattice
ENat.sSup_mul : ∀ {s : Set ℕ∞} {a : ℕ∞}, sSup s * a = ⨆ b ∈ s, b * a
-- Init.Data.List.Sublist
List.dropLast_prefix : ∀ {α : Type u_1} (l : List α), l.dropLast <+: l
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive commutative monoid form
an additive commutative group.  -/
AddUnits.instAddCommGroupAddUnits : {α : Type u_1} → [inst : AddCommMonoid α] → AddCommGroup (AddUnits α)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α),
  Std.DTreeMap.Internal.Impl.leaf.get? k = none
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_le_of_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [inst : Fintype ι],
  J ∈ π → J.distortion ≤ π.distortion
-- Init.Data.BitVec.Lemmas
BitVec.toInt_eq_toNat_of_lt : ∀ {n : ℕ} {x : BitVec n}, 2 * x.toNat < 2 ^ n → x.toInt = ↑x.toNat
-- Mathlib.Data.Set.Prod
preimage_map_fst_pullbackDiagonal : ∀ {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} {f : X → Y} {g : Z → Y},
  Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f = Function.pullbackDiagonal Function.Pullback.snd
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_pow : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ), DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
-- Lean.Data.Lsp.CodeActions
/-- A short, human-readable, title for this code action.  -/
Lean.Lsp.CodeAction.title : Lean.Lsp.CodeAction → String
-- Mathlib.Combinatorics.Matroid.Basic
/-- A `RankFinite` matroid is one whose bases are finite  -/
Matroid.RankFinite : {α : Type u_1} → Matroid α → Prop
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] (X : CategoryTheory.Functor Cᵒᵖ A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Limits.FormalCoproduct.evalOpCompInlIsoId C A).hom.app X).app X_1 =
    CategoryTheory.Limits.Pi.π (fun i => X.obj X_1) PUnit.unit
-- Mathlib.GroupTheory.Nilpotent
/-- The range of a surjective homomorphism from a nilpotent group is nilpotent.  -/
Group.nilpotent_of_surjective : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [h : Group.IsNilpotent G] (f : G →* G'),
  Function.Surjective ⇑f → Group.IsNilpotent G'
-- Mathlib.Topology.Instances.Real.Lemmas
Real.exists_seq_rat_strictAnti_tendsto : ∀ (x : ℝ), ∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < ↑(u n)) ∧ Filter.Tendsto (fun x => ↑(u x)) Filter.atTop (nhds x)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.intCast_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ), ↑z1 = ↑z2 ↔ z1 = z2
-- Init.Data.List.MinMaxOn
List.le_apply_get_maxOn?_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} {x : α} (h : x ∈ xs), f x ≤ f ((List.maxOn? f xs).get ⋯)
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_apply_inl_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (b : β),
  (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inr b)))) = toLex (Sum.inr (toLex (Sum.inl b)))
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableWithinAt.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} {M : ι → Type u_6}
  [inst_3 : (i : ι) → NormedAddCommGroup (M i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  DifferentiableWithinAt 𝕜 c s x → ∀ (u : (i : ι) → M i), DifferentiableWithinAt 𝕜 (fun y => (c y) u) s x
-- Std.Data.DTreeMap.Basic
/-- Internal implementation detail of the tree map.  -/
Std.DTreeMap.wf : ∀ {α : Type u} {β : α → Type v} {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1} (self : Std.DTreeMap α β cmp),
  self.inner.WF
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset : ∀ {A B : GrpCat} (f : A ⟶ B) (x : ↑B) (y : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)),
  ((GrpCat.SurjectiveOfEpiAuxs.g f) x) (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset y) =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨x • ↑y, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_log : ∀ {a b : ℝ}, ∫ (s : ℝ) in a..b, Real.log s = b * Real.log b - a * Real.log a - b + a
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodProdProdComm_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (mnmn : (M × M₂) × M₃ × M₄),
  (LinearEquiv.prodProdProdComm R M M₂ M₃ M₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
-- Lean.Parser.Extension
/-- A builtin parser attribute that can be extended by users.  -/
Lean.Parser.registerBuiltinDynamicParserAttribute : Lean.Name → Lean.Name → autoParam Lean.Name Lean.Parser.registerBuiltinDynamicParserAttribute._auto_1 → IO Unit
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y}
  (h : CategoryTheory.Limits.IsColimit s) {f g : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.inl f = CategoryTheory.CategoryStruct.comp s.inl g →
    CategoryTheory.CategoryStruct.comp s.inr f = CategoryTheory.CategoryStruct.comp s.inr g → f = g
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.vectorBundle : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι),
  VectorBundle R F Z.Fiber
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.instAddHomComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) → [R.Additive] → {u v : CategoryTheory.Comma L R} → Add (u ⟶ v)
-- Mathlib.RingTheory.Localization.Basic
/-- If `S`, `Q` are localizations of `R` and `P` at submonoids `M`, `T` respectively,
an isomorphism `h : R ≃ₐ[A] P` such that `h(M) = T` induces an isomorphism of localizations
`S ≃ₐ[A] Q`.  -/
IsLocalization.algEquivOfAlgEquiv : {A : Type u_4} →
  [inst : CommSemiring A] →
    {R : Type u_5} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra A R] →
          {M : Submonoid R} →
            (S : Type u_6) →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra A S] →
                  [inst_5 : Algebra R S] →
                    [IsScalarTower A R S] →
                      [IsLocalization M S] →
                        {P : Type u_7} →
                          [inst_8 : CommSemiring P] →
                            [inst_9 : Algebra A P] →
                              {T : Submonoid P} →
                                (Q : Type u_8) →
                                  [inst_10 : CommSemiring Q] →
                                    [inst_11 : Algebra A Q] →
                                      [inst_12 : Algebra P Q] →
                                        [IsScalarTower A P Q] →
                                          [IsLocalization T Q] → (h : R ≃ₐ[A] P) → Submonoid.map h M = T → S ≃ₐ[A] Q
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The functor `ModuleCat R ⥤ ModuleCat R` which sends a module to its
`n`th exterior power.  -/
ModuleCat.exteriorPower.functor : (R : Type u) → [inst : CommRing R] → ℕ → CategoryTheory.Functor (ModuleCat R) (ModuleCat R)
-- Mathlib.CategoryTheory.Galois.Basic
/-- A functor is said to preserve connectedness if whenever `X : C` is connected,
also `F.obj X` is connected.  -/
CategoryTheory.PreGaloisCategory.PreservesIsConnected : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {D : Type v₁} → [inst_1 : CategoryTheory.Category.{v₂, v₁} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Order.SupIndep
sSupIndep_iff : ∀ {α : Type u_5} [inst : CompleteLattice α] (s : Set α), sSupIndep s ↔ iSupIndep Subtype.val
-- Init.NotationExtra
unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Order.Part
Monotone.partSeq : ∀ {α : Type u_1} [inst : Preorder α] {β γ : Type u_4} {f : α → Part (β → γ)} {g : α → Part β},
  Monotone f → Monotone g → Monotone fun x => f x <*> g x
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalWithReducible : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- An element is in the closure of a two-element set if it is a linear combination of those two
elements.  -/
Submonoid.mem_closure_pair : ∀ {A : Type u_4} [inst : CommMonoid A] (a b c : A), c ∈ Submonoid.closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.sup_comm : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), a ⊔ b = b ⊔ a
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioi_pred_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (Order.pred a) = Set.Ici a
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMapTgt.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C],
  CategoryTheory.SmallObject.functorMapTgt f τ =
    CategoryTheory.Limits.Sigma.map'
      (fun x =>
        { i := x.i, t := CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.Arrow.Hom.left τ),
          b := CategoryTheory.CategoryStruct.comp x.b (CategoryTheory.Arrow.Hom.right τ), w := ⋯ })
      fun x => CategoryTheory.CategoryStruct.id (CategoryTheory.SmallObject.functorObjTgtFamily f πX x)
-- Mathlib.CategoryTheory.Functor.Currying
/-- The equivalence of functor categories given by flipping.  -/
CategoryTheory.Functor.flipping : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor C (CategoryTheory.Functor D E) ≌
              CategoryTheory.Functor D (CategoryTheory.Functor C E)
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves limits of some shape `J` if
`V` has limits of shape `J` and `F` preserves limits of shape `J`.  -/
Action.Functor.mapActionPreservesLimitsOfShapeOfPreserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  {J : Type u_5} [inst_3 : CategoryTheory.Category.{v_3, u_5} J] [CategoryTheory.Limits.PreservesLimitsOfShape J F]
  [CategoryTheory.Limits.HasLimitsOfShape J V], CategoryTheory.Limits.PreservesLimitsOfShape J (F.mapAction G)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₃`, graded objects `X₁ : GradedObject I₁ C₁`,
`X₂ : GradedObject I₂ C₂`, `X₃ : GradedObject I₃ C₃`, and a map `p : I₁ × I₂ × I₃ → J`,
this is the `J`-graded object sending `j` to the coproduct of
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)` for `p ⟨i₁, i₂, i₃⟩ = k`.  -/
CategoryTheory.GradedObject.mapTrifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) →
                  {I₁ : Type u_7} →
                    {I₂ : Type u_8} →
                      {I₃ : Type u_9} →
                        {J : Type u_10} →
                          (p : I₁ × I₂ × I₃ → J) →
                            (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                              (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                  [((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj
                                            X₃).HasMap
                                        p] →
                                    CategoryTheory.GradedObject J C₄
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.alwaysInline.sizeOf_spec : sizeOf Lean.Compiler.InlineAttributeKind.alwaysInline = 1
-- Lean.Declaration
Lean.ConstantInfo.recInfo.sizeOf_spec : ∀ (val : Lean.RecursorVal), sizeOf (Lean.ConstantInfo.recInfo val) = 1 + sizeOf val
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.normalizer_addCommutator_ge_right : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), H₂ ≤ AddSubgroup.normalizer ↑⁅H₁, H₂⁆
-- Mathlib.Topology.Maps.Basic
Topology.IsCoinducing.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsCoinducing f → Continuous f
-- Mathlib.Topology.Piecewise
continuous_if_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} (p : Prop)
  [inst_2 : Decidable p], (p → Continuous f) → (¬p → Continuous g) → Continuous fun a => if p then f a else g a
-- Mathlib.Data.Finmap
Finmap.liftOn₂_toFinmap : ∀ {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ s₂ : AList β) (f : AList β → AList β → γ)
  (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entries → b₁.entries.Perm b₂.entries → f a₁ b₁ = f a₂ b₂),
  s₁.toFinmap.liftOn₂ s₂.toFinmap f H = f s₁ s₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l}, (t.insertMany l)[k] = t[k]
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
CategoryTheory.Bicategory.eqToHom_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom η) h = CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- `Localization.localRingHom` specialized to a projection homomorphism from a product ring.  -/
Localization.AtPrime.mapPiEvalRingHom : {ι : Type u_4} →
  {R : ι → Type u_5} →
    [inst : (i : ι) → CommSemiring (R i)] →
      {i : ι} →
        (I : Ideal (R i)) →
          [inst_1 : I.IsPrime] → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I) →+* Localization.AtPrime I
-- Mathlib.Order.Filter.FilterProduct
/-- If `φ` is an ultrafilter then the ultraproduct is a linear order.  -/
Filter.Germ.instLinearOrder : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [LinearOrder β] → LinearOrder ((↑φ).Germ β)
-- Init.Data.Array.Basic
/-- See comment at `forIn'Unsafe`. This mirrors `mapMUnsafe`, threading the index `i`
and supplying the in-bounds proof via `lcProof`.  -/
Array.mapFinIdxMUnsafe : {α : Type u} →
  {β : Type v} → {m : Type v → Type w} → [Monad m] → (as : Array α) → ((i : ℕ) → α → i < as.size → m β) → m (Array β)
-- Mathlib.Algebra.Ring.BooleanRing
/-- Type synonym to view a Boolean ring as a Boolean algebra.  -/
AsBoolAlg : Type u_4 → Type u_4
-- Mathlib.Topology.Sheaves.Flasque
_private.Mathlib.Topology.Sheaves.Flasque.0.TopCat.Sheaf.IsFlasque.epi_of_shortExact.match_1_7.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.mono_left : ∀ {α : Type u_1} {β : Type u_2} {G H K : Graph α β}, H ≤ K → K ≤ G → H ≤s G → K ≤s G
-- Mathlib.Topology.Clopen
isClopen_range_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClopen (Set.range Sum.inr)
-- Mathlib.Topology.Algebra.AsymptoticCone
/-- If `v` is in the asymptotic cone of a convex set `s`, then for every interior point `p`, the ray
of direction `v` starting from `p` is contained in `s`.  -/
Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : TopologicalSpace k] [OrderTopology k] [inst_5 : AddCommGroup V] [inst_6 : Module k V]
  [inst_7 : TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V} {c : k} {v p : V},
  Convex k s → 0 ≤ c → s ∈ nhds p → v ∈ asymptoticCone k s → c • v +ᵥ p ∈ s
-- Std.Do.SPred.SPred
Std.Do.SPred.forall_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {α : Sort u_1} {P : α → Std.Do.SPred (σ :: σs)},
  Std.Do.SPred.forall P s = spred(∀ a, P a s)
-- Mathlib.Data.Set.Subsingleton
/-- **Alias** of the reverse direction of `Set.not_subsingleton_iff`. -/
Set.Nontrivial.not_subsingleton : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ¬s.Subsingleton
-- Mathlib.RingTheory.TensorProduct.Pi
/-- Variant of `Algebra.TensorProduct.piRight` with constant factors.  -/
Algebra.TensorProduct.piScalarRight : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra S A] →
                  [inst_6 : IsScalarTower R S A] →
                    (ι : Type u_4) → [Fintype ι] → [DecidableEq ι] → TensorProduct R A (ι → R) ≃ₐ[S] ι → A
-- Mathlib.Data.Seq.Computation
Computation.Results.terminates : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → s.Terminates
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.sum_Icc_mu_left : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] (a b : α), ∑ x ∈ Finset.Icc a b, (IncidenceAlgebra.mu 𝕜) x b = if a = b then 1 else 0
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_val_nd : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).val = s.val.ndunion t.val
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_inv_mul_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α} [MulRightMono α],
  a / b ≤ a⁻¹ * b ↔ a ≤ b