mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Unitization
/-- See note [partially-applied ext lemmas]  -/
Unitization.starAlgHom_ext : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  {φ ψ : Unitization R A →⋆ₐ[R] C},
  (↑φ).comp (Unitization.inrNonUnitalStarAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalStarAlgHom R A) → φ = ψ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {a : α}, m.get? a = m[a]?
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℕ → Bool
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The homogeneous differential as a linear map, denoted as `𝒅` within the `Manifold` namespace.  -/
fdifferential : {𝕜 : 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] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                {I' : ModelWithCorners 𝕜 E' H'} →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (f : ContMDiffMap I I' M M' ↑⊤) →
                                          (x : M) → PointDerivation I x →ₗ[𝕜] PointDerivation I' (f x)
-- Mathlib.Analysis.Complex.Exponential
Real.one_sub_div_pow_le_exp_neg : ∀ {n : ℕ} {t : ℝ}, t ≤ ↑n → (1 - t / ↑n) ^ n ≤ Real.exp (-t)
-- Init.Data.List.Lex
_private.Init.Data.List.Lex.0.List.lex.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (l₁ l₂ : List α) →
      ((head : α) → (tail : List α) → motive [] (head :: tail)) →
        ((x : List α) → motive x []) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) → motive l₁ l₂
-- Mathlib.Order.InitialSeg
PrincipalSeg.top_rel_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [IsWellOrder γ t] (f : PrincipalSeg r s) (g : PrincipalSeg s t) (h : PrincipalSeg r t), t h.top g.top
-- Mathlib.Order.Basic
le_update_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i}
  {i : ι} {a : π i}, x ≤ Function.update y i a ↔ x i ≤ a ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
-- Mathlib.RingTheory.KrullDimension.Basic
instKrullDimLEOfNatNat : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R], Ring.KrullDimLE 1 R
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.of_isInitial : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsInitial X),
  CategoryTheory.IsCofiltered C
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.diagramIsoParallelPair_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.diagramIsoParallelPair F).inv.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Module.PUnit
PUnit.mulDistribMulAction : {R : Type u_1} → [inst : Monoid R] → MulDistribMulAction R PUnit.{u_3 + 1}
-- Mathlib.Data.Set.Image
Set.mem_range_of_mem_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) {x : β}, x ∈ f '' s → x ∈ Set.range f
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.numParams : Lean.Elab.Command.FinalizeInductiveDecl✝ → ℤ
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.lifting₂CurriedTensorPre_iso : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_4 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Localization.Lifting₂.iso L L W W (CategoryTheory.MonoidalCategory.curriedTensorPre G)
      (CategoryTheory.MonoidalCategory.curriedTensorPre F) =
    CategoryTheory.MonoidalCategory.curriedTensorPreFunctor.mapIso (CategoryTheory.Localization.Lifting.iso L W G F)
-- Init.Omega.IntList
Lean.Omega.IntList.sum_cons : ∀ {x : ℤ} {xs : List ℤ}, Lean.Omega.IntList.sum (x :: xs) = x + Lean.Omega.IntList.sum xs
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_mul_single`. -/
MonoidAlgebra.support_mul_single : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : IsRightCancelMul G] (f : MonoidAlgebra k G)
  (r : k),
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ (x : G), (f * MonoidAlgebra.single x r).coeff.support = Finset.map (mulRightEmbedding x) f.coeff.support
-- Mathlib.Data.Finset.PImage
Finset.pimage.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f f_1 : α →. β),
  f = f_1 →
    ∀ {inst_1 : (x : α) → Decidable (f x).Dom} [inst_2 : (x : α) → Decidable (f_1 x).Dom] (s s_1 : Finset α),
      s = s_1 → Finset.pimage f s = Finset.pimage f_1 s_1
-- Std.Time.Format.Modifier
Std.Time.Modifier.F.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.F presentation = Std.Time.Modifier.F presentation_1 → presentation = presentation_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk''_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X)
  (zero_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddGrp.homMk''._auto_1)
  (add_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
          CategoryTheory.AddMonObj.add)
      CategoryTheory.AddGrp.homMk''._auto_3),
  (CategoryTheory.AddGrp.homMk'' f zero_f add_f).hom.hom = f
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instEpiFOfHasFiniteColimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C]
  {K L : HomologicalComplex C c} (φ : K ⟶ L) [CategoryTheory.Epi φ] (n : ι), CategoryTheory.Epi (φ.f n)
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_insert : ∀ {α : Type u} [uniformSpace : UniformSpace α] (a : α) {s : Set α}, TotallyBounded (insert a s) ↔ TotallyBounded s
-- Init.Data.PLift
instSubsingletonPLift : ∀ {α : Sort u_1} [Subsingleton α], Subsingleton (PLift α)
-- Mathlib.Algebra.LinearRecurrence
/-- A basis of the solution space given by solutions whose initial conditions are the standard basis
vectors  -/
LinearRecurrence.basis : {R : Type u_1} → [inst : CommSemiring R] → (E : LinearRecurrence R) → Module.Basis (Fin E.order) R ↥E.solSpace
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_map_eval : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι),
  MeasureTheory.Measure.map (fun x => x i) (MeasureTheory.Measure.infinitePi μ) = μ i
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The "right" map `W ⟶ X`.  -/
CategoryTheory.IsRegularEpi.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.IsRegularEpi f] → CategoryTheory.IsRegularEpi.W f ⟶ X
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiberι_asFiber : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  (AlgebraicGeometry.Scheme.Hom.fiberι f (f x)) (AlgebraicGeometry.Scheme.Hom.asFiber f x) = x
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.size.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)) → motive x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instFunLike : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → FunLike (CentroidHom α) α α
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, s.Nonempty → t.Nonempty → (s • t).Nonempty
-- Lean.Util.Recognizers
Lean.Expr.arrayLit? : Lean.Expr → Option (Lean.Expr × List Lean.Expr)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instInhabitedFanin.default : Std.Sat.AIG.Fanin
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.le_def : ∀ {X : TopCat} {x : ↑X} (U V : TopologicalSpace.OpenNhds x), U ≤ V ↔ ↑U ≤ ↑V
-- Batteries.Data.List.Basic
/-- Computes the partial sums of the elements of a list.

Examples:

`[a, b, c].partialSums = [0, 0 + a, (0 + a) + b, ((0 + a) + b) + c]`
`[1, 2, 3].partialSums = [0, 1, 3, 6]`
 -/
List.partialSums : {α : Type u_1} → [Add α] → [Zero α] → List α → List α
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.Visitor : Type
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- We denote the normalized derivative by `D`.  -/
Derivative.termD : Lean.ParserDescr
-- Mathlib.ModelTheory.Substructures
/-- Closure of a substructure `S` equals `S`.  -/
FirstOrder.Language.Substructure.closure_eq : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M),
  (FirstOrder.Language.Substructure.closure L).toFun ↑S = S
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.unionₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.unionₘ m₂ =
    if (↑m₁).size ≤ (↑m₂).size then m₂.insertListIfNewₘ (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
    else m₁.insertListₘ (Std.DHashMap.Internal.toListModel (↑m₂).buckets)
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action on a nontrivial type is preprimitive iff
the set of blocks containing a given element is a simple order  -/
MulAction.isSimpleOrder_blockMem_iff_isPreprimitive : ∀ (G : Type u_3) [inst : Group G] {X : Type u_4} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] [Nontrivial X]
  (a : X), IsSimpleOrder (MulAction.BlockMem G a) ↔ MulAction.IsPreprimitive G X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A shorthand for `toBinaryBiconeFunctor.obj`  -/
CategoryTheory.Limits.Bicone.toBinaryBicone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y) → CategoryTheory.Limits.BinaryBicone X Y
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `colimitCocone F` becomes colimit after the application of `π₂ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isColimitπ₂MapCoconeColimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.ShortComplex.π₂.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The functor sending an object in `Action (TopModuleCat k) G` to the corresponding topological
representation.  -/
TopRep.fromActionTopModFunc : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] → [inst_2 : Monoid G] → CategoryTheory.Functor (Action (TopModuleCat k) G) (TopRep k G)
-- Mathlib.Order.LiminfLimsup
/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below.  -/
Filter.HasBasis.liminf_eq_ciSup_ciInf : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
  v.HasBasis p s →
    ∀ {f : ι → α},
      (∀ (j : Subtype p), (s ↑j).Nonempty) →
        (∃ j, BddBelow (Set.range fun i => f ↑i)) → Filter.liminf f v = ⨆ j, ⨅ i, f ↑i
-- Mathlib.Topology.Homotopy.Path
/-- A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quotient.mk`. This is the two-variable version of `ind`.
 -/
Path.Homotopic.Quotient.ind₂ : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_1} [inst_1 : TopologicalSpace Y] {x₀ y₀ : X} {x₁ y₁ : Y}
  {motive : Path.Homotopic.Quotient x₀ y₀ → Path.Homotopic.Quotient x₁ y₁ → Prop},
  (∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (Path.Homotopic.Quotient.mk a) (Path.Homotopic.Quotient.mk b)) →
    ∀ (q₀ : Path.Homotopic.Quotient x₀ y₀) (q₁ : Path.Homotopic.Quotient x₁ y₁), motive q₀ q₁
-- Mathlib.Analysis.Normed.Module.Basic
Filter.Tendsto.zero_smul_isBoundedUnder_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {α : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α},
  Filter.Tendsto f l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) → Filter.Tendsto (fun x => f x • g x) l (nhds 0)
-- Init.Internal.Order.Basic
Lean.Order.CompleteLattice.sup : {α : Sort u} → [Lean.Order.CompleteLattice α] → (α → Prop) → α
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The identity equivalence between `List α` and `FreeMonoid α`.  -/
FreeMonoid.ofList : {α : Type u_1} → List α ≃ FreeMonoid α
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_lt_one_iff_of_le_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelMonoid M] {f : ι → M}, f ≤ 1 → (∏ i, f i < 1 ↔ f < 1)
-- Mathlib.GroupTheory.Solvable
Group.IsSolvable.commutator_lt_top_of_nontrivial : ∀ (G : Type u_1) [inst : Group G] [hG : Group.IsSolvable G] [Nontrivial G], commutator G < ⊤
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.strictMono_iff_Icc : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), StrictMono ⇑f ↔ StrictMonoOn (⇑f) (Set.Icc l (l + a))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] [Inhabited α]
  {k : α} {f : β k → β k} {h : k ∈ m.modify k f}, (m.modify k f).getKey k h = k
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.ExtDTreeMap.Const.ofArray : {α : Type u} →
  {β : Type v} →
    Array (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.Const.ofArray._auto_1) → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.Probability.Moments.ComplexMGF
/-- For `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`, the derivative of the function
`z' ↦ μ[X ^ n * cexp (z' * X)]` at `z` is `μ[X ^ (n + 1) * cexp (z * X)]`.  -/
ProbabilityTheory.hasDerivAt_integral_pow_mul_exp : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ),
      HasDerivAt (fun z => ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) x ∂μ)
        (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * Complex.exp (z * ↑(X ω))) x ∂μ) z
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The functor projecting out the domain of arrows from the Grothendieck construction on
costructured arrows.  -/
CategoryTheory.CostructuredArrow.grothendieckProj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) C
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_inv_toFunctor_obj_map_app : ∀ {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] (F : CategoryTheory.Functor (C × D) E) {X Y : C}
  (f : X ⟶ Y) (Y_1 : D),
  ((CategoryTheory.curryingIso.inv.toFunctor.obj F).map f).app Y_1 =
    F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y_1))
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_aleph0 : Cardinal.aleph0.ord = Ordinal.omega0
-- Lean.Meta.Basic
Lean.Meta.modifyDefEqTransientCache : (Lean.Meta.DefEqCache → Lean.Meta.DefEqCache) → Lean.MetaM Unit
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_comp_three : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜},
  ContDiffWithinAt 𝕜 3 g t (f x) →
    ContDiffWithinAt 𝕜 3 f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              iteratedDerivWithin 3 (g ∘ f) s x =
                iteratedDerivWithin 3 g t (f x) * derivWithin f s x ^ 3 +
                    3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x +
                  derivWithin g t (f x) * iteratedDerivWithin 3 f s x
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxAttr.quot : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.eq_of_eqOn_top : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : Monoid M] {f g : G →* M}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {newWidth w : ℕ} {vec : aig.RefVec w}
  {w_1 : ℕ} {vec_1 : aig.RefVec w_1}, { w := w, vec := vec } = { w := w_1, vec := vec_1 } → w = w_1 ∧ vec ≍ vec_1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C_mul_X : ∀ {R : Type u} [inst : Semiring R] {c : R}, c ≠ 0 → (Polynomial.C c * Polynomial.X).support = {1}
-- Mathlib.Order.Lex
toLex_inj : ∀ {α : Type u_1} {a b : α}, toLex a = toLex b ↔ a = b
-- Lean.Environment
/-- The "signature" including level params and type, potentially filled asynchronously.  -/
Lean.AsyncConstantInfo.sig : Lean.AsyncConstantInfo → Task Lean.ConstantVal
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_left_pointReflection : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (p q : P), dist p ((Equiv.pointReflection p) q) = dist p q
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function is strongly measurable with respect to the σ-algebra generated by the
first coordinates, then it only depends on those first coordinates.  -/
MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset : ∀ {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z}
  {s : Finset ι} [inst_1 : TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] [T1Space Z],
  MeasureTheory.StronglyMeasurable f → DependsOn f ↑s
-- Mathlib.Data.Set.Lattice.Image
Set.image_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {s : ι → Set α}, f '' ⋃ i, s i = ⋃ i, f '' s i
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.tryTactic? : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (Option α)
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.toZeroLEOneClass : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsOrderedRing R], ZeroLEOneClass R
-- Init.Data.Array.Erase
Array.erase_eq_iff : ∀ {α : Type u_1} [inst : BEq α] {ys : Array α} [LawfulBEq α] {a : α} {xs : Array α},
  xs.erase a = ys ↔ a ∉ xs ∧ xs = ys ∨ ∃ as bs, a ∉ as ∧ xs = as.push a ++ bs ∧ ys = as ++ bs
-- Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
/-- `QCat` is the category of quasi-categories defined as the full subcategory of the category
`SSet` of simplicial sets.  -/
SSet.QCat : Type (u_1 + 1)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.minDegree_eq : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [Nonempty V] [inst_2 : DecidableRel G.Adj] {d : ℕ},
  G.IsRegularOfDegree d → G.minDegree = d
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefixWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.copy.skipPrefixWhile pat = (s.skipPrefixWhile pat).copy
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_natGeneratingSequence : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  MeasurableSet (MeasurableSpace.natGeneratingSequence α n)
-- Mathlib.Algebra.Module.Torsion.Free
smul_eq_zero_iff_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → (r • m = 0 ↔ m = 0)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.proj_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : B × F}, x ∈ e.target → proj (↑e.symm x) = x.1
-- Mathlib.NumberTheory.Real.Irrational
/-- If `x^n = m` is an integer and `n` does not divide the `multiplicity p m`, then `x`
is irrational.  -/
irrational_nrt_of_n_not_dvd_multiplicity : ∀ {x : ℝ} (n : ℕ) {m : ℤ},
  m ≠ 0 → ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], x ^ n = ↑m → multiplicity (↑p) m % n ≠ 0 → Irrational x
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_prod : ∀ {ι : Type u_1} (s : Finset ι) {x : ι → ℝ}, (∀ i ∈ s, 0 ≤ x i) → √(∏ i ∈ s, x i) = ∏ i ∈ s, √(x i)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.rnDeriv_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α)
  [s.HaveLebesgueDecomposition μ] (r : ℝ), (r • s).rnDeriv μ =ᵐ[μ] r • s.rnDeriv μ