mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.SpanRankOperations
Submodule.spanRank_baseChange_le : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Submodule R M),
  (Submodule.baseChange A N).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.subtype_comp_codRestrict : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {U : Submodule S M}
  {f : M →ₗ[S] M} (hf : LinearMap.IsProj U f), U.subtype ∘ₗ hf.codRestrict = f
-- Init.Data.String.Defs
String.toByteArray_empty : "".toByteArray = ByteArray.empty
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.get?_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.get? a = Std.Internal.List.getValueCast? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- If `𝒢` is discrete, so is its period subgroup.  -/
Subgroup.instDiscreteTopPeriods : ∀ {R : Type u_1} [inst : Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} [inst_1 : TopologicalSpace R] [IsTopologicalRing R]
  [T2Space R] [hG : DiscreteTopology ↥𝒢], DiscreteTopology ↥𝒢.periods
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [inst_4 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_5 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_6 :
    ∀ (X : A),
      CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A) {Z : A}
  (h : Φ.presheafFiber.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) h) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂)) h
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.of_hasBinaryCoproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierIntegral_continuousMultilinearMap_apply' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ι : Type u_4} {V : Type u_6} {W : Type u_7}
  [inst_2 : Fintype ι] [inst_3 : NormedAddCommGroup V] [inst_4 : NormedSpace ℝ V] [inst_5 : MeasurableSpace V]
  [BorelSpace V] [inst_7 : NormedAddCommGroup W] [inst_8 : NormedSpace ℝ W] {μ : MeasureTheory.Measure V}
  {L : V →L[ℝ] W →L[ℝ] ℝ} {M : ι → Type u_8} [inst_9 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_10 : (i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {w : W},
  MeasureTheory.Integrable f μ →
    (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) m =
      VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x => (f x) m) w
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.mk.sizeOf_spec : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] [inst_4 : SizeOf X] [inst_5 : SizeOf Y] (toFun : X → Y)
  (map_smul' : ∀ (m : M) (x : X), toFun (m • x) = φ m • toFun x), sizeOf { toFun := toFun, map_smul' := map_smul' } = 1
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- **Alias** of `FiberBundle.contMDiffAt_extend`. -/
FiberBundle.contMDiffAt_extend' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  {V : M → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F] {k : WithTop ℕ∞}
  {x : M} (σ₀ : V x), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x' => ⟨x', FiberBundle.extend F σ₀ x'⟩) x
-- Mathlib.LinearAlgebra.BilinearMap
/-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`.  -/
LinearMap.BilinMap : (R : Type u_2) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (Nₗ : Type u_8) →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid Nₗ] → [Module R M] → [Module R Nₗ] → Type (max u_8 u_5)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- A module `M` is precomplete with respect to an ideal `I` if every Cauchy sequence converges.  -/
IsPrecomplete : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Init.Control.Lawful.Instances
ReaderT.run_mk : ∀ {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (x : ρ → m α) (ctx : ρ), (ReaderT.mk x).run ctx = x ctx
-- Batteries.Control.Nondet.Basic
/-- Convert any value in the monad to the singleton nondeterministic value.  -/
Nondet.singletonM : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → m α → Nondet m α
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.toListAppend.eq_1 : ∀ {α : Type u} (as : Array α) (l : List α), as.toListAppend l = Array.foldr List.cons l as
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.hasForget : CategoryTheory.ConcreteCategory Pointed fun X Y => { f // f X.point = Y.point }
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.smithNormalFormCoeffs.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] {N N_1 : Submodule R M} (e_N : N = N_1) [inst_5 : Finite ι]
  (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ (h : Module.finrank R ↥N = Module.finrank R M) (a a_1 : ι),
      a = a_1 → Submodule.smithNormalFormCoeffs b h a = Submodule.smithNormalFormCoeffs b_1 ⋯ a_1
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.toUpperSet_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Topology.WithUpperSet.toUpperSet a ≤ Topology.WithUpperSet.toUpperSet b ↔ a ≤ b
-- Mathlib.RingTheory.KrullDimension.Polynomial
/-- If `R` is Noetherian, `dim R[X] = dim R + 1`.  -/
Polynomial.ringKrullDim_of_isNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R], ringKrullDim (Polynomial R) = ringKrullDim R + 1
-- Mathlib.Algebra.Order.Nonneg.Field
NNRat.cast_nonneg : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (q : ℚ≥0), 0 ≤ ↑q
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instFaithfulSMul : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], FaithfulSMul R M
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.range_embedProduct : ∀ {α : Type u} [inst : AddMonoid α],
  Set.range ⇑(AddUnits.embedProduct α) = {p | p.1 + AddOpposite.unop p.2 = 0 ∧ AddOpposite.unop p.2 + p.1 = 0}
-- Lean.Meta.Sym.Canon
/-- Canonicalize a decidable instance without checking the cache.
Given a term `e` of the form `@Grind.nestedDecidable prop inst`, where `g` is the constant `Grind.nestedDecidable`,
we canonicalize it as follows:
1- We recursively canonicalize the proposition `prop`.
2- Try to resynthesize the instance, but keep the original one in case of failure since users often
provide them using `haveI`.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInstDec' : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_apply_inr : ∀ {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s] (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
-- Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
/-- The sheaf of continuous maps `U ↦ C(U, ℤ_[ℓ])` on the pro-étale site. This the coefficient
sheaf for `ℓ`-adic cohomology.
[Definition 6.8.1.][proetale2015]
 -/
AlgebraicGeometry.Scheme.ellAdicSheaf : (X : AlgebraicGeometry.Scheme) →
  (ℓ : ℕ) → [Fact (Nat.Prime ℓ)] → CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.ProEt.topology X) Ab
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_sup : ∀ {V : Type u} (G₁ G₂ : SimpleGraph V), (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_le : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β} [inst : LE β], ↑f ≤ ↑g ↔ f ≤ᶠ[l] g
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- A single vertex, in terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.points i =
    (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.pointWeightsWithCircumcenter i)
-- Mathlib.Condensed.Explicit
/-- A condensed object regarded as a sheaf on `Profinite` satisfies the equalizer condition.  -/
Condensed.equalizerCondition_profinite : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A),
  CategoryTheory.regularTopology.EqualizerCondition X.obj
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.HasSmallObjectArgument.exists_cardinal : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {I : CategoryTheory.MorphismProperty C}
  [self : I.HasSmallObjectArgument], ∃ κ, ∃ (x : Fact κ.IsRegular), ∃ x_1, I.IsCardinalForSmallObjectArgument κ
-- Mathlib.Order.RelSeries
/-- Given the series `a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ`, the series `a₀ -r→ … -r→ aᵢ`.  -/
RelSeries.take : {α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → Fin (p.length + 1) → RelSeries r
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.isoClosure_strictLimitsClosureIter_eq_limitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular],
  (∀ (a : α), HasCardinalLT (J a) κ) → (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J
-- Init.Data.Order.Ord
Std.ReflCmp.mk : ∀ {α : Type u} {cmp : α → α → Ordering}, (∀ {a : α}, cmp a a = Ordering.eq) → Std.ReflCmp cmp
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.entryAddMonoidHom_comp_mapMatrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  (f : α →+ β) (i : m) (j : n),
  (Matrix.entryAddMonoidHom β i j).comp f.mapMatrix = f.comp (Matrix.entryAddMonoidHom α i j)
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A submodule of a free `R`-module of finite rank is also a free `R`-module of finite rank,
if `R` is a principal ideal domain.

This is a `lemma` to make the induction a bit easier. To actually access the basis,
see `Submodule.basisOfPid`.

See also the stronger version `Submodule.smithNormalForm`.
 -/
Submodule.nonempty_basis_of_pid : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrincipalIdealRing R] [IsDomain R] {ι : Type u_4} [Finite ι] (b : Module.Basis ι R M) (N : Submodule R M),
  ∃ n, Nonempty (Module.Basis (Fin n) R ↥N)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- Transporting a monoidal structure along a natural isomorphism of functors makes the isomorphism
a monoidal natural transformation.
 -/
CategoryTheory.Functor.Monoidal.natTransIsMonoidal_of_transport : ∀ {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 D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (e : F ≅ G), CategoryTheory.NatTrans.IsMonoidal e.hom
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_mul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x y : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x ≠ 0 →
    NumberField.mixedEmbedding.norm y ≠ 0 →
      NumberField.mixedEmbedding.logMap (x * y) =
        NumberField.mixedEmbedding.logMap x + NumberField.mixedEmbedding.logMap y
-- Batteries.Lean.System.IO
_private.Batteries.Lean.System.IO.0.tacticNonempty_list : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_set_inclusion : ∀ {α : Type u} [inst : UniformSpace α] {s t : Set α} (hst : s ⊆ t), IsUniformEmbedding (Set.inclusion hst)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.mk.sizeOf_spec : ∀ {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]
  [inst_6 : SizeOf C] (le ge : ℤ → CategoryTheory.ObjectProperty C)
  (le_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam)
  (ge_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam)
  (le_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X))
  (ge_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X))
  (zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0) (le_zero_le : le 0 ≤ le 1) (ge_one_le : ge 1 ≤ ge 0)
  (exists_triangle_zero_one :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le 0 X) (_ : ge 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  sizeOf
      { le := le, ge := ge, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms, le_shift := le_shift, ge_shift := ge_shift,
        zero' := zero', le_zero_le := le_zero_le, ge_one_le := ge_one_le,
        exists_triangle_zero_one := exists_triangle_zero_one } =
    1
-- Mathlib.Order.Hom.Set
/-- A strictly monotone function from a linear order is an order isomorphism between its domain and
its range.  -/
StrictMono.orderIso : {α : Type u_1} →
  {β : Type u_2} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → α ≃o ↑(Set.range f)
-- Aesop.Tree.TreeM
Aesop.getRootMetaState : Aesop.TreeM Lean.Meta.SavedState
-- Mathlib.Order.Defs.LinearOrder
compare_eq_iff_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, compare a b = Ordering.eq ↔ a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.cosk.faithful : ∀ (n : ℕ), (SSet.Truncated.cosk n).Faithful
-- Batteries.Recycling.RBTree.WF
/-- The `map` function preserves the order invariants if `f` is monotone.  -/
RBTree.RBNode.Ordered.map : ∀ {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} (f : α → β)
  [RBTree.RBNode.IsMonotone cmpα cmpβ f] {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmpα t → RBTree.RBNode.Ordered cmpβ (RBTree.RBNode.map f t)
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.Monad C) (x_1 : C),
  ((CategoryTheory.Monad.monadMonEquiv C).unitIso.hom.app x).app x_1 =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Monad C)).obj x).obj x_1)
-- Mathlib.CategoryTheory.Functor.Currying
/-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism
between `curry.obj ((F₁.prod F₂).comp G)` and
`F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`.  -/
CategoryTheory.Functor.curryObjProdComp : {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] →
            {C' : Type u_1} →
              {D' : Type u_2} →
                [inst_3 : CategoryTheory.Category.{v_1, u_1} C'] →
                  [inst_4 : CategoryTheory.Category.{v_2, u_2} D'] →
                    (F₁ : CategoryTheory.Functor C D) →
                      (F₂ : CategoryTheory.Functor C' D') →
                        (G : CategoryTheory.Functor (D × D') E) →
                          CategoryTheory.Functor.curry.obj ((F₁.prod F₂).comp G) ≅
                            F₁.comp
                              ((CategoryTheory.Functor.curry.obj G).comp
                                ((CategoryTheory.Functor.whiskeringLeft C' D' E).obj F₂))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.inclusion_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : MulAction M α] (s : SubMulAction M α),
  Function.Injective ⇑s.inclusion
-- Mathlib.Order.Defs.Unbundled
IsRelUpperSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α) (P : α → Prop),
  IsRelUpperSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ico' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ioc (f b) (f a) ⊆ f '' Set.Ico a b
-- Mathlib.Topology.Separation.Regular
/-- In a (possibly non-Hausdorff) locally compact regular space, for every compact set `K`,
`𝓝ˢ K` has a basis consisting of closed compact sets.  -/
IsCompact.nhdsSet_basis_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K : Set X},
  IsCompact K → (nhdsSet K).HasBasis (fun L => L ∈ nhdsSet K ∧ IsCompact L ∧ IsClosed L) id
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.of_mul_add : ∀ {R : Type u_1} [inst : Semiring R] {a b : R}, a * b = 0 → a + b = 1 → IsIdempotentElem a ∧ IsIdempotentElem b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- The equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`  -/
AddMonoidAlgebra.toMultiplicative : (R : Type u_3) →
  (M : Type u_6) → [inst : Semiring R] → [inst_1 : Add M] → AddMonoidAlgebra R M ≃+* MonoidAlgebra R (Multiplicative M)
-- Init.Data.UInt.Bitwise
UInt32.and_le_right : ∀ {a b : UInt32}, a &&& b ≤ b
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeTR.go.eq_def : ∀ {α : Type u_1} (l a : List α) (a_1 : ℕ) (a_2 : Array α),
  List.takeTR.go✝ l a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => l
    | head :: tail, 0, acc => acc.toList
    | a :: as, n.succ, acc => List.takeTR.go✝ l as n (acc.push a)
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxHom_auxInv : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  (IsLocalization.Away.auxHom✝ S r).comp (IsLocalization.Away.auxInv✝ S r) = RingHom.id S
-- Mathlib.RingTheory.Localization.Finiteness
Submodule.localized'_fg : ∀ {R : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (R' : Type u_1) [inst_3 : CommSemiring R'] [inst_4 : Algebra R R'] {M' : Type u_2} [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : Module R' M'] [inst_8 : IsScalarTower R R' M'] (S : Submonoid R)
  [inst_9 : IsLocalization S R'] (f : M →ₗ[R] M') [inst_10 : IsLocalizedModule S f],
  N.FG → (Submodule.localized' R' S f N).FG
-- Init.Data.UInt.Lemmas
UInt8.succ_mul : ∀ {a b : UInt8}, (a + 1) * b = a * b + b
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {A B : CommHopfAlgCat R} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.approx_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : SemilatticeSup β]
  [inst_2 : OrderBot β] [inst_3 : Zero β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  [inst_6 : MeasurableSpace β] [OpensMeasurableSpace β] [inst_8 : MeasurableSpace γ] {i : ℕ → β} {f : γ → β} {g : α → γ}
  {n : ℕ} (a : α),
  Measurable f →
    Measurable g → (MeasureTheory.SimpleFunc.approx i (f ∘ g) n) a = (MeasureTheory.SimpleFunc.approx i f n) (g a)
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.exists_finset_toPOUFun_eventuallyEq : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  ∃ t, f.toPOUFun i =ᶠ[nhds x] ⇑(f i) * ⇑(∏ j ∈ t with WellOrderingRel j i, (1 - f j))
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}
  (onFunction : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam)
  (onRelation : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam),
  sizeOf { onFunction := onFunction, onRelation := onRelation } = 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_filterMap : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → Option β'} {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.IterM.filterMap f it) =
    Std.IterM.anyM
      (fun x =>
        match f x with
        | some fx => p fx
        | none => pure { down := false })
      it
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A variant of `multiplicativeClosure` in which compositions are taken on the left rather than
on the right. It is not intended to be used directly, and one should rather access this via
`multiplicativeClosure_eq_multiplicativeClosure'` in cases where the inductive principle of this
variant is needed.  -/
CategoryTheory.MorphismProperty.multiplicativeClosure' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
the edist from `x` to `y`  -/
Metric.infEDist_le_infEDist_add_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  Metric.infEDist x s ≤ Metric.infEDist y s + edist x y