mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listL.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.Path.root.listL = []
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` reflects
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsColimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimit K.op F],
  CategoryTheory.Limits.ReflectsColimit K F.unop
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- This homology map data expresses compatibilities of the homology data
constructed by `HomologyData.ofEpiOfIsIsoOfMono'`  -/
CategoryTheory.ShortComplex.HomologyMapData.ofEpiOfIsIsoOfMono' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₂.HomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.HomologyMapData φ
                    (CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono' φ h) h
-- Mathlib.RingTheory.HahnSeries.Summable
/-- A summable family of powers of a Hahn series `x`. If `x` has non-positive `orderTop`, then
return a junk value given by pretending `x = 0`.  -/
HahnSeries.SummableFamily.powers : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : LinearOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : CommRing R] → HahnSeries Γ R → HahnSeries.SummableFamily Γ R ℕ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a
limit. This essentially lets us commute `PullbackCone.mk` with `Functor.mapCone`.  -/
CategoryTheory.Limits.isLimitMapConePullbackConeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {W X Y Z : C} →
            {f : X ⟶ Z} →
              {g : Y ⟶ Z} →
                {h : W ⟶ X} →
                  {k : W ⟶ Y} →
                    (comm : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) →
                      CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.PullbackCone.mk h k comm)) ≃
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map h) (G.map k) ⋯)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.FormallySmooth = Algebra.FormallySmooth R S
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquivSubtype_symm_none : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {p : W'.Point → Prop} (p0 : p WeierstrassCurve.Affine.Point.zero),
  (WeierstrassCurve.Affine.pointEquivSubtype p0).symm none = ⟨WeierstrassCurve.Affine.Point.zero, p0⟩
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.nil.sizeOf_spec : ∀ {V : Type u} [inst : Quiver V] {a : V} [inst_1 : SizeOf V], sizeOf Quiver.Path.nil = 1
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- given two distinguished triangle, a commutative square
can be extended as morphism of triangles  -/
CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} [self : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
        CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
          ∃ c,
            CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
                CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Mathlib.Data.TypeVec
TypeVec.last_append1 : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1}, (α ::: β).last = β
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ (t : ℝ) (p : NNReal), MeasureTheory.MemLp (fun ω => Real.exp (t * X ω)) (↑p) μ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₁ =
    CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.left φ)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilterDistortion I c` if there exists
a function `r : ℝⁿ → (0, ∞)` (or a constant `r` if `l.bRiemann = true`) such that `s` contains each
prepartition `π` such that `l.MemBaseSet I c r π`.  -/
BoxIntegral.IntegrationParams.toFilterDistortion : {ι : Type u_1} →
  [Fintype ι] →
    BoxIntegral.IntegrationParams → (I : BoxIntegral.Box ι) → NNReal → Filter (BoxIntegral.TaggedPrepartition I)
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
/-- A simplicial set `X` has dimension `< d` iff for any `n : ℕ`
such that `d ≤ n`, all `n`-simplices are degenerate.  -/
SSet.HasDimensionLT : SSet → ℕ → Prop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, a ∉ t → t.getKey! a = default
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxoIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxo.IsAlwaysFinite (BitVec n)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mk.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (toPrepartition toPrepartition_1 : BoxIntegral.Prepartition I),
  toPrepartition = toPrepartition_1 →
    ∀ (tag tag_1 : BoxIntegral.Box ι → ι → ℝ) (e_tag : tag = tag_1)
      (tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), tag J ∈ BoxIntegral.Box.Icc I),
      { toPrepartition := toPrepartition, tag := tag, tag_mem_Icc := tag_mem_Icc } =
        { toPrepartition := toPrepartition_1, tag := tag_1, tag_mem_Icc := ⋯ }
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_comp_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
  (f : X ⟶ CategoryTheory.Subobject.underlying.obj P) (h : P.Factors (CategoryTheory.CategoryStruct.comp f P.arrow)),
  P.factorThru (CategoryTheory.CategoryStruct.comp f P.arrow) h = f
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_sub_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R (n - 2) = Polynomial.X * Polynomial.Chebyshev.C R (n - 1) - Polynomial.Chebyshev.C R n
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.precoverage_le_comap_uliftFunctor : TopCat.precoverage ≤ CategoryTheory.Precoverage.comap TopCat.uliftFunctor TopCat.precoverage
-- Init.Data.List.OfFn
List.ofFn_succ_last : ∀ {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α}, List.ofFn f = (List.ofFn fun i => f i.castSucc) ++ [f (Fin.last n)]
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Isomorphic objects have equivalent `MonoOver` categories.
 -/
CategoryTheory.MonoOver.mapIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : C} → (A ≅ B) → (CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol is a homomorphism of monoids with zero.  -/
legendreSym.hom : (p : ℕ) → [Fact (Nat.Prime p)] → ℤ →*₀ ℤ
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
/-- The evaluation functor `X.Subcomplex ⥤ Set (X.obj j)` when `X : SSet`
and `j : SimplexCategoryᵒᵖ`.  -/
SSet.Subcomplex.evaluation : (X : SSet) → (j : SimplexCategoryᵒᵖ) → CategoryTheory.Functor X.Subcomplex (Set (X.obj j))
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite' : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Nonempty M'] [Infinite R],
  Cardinal.mk (MonoidAlgebra R M') = max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.id_apply : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : A),
  (GradedRingHom.id 𝒜) x = x
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instSub : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → Sub (HomogeneousLocalization 𝒜 x)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              Set.MapsTo f s t →
                ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) s x₀
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.preimage_op_unionProd : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (S.unionProd T).op.preimage (CategoryTheory.Functor.LaxMonoidal.μ SSet.opFunctor X Y) = S.op.unionProd T.op
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_of_isEmpty : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [IsEmpty ι] (μ : ι → MeasureTheory.Measure α),
  MeasureTheory.Measure.sum μ = 0
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.proj_incl : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) (x : M), E.proj (E.incl x) = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapId : ∀ {B₀ : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} B₀] [inst_1 : CategoryTheory.Bicategory C]
  (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B₀} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5)
  (x : CategoryTheory.LocallyDiscrete B₀),
  (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapId
      x =
    mapId x.as
-- Init.Data.Vector.Attach
Vector.unattach_reverse : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n}, xs.reverse.unattach = xs.unattach.reverse
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a Heyting homomorphism preserves the bottom element.  -/
HeytingHomClass.map_bot : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : HeytingAlgebra α} {inst_1 : HeytingAlgebra β}
  {inst_2 : FunLike F α β} [self : HeytingHomClass F α β] (f : F), f ⊥ = ⊥
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `α ≃*o β` is the type of isomorphisms `α ≃ β` that preserve the ordered monoid structure.

`OrderMonoidIso` is also used for ordered group isomorphisms.

When possible, instead of parametrizing results over `(f : α ≃*o β)`,
you should parametrize over
`(F : Type*) [FunLike F M N] [MulEquivClass F M N] [OrderIsoClass F M N] (f : F)`.  -/
OrderMonoidIso : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → [Mul α] → [Mul β] → Type (max u_6 u_7)
-- Mathlib.Computability.DFA
DFA.mem_accepts : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {x : List α}, x ∈ M.accepts ↔ M.eval x ∈ M.accept
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.sum`

---

Sums of circle integrable functions are circle integrable.  -/
CircleIntegrable.fun_sum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} (s : Finset ι) {f : ι → ℂ → E},
  (∀ i ∈ s, CircleIntegrable (f i) c R) → CircleIntegrable (fun a => ∑ c ∈ s, f c a) c R
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.instIsContMDiffRiemannianBundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : ∀ (b : B), IsTopologicalAddGroup (E b)]
  [inst_12 : ∀ (b : B), ContinuousConstSMul ℝ (E b)] [inst_13 : FiberBundle F E] [inst_14 : VectorBundle ℝ F E]
  (g : Bundle.ContMDiffRiemannianMetric IB n F E), IsContMDiffRiemannianBundle IB n F E
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_compl_singleton_zero : ∀ {M : Type u_1} [inst : AddGroup M], SimpleGraph.addCayley {0}ᶜ = ⊤
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.range'.eq_1 : ∀ (start size step : ℕ), Array.range' start size step = Array.ofFn fun i => start + step * ↑i
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Smooth.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Smooth) →
    AlgebraicGeometry.Smooth f
-- Mathlib.Topology.Continuous
continuousAt_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y},
  ContinuousAt (fun x => y) x
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.mk : ∀ {G : Type u_1} [inst : Group G], (∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P) → IsZGroup G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toArray_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp] {k : α} {v : β},
  (Std.DTreeMap.Const.toArray (t.insert k v)).Perm
    ((Array.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Const.toArray t)).push (k, v))
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.instStarRing : {R : Type u_2} → {a b : R} → [inst : CommRing R] → StarRing (QuadraticAlgebra R a b)
-- Mathlib.LinearAlgebra.Contraction
homTensorHomEquiv_toLinearMap : ∀ (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  [inst_9 : Module.Projective R M] [inst_10 : Module.Finite R M] [inst_11 : Module.Projective R N]
  [inst_12 : Module.Finite R N], ↑(homTensorHomEquiv R M N P Q) = TensorProduct.homTensorHomMap (RingHom.id R) M N P Q
-- Mathlib.Algebra.Algebra.Subalgebra.Matrix
Subalgebra.coe_matrix : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {n : Type u_3}
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (S : Subalgebra R A), ↑S.matrix = S.toAddSubmonoid.matrix.carrier
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.taylorLinearEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (r : R),
  (Polynomial.taylorLinearEquiv r n).symm = Polynomial.taylorLinearEquiv (-r) n
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_lt_mul_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a b : R) {c : R}, c < 0 → (a < b * c⁻¹ ↔ b < a * c)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instIsScalarTower : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {G : Type u_3} [inst_5 : SMul G β]
  [inst_6 : IsScalarTower G β β], IsScalarTower G (CauSeq β abv) (CauSeq β abv)
-- Std.Internal.Do.WP.Basic
/-- `Except ε` is a WPMonad with `Prop` assertions and a single exception postcondition.  -/
Std.Internal.Do.Except.instWPMonad : {ε : Type u_1} → Std.Internal.Do.WPMonad (Except ε) Prop EPost⟨ε → Prop⟩
-- Init.Data.Array.Subarray
/-- The underlying array.  -/
Subarray.array : {α : Type u_1} → Subarray α → Array α
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_image_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Monotone f →
    (Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f ↔ ∀ (x : α), f '' Set.Ici x = Set.Ici (f x))
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub.eq_def : ∀ (x x_1 : ONote),
  x.sub x_1 =
    match x, x_1 with
    | ONote.zero, x => 0
    | o, ONote.zero => o
    | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ =>
      match e₁.cmp e₂ with
      | Ordering.lt => 0
      | Ordering.gt => o₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_le_omega_ofNat : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.lift.{v, u} o ≤ Ordinal.omega (OfNat.ofNat n) ↔ o ≤ Ordinal.omega (OfNat.ofNat n)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
/-- If a localizer morphism `Φ` is a localized equivalence, then it is a left
derivability structure if the categories of left resolutions are connected and the
categories of left resolutions of arrows are nonempty.  -/
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.LeftResolution X₂)] [Φ.arrow.HasLeftResolutions] [W₂.ContainsIdentities]
  [Φ.IsLocalizedEquivalence], Φ.IsLeftDerivabilityStructure
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_pi_div_two_sub_arccos : ∀ (x : ℝ), Real.arcsin x = Real.pi / 2 - Real.arccos x
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
See `Int.ediv_emod_unique` for a similar propositional statement.  -/
Int.divModEquiv : (n : ℕ) → [NeZero n] → ℤ ≃ ℤ × Fin n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.mem_cocycles₂_def : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : G × G → ↑A),
  f ∈ groupCohomology.cocycles₂ A ↔ ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0
-- Mathlib.Analysis.Calculus.FDeriv.Norm
differentiableAt_norm_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E} {t : ℝ},
  t ≠ 0 → (DifferentiableAt ℝ (fun x => ‖x‖) x ↔ DifferentiableAt ℝ (fun x => ‖x‖) (t • x))
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.norm_def' : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  ‖a‖ = ‖DoubleCentralizer.toProdMulOppositeHom a‖
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_endPos : ∀ {s : String} {pos : s.Pos}, String.Pos.ofSliceFrom (s.sliceFrom pos).endPos = s.endPos