mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_mono : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {S₁ S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B},
  S₁ ≤ S₂ → StarSubalgebra.map f S₁ ≤ StarSubalgebra.map f S₂
-- Mathlib.Data.Multiset.Fintype
Multiset.prod_eq_prod_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommMonoid α] (m : Multiset α), m.prod = ∏ x ∈ m.toEnumFinset, x.1
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.snd B C).mapId x).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.associator_inv_hom : ∀ {R : Type u} [inst : CommRing R] (A B C : CommAlgCat R),
  CommAlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator A B C).inv =
    ↑(Algebra.TensorProduct.assoc R R R ↑A ↑B ↑C).symm
-- Mathlib.Topology.NhdsWithin
pure_le_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, a ∈ s → pure a ≤ nhdsWithin a s
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableUniformlyOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  SummableUniformlyOn f Set.univ ↔ SummableUniformly f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.startLine : Lean.Lsp.FoldingRange → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The coproduct of the horn inclusions corresponding to all the cells
of rank `j` for a rank function for a proper pairing of a subcomplex
of a simplicial set.  -/
SSet.Subcomplex.Pairing.RankFunction.m : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) → [inst_1 : P.IsProper] → (j : ι) → f.sigmaHorn j ⟶ f.sigmaStdSimplex j
-- Mathlib.RingTheory.FiniteType
AlgHom.FiniteType.comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {g : B →ₐ[R] C} {f : A →ₐ[R] B}, g.FiniteType → f.FiniteType → (g.comp f).FiniteType
-- Mathlib.Data.Finsupp.Notation
Finsupp.fun₀.matchAlts : Lean.Parser.Parser
-- Mathlib.Data.Fin.Tuple.Basic
Fin.forall_iff_castSucc : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∀ (i : Fin (n + 1)), P i) ↔ P (Fin.last n) ∧ ∀ (i : Fin n), P i.castSucc
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α}, G.egirth = ⊤ ↔ G.IsAcyclic
-- Mathlib.Algebra.Group.EvenFunction
/-- An odd function `f` satisfies `f (-x) = -f x`.  -/
Function.Odd.eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : Neg β] {f : α → β}, Function.Odd f → ∀ (x : α), f (-x) = -f x
-- Mathlib.Algebra.Algebra.Basic
/-- **Alias** of `Module.isTorsionFree_iff_algebraMap_injective`. -/
NoZeroSMulDivisors.iff_algebraMap_injective : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [IsDomain R] [IsDomain A],
  Module.IsTorsionFree R A ↔ Function.Injective ⇑(algebraMap R A)
-- Mathlib.Tactic.Push
_private.Mathlib.Tactic.Push.0.Mathlib.Tactic.Push.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.Push.Config
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_of_eventuallyEq_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → g =ᶠ[nhdsWithin x s] f → x ∈ s → ContinuousWithinAt g s x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instIsIsoHomHomMon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.AddGrp C} {f : G ⟶ H} [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom.hom
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff`.

---

The natural map from `G →₀ k` to `SkewMonoidAlgebra k G`.  -/
SkewMonoidAlgebra.ofFinsupp : {k : Type u_1} → {G : Type u_2} → [inst : Zero k] → (G →₀ k) → SkewMonoidAlgebra k G
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.add_const : ∀ {l₁ l₂ : Lean.Omega.LinearCombo}, (l₁ + l₂).const = l₁.const + l₂.const
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Composition of left-translation shifts corresponds to multiplication in the monoid `G`.  -/
SymbolicDynamics.FullShift.mulShift_mul : ∀ {A : Type u_1} {G : Type u_2} [inst : Monoid G] (g₁ g₂ : G) (x : G → A),
  SymbolicDynamics.FullShift.mulShift (g₁ * g₂) x =
    SymbolicDynamics.FullShift.mulShift g₂ (SymbolicDynamics.FullShift.mulShift g₁ x)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : AddZeroClass M] (S : ι → AddSubmonoid M), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- If a category has all products then in particular it has finite products.
 -/
CategoryTheory.Limits.hasFiniteProducts_of_hasProducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
HasCardinalLT.of_surjective : ∀ {X : Type u} {κ : Cardinal.{v}},
  HasCardinalLT X κ → ∀ {Y : Type u'} (f : X → Y), Function.Surjective f → HasCardinalLT Y κ
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instCommGroupCoeOfSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → CommGroup (R i)] →
              [∀ (i : ι), SubgroupClass (S i) (R i)] → CommGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → P 2 = 0 → Q 2 = 0 → P ≈ Q
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.minKey! ∈ t
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.numNodes : Lean.PersistentHashMap.Stats → ℕ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_map_nhds_eq : ∀ {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) (a : A), Filter.map (⇑e.symm) (nhds (e a)) = nhds a
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Algebra.IsQuadraticExtension.finrank_eq_two : ∀ (R : Type u_2) (S : Type u_3) [inst : CommSemiring R] [inst_1 : StrongRankCondition R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [Algebra.IsQuadraticExtension R S], Module.finrank R S = 2
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_eq_zero_of_not_squarefree : ∀ {n : ℕ}, ¬Squarefree n → ArithmeticFunction.moebius n = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.mk.inj : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  {map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w}
  {hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size}
  {map_1 : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w}
  {hbound_1 :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map_1) (h2 : i < k.w),
      (map_1.get k h1)[i].gate < aig.decls.size},
  { map := map, hbound := hbound } = { map := map_1, hbound := hbound_1 } → map = map_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h) = h
-- Std.Data.DHashMap.Raw
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `none`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.Raw.getEntry? : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → Option ((a : α) × β a)
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The functor `Sigma.map` applied to a composition is a composition of functors.  -/
CategoryTheory.Sigma.mapComp : {I : Type w₁} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₂} →
        {K : Type w₃} →
          (f : K → J) →
            (g : J → I) →
              (CategoryTheory.Sigma.map (fun x => C (g x)) f).comp (CategoryTheory.Sigma.map C g) ≅
                CategoryTheory.Sigma.map C (g ∘ f)
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.mkAddHom.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), c.mkAddHom = { toFun := AddCon.toQuotient, map_add' := ⋯ }
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_stoppedProcess_of_le_right : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  σ ≤ τ → MeasureTheory.stoppedProcess (MeasureTheory.stoppedProcess u τ) σ = MeasureTheory.stoppedProcess u σ
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.divInvMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : DivInvMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.divInvMonoid f hf one mul inv div npow zpow =
    { toMonoid := Function.Injective.monoid f hf one mul npow, toInv := inst_3, toDiv := inst_4,
      zpow := fun n x => x ^ n, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_add_right_ne_zero : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant],
  μ s ≠ 0 → ∀ (y : G), μ ((fun x => x + y) ⁻¹' s) ≠ 0
-- Init.Data.List.Lex
List.le_append_left : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] {l₁ l₂ : List α}, l₁ ≤ l₁ ++ l₂
-- Mathlib.Topology.EMetricSpace.Defs
instWeakPseudoEMetricSpaceOrderDual : {X : Type u_1} → [inst : TopologicalSpace X] → [WeakPseudoEMetricSpace X] → WeakPseudoEMetricSpace Xᵒᵈ
-- Init.Data.List.MapIdx
List.mapFinIdx.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : ℕ) → α → i < as.length → β) (acc : Array β) (a : α)
  (as_1 : List α) (a_1 : (a :: as_1).length + acc.size = as.length),
  List.mapFinIdx.go as f (a :: as_1) acc a_1 = List.mapFinIdx.go as f as_1 (acc.push (f acc.size a ⋯)) ⋯
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.exists_le_minimal : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α}, s.IsPWO → a ∈ s → ∃ b ≤ a, Minimal (fun x => x ∈ s) b
-- Std.Http.Test.Helpers
/-- Like `check` wrapped in a wall-clock timeout.
Required when the test involves streaming, async timers, or keep-alive behavior.
 -/
Std.Http.Internal.Test.checkTimed : String →
  optParam ℕ 2000 →
    String →
      Std.Http.Internal.Test.TestHandler →
        (ByteArray → IO Unit) → optParam Std.Http.Config Std.Http.Internal.Test.defaultConfig → IO Unit
-- Std.Http.Server.Config
/-- Whether to automatically generate the `Date` header in responses.
 -/
Std.Http.Config.generateDate : Std.Http.Config → Bool
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The forgetful functor from sheaves of modules over sheaf of ring `R` to sheaves of `R(X)`-module
when `X` is initial.
 -/
SheafOfModules.forgetToSheafModuleCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        (X : Cᵒᵖ) →
          CategoryTheory.Limits.IsInitial X →
            CategoryTheory.Functor (SheafOfModules R) (CategoryTheory.Sheaf J (ModuleCat ↑(R.obj.obj X)))
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_div_left : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (a : G), IsOpenMap fun x => a / x
-- Mathlib.Algebra.Module.Injective
Module.Baer.extensionOfMax_to_submodule_eq_top : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)],
  Module.Baer R Q → (Module.Baer.extensionOfMax i f).domain = ⊤
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.natPow_zero_natMod_zero : ∀ {a : ℕ}, (a.pow 0).mod 0 = 1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_mul_const_iff : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [ContinuousMul β] {c : β},
  c ≠ 0 → ((Asymptotics.SuperpolynomialDecay l k fun n => f n * c) ↔ Asymptotics.SuperpolynomialDecay l k f)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.dirac_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (x : M) (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ], (MeasureTheory.Measure.dirac x).mconv μ = MeasureTheory.Measure.map (fun y => x * y) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.instSubsingleton : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S},
  Subsingleton (h.LiftStruct g₁ g₂ b)
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.mk.inj : ∀ {fvarId newFVarId fvarId_1 newFVarId_1 : Lean.FVarId},
  { fvarId := fvarId, newFVarId := newFVarId } = { fvarId := fvarId_1, newFVarId := newFVarId_1 } →
    fvarId = fvarId_1 ∧ newFVarId = newFVarId_1
-- Std.Http.Data.Status
Std.Http.Status.requestTimeout.sizeOf_spec : sizeOf Std.Http.Status.requestTimeout = 1
-- Init.Data.UInt.Lemmas
UInt32.ofFin_uint16ToFin : ∀ (n : UInt16), UInt32.ofFin (Fin.castLE UInt16.toFin_toUInt32._proof_1 n.toFin) = n.toUInt32
-- Mathlib.RingTheory.KrullDimension.Basic
/-- A ring has krull dimension at most zero if and only if all minimal primes are maximal.  -/
Ring.krullDimLE_zero_iff_forall_minimalPrimes_isMaximal : ∀ {R : Type u_1} [inst : CommSemiring R], Ring.KrullDimLE 0 R ↔ ∀ I ∈ minimalPrimes R, I.IsMaximal
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoColimitUncurryWhiskeringLeft₂_hom : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasColimit K₁]
  [inst_7 : CategoryTheory.Limits.HasColimit K₂] (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
      (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).hom =
    CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.Limits.colimit.ι K₁ j.1)).app (K₂.obj j.2))
      ((G.obj (CategoryTheory.Limits.colimit K₁)).map (CategoryTheory.Limits.colimit.ι K₂ j.2))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instModule : {ι : 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)] → Module R (PiTensorProduct R fun i => s i)
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.sub : ∀ {M : Type u_1} {E : Type u_2} [inst : Monoid M] [inst_1 : AddGroup E] [inst_2 : DistribMulAction M E]
  [inst_3 : Bornology M] {s₁ s₂ t₁ t₂ : Set E}, Absorbs M s₁ t₁ → Absorbs M s₂ t₂ → Absorbs M (s₁ - s₂) (t₁ - t₂)
-- Mathlib.Order.Category.DistLat
/-- `OrderDual` as a functor.  -/
DistLat.dual : CategoryTheory.Functor DistLat DistLat
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.concreteCategory : CategoryTheory.ConcreteCategory FinPartOrd fun x1 x2 => ↑x1.toPartOrd →o ↑x2.toPartOrd
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t.keys → k ∈ t
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_one : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 1 → M), ∑ i, f i = f 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_eq_pow : ∀ (x y : ℂ), x.cpow y = x ^ y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β} {f : Option β → Option β}, (t.alter k f).getD k fallback = (f t[k]?).getD fallback
-- Mathlib.Order.Directed
Directed.mono_comp : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) {ι : Sort u_5} {rb : β → β → Prop} {g : α → β} {f : ι → α},
  (∀ ⦃x y : α⦄, r x y → rb (g x) (g y)) → Directed r f → Directed rb (g ∘ f)
-- Mathlib.Order.Category.BddOrd
/-- Turn a morphism in `BddOrd` back into a `BoundedOrderHom`.  -/
BddOrd.Hom.hom : {X Y : BddOrd} → X.Hom Y → BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd
-- Mathlib.Data.Fin.Fin2
Fin2.instInhabitedOfNatNat : Inhabited (Fin2 1)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.isPrime_comap : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {J : HomogeneousIdeal ℬ} [J.toIdeal.IsPrime],
  (HomogeneousIdeal.comap f J).toIdeal.IsPrime
-- Mathlib.Order.RelClasses
Order.Preimage.instIsEquiv : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [IsEquiv α r] {f : β → α}, IsEquiv β (f ⁻¹'o r)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_succ_le : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ n
-- Init.Data.SInt.Lemmas
Int64.toNat_toBitVec_of_le : ∀ {x : Int64}, 0 ≤ x → x.toBitVec.toNat = x.toNatClampNeg
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderComposition],
  (HomotopicalAlgebra.weakEquivalences C).RespectsIso
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hasForgetToSemiRingCat : CategoryTheory.HasForget₂ CommSemiRingCat SemiRingCat
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_countablePartitionSet : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) (a : α),
  MeasurableSet (MeasurableSpace.countablePartitionSet n a)
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `i` and then shifting by `-i` is the identity.  -/
CategoryTheory.shiftShiftNeg : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddGroup A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (X : C) → (i : A) → (CategoryTheory.shiftFunctor C (-i)).obj ((CategoryTheory.shiftFunctor C i).obj X) ≅ X
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.differentiableAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  DiffContOnCl 𝕜 f s → IsOpen s → x ∈ s → DifferentiableAt 𝕜 f x
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.supSum_union_add_supSum_infs : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 ℬ : Finset (Finset α)),
  AhlswedeZhang.supSum (𝒜 ∪ ℬ) + AhlswedeZhang.supSum (𝒜 ⊼ ℬ) = AhlswedeZhang.supSum 𝒜 + AhlswedeZhang.supSum ℬ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.hasCompactSupport' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (self : TestFunction Ω F n),
  HasCompactSupport self.toFun
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X X_1 X_2 : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap δ).app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.comp ((δ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X X_1)).app X_2)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((δ.app X).app X_1) (F.obj X_2))
        (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj X_1) (F.obj X_2)).hom)
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a left-open right-closed range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Roc.HasRcoIntersection : Type w → Type w
-- Init.Data.Nat.Div.Basic
Nat.div_eq_of_eq_mul_left : ∀ {n m k : ℕ}, 0 < n → m = k * n → m / n = k