mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.quotient.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (x y : R),
  IsDiscreteValuationRing.quotient x y = if y = 0 then 0 else if h : y ∣ x then Exists.choose h else 0
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), CategoryTheory.Sieve.functorPushforward F ⊤ = ⊤
-- Mathlib.Algebra.Group.End
AddAut.congr.eq_1 : ∀ {G : Type u_3} [inst : AddGroup G] {H : Type u_7} [inst_1 : AddGroup H] (ϕ : G ≃+ H),
  AddAut.congr ϕ =
    { toFun := fun f => ϕ.symm.trans (AddEquiv.trans f ϕ), invFun := fun f => ϕ.trans (AddEquiv.trans f ϕ.symm),
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cone on `F.rightOp : J ⥤ Cᵒᵖ` to a cocone on `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coconeOfConeRightOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → CategoryTheory.Limits.Cone F.rightOp → CategoryTheory.Limits.Cocone F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquiv_symm_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  W'.nonsingularPointEquiv.symm (some ⟨(x, y), h⟩) = WeierstrassCurve.Affine.Point.some x y h
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` creates
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsLimitOfLeftOp : {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.CreatesColimit K.op F.leftOp] → CategoryTheory.CreatesLimit K F
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Given `x = f * g` with `g` homogeneous of positive degree,
this is the map `A_{(f)} → A_{(x)}` taking `a/f^i` to `ag^i/(fg)^i`.  -/
HomogeneousLocalization.awayMap : {ι : 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 ι] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] →
                    {e : ι} →
                      {f g : A} →
                        g ∈ 𝒜 e →
                          {x : A} → x = f * g → HomogeneousLocalization.Away 𝒜 f →+* HomogeneousLocalization.Away 𝒜 x
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pullback a distributive scalar multiplication along an injective additive monoid
homomorphism.
See note [reducible non-instances].  -/
Function.Injective.distribSMul : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : AddZeroClass A] →
        [inst_1 : DistribSMul M A] →
          [inst_2 : AddZeroClass B] →
            [inst_3 : SMul M B] →
              (f : B →+ A) → Function.Injective ⇑f → (∀ (c : M) (x : B), f (c • x) = c • f x) → DistribSMul M B
-- Mathlib.Topology.Metrizable.ContinuousMap
ContinuousMap.instMetrizableSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
  [inst_3 : TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y], TopologicalSpace.MetrizableSpace C(X, Y)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.LocallyQuasiFinite f],
  AlgebraicGeometry.LocallyQuasiFinite (f ∣_ V)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Commuting a functor that preserves left Kan extensions with the `lan` functor.  -/
CategoryTheory.Functor.lanCompIsoOfPreserves : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (L : CategoryTheory.Functor A C) →
                    [G.PreservesLeftKanExtensions L] →
                      [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F] →
                        [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] →
                          L.lan.comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G) ≅
                            ((CategoryTheory.Functor.whiskeringRight A B D).obj G).comp L.lan
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.instLawfulGetElemMemOfTransCmp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp],
  LawfulGetElem (Std.TreeMap α β cmp) α β fun m a => a ∈ m
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.zero_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel α γ), ProbabilityTheory.Kernel.prod 0 η = 0
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- If `A` has no rows, then it is totally unimodular.  -/
Matrix.emptyRows_isTotallyUnimodular : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [IsEmpty m] (A : Matrix m n R), A.IsTotallyUnimodular
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.abs_arg_lt_pi_div_two_iff : ∀ {z : ℂ}, |z.arg| < Real.pi / 2 ↔ 0 < z.re ∨ z = 0
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.inv_mem_of_algebraic : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subalgebra K L)
  {x : ↥A}, IsAlgebraic K ↑x → (↑x)⁻¹ ∈ A
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_intCast : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ) (n : ℤ), x ^ (y - ↑n) = x ^ y / x ^ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.plaintext.injEq : ∀ (text text_1 : String),
  (Lean.Lsp.InlayHintTooltip.plaintext text = Lean.Lsp.InlayHintTooltip.plaintext text_1) = (text = text_1)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- The short complex of abelian sheaves
`ℤ[S.X₁] ⟶ ℤ[S.X₂] ⊞ ℤ[S.X₃] ⟶ ℤ[S.X₄]`
where the left map is a difference and the right map a sum.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        [CategoryTheory.HasSheafify J AddCommGrpCat] →
          J.MayerVietorisSquare → CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrpCat)
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.IsPushout.epi_shortComplex_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (h : CategoryTheory.IsPushout f g inl inr), CategoryTheory.Epi ⋯.shortComplex.g
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given `R`-algebras `A, B` and localization maps to their fraction rings
`f : A →ₐ[R] K, g : B →ₐ[R] L`, an isomorphism `h : A ≃ₐ[R] B` induces an isomorphism of
fraction rings `K ≃ₐ[R] L`.  -/
IsFractionRing.algEquivOfAlgEquiv : {R : Type u_8} →
  {A : Type u_9} →
    {K : Type u_10} →
      {B : Type u_11} →
        {L : Type u_12} →
          [inst : CommSemiring R] →
            [inst_1 : CommRing A] →
              [inst_2 : CommRing B] →
                [inst_3 : CommRing K] →
                  [inst_4 : CommRing L] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R K] →
                        [inst_7 : Algebra A K] →
                          [IsFractionRing A K] →
                            [IsScalarTower R A K] →
                              [inst_10 : Algebra R B] →
                                [inst_11 : Algebra R L] →
                                  [inst_12 : Algebra B L] →
                                    [IsFractionRing B L] → [IsScalarTower R B L] → (A ≃ₐ[R] B) → K ≃ₐ[R] L
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [inst_4 : CategoryTheory.Limits.HasCoproduct X]
  [inst_5 : CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Sigma.map f)
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_eq_opNorm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NontriviallyNormedField α] [NormedAlgebra ℝ α] (A : Matrix m n α),
  ‖A‖ = ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piUnique_symm_apply : ∀ {α : Type u_7} [inst : Unique α] (f : α → Type u_8) [inst_1 : (x : α) → TopologicalSpace (f x)],
  ⇑(Homeomorph.piUnique f).symm = uniqueElim
-- Std.Sync.Notify
Std.Notify.Consumer.select.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (finished : Std.Async.Waiter α),
  sizeOf (Std.Notify.Consumer.select finished) = 1 + sizeOf finished
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.Hom.left.eq_1 : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (f : X ⟶ Y),
  CategoryTheory.Arrow.Hom.left f = f.left
-- Lean.Expr
Lean.mkLitEx : Lean.Literal → Lean.Expr
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalLE_true : ∀ {a b : Ordinal.{u}} {an bn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an → Mathlib.Meta.NormNum.IsNat b bn → decide (an ≤ bn) = true → a ≤ b
-- Mathlib.Analysis.RCLike.Inner
_private.Mathlib.Analysis.RCLike.Inner.0.RCLike.wInner.eq_1 : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g : (i : ι) → E i), ⟪f, g⟫_[𝕜, w] = ∑ i, w i • inner 𝕜 (f i) (g i)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose.eq_1 : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  μ.transpose B = μ.mapRange (↑B.flip).toAddMonoidHom ⋯
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.parse.goAlts : Lean.TSyntax `Lean.Parser.Tactic.mcasesPatAlts → Option Lean.Parser.Tactic.MCasesPat
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_nsmul : ∀ (n : ℕ) (x : ℝ), ↑(n • x) = n • ↑x
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ico_eq_nhdsGE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → nhdsWithin b (Set.Ico b a) = nhdsWithin b (Set.Ici b)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The splitting of the short complex `S.unop` deduced from a splitting of `S`.  -/
CategoryTheory.ShortComplex.Splitting.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S : CategoryTheory.ShortComplex Cᵒᵖ} → S.Splitting → S.unop.Splitting
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.eVariationOn_Iic_eq_Iio_add_edist : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [DenselyOrdered α] {f : α → E} {a : α},
  BoundedVariationOn f Set.univ →
    eVariationOn f (Set.Iic a) = eVariationOn f (Set.Iio a) + edist (f a) (Function.leftLim f a)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- When `P` is a sheaf and `S` is a cover, the associated multifork is a limit.  -/
CategoryTheory.Presheaf.isLimitOfIsSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (P : CategoryTheory.Functor Cᵒᵖ A) →
            {X : C} →
              (S : J.Cover X) → CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Limits.IsLimit (S.multifork P)
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_zero_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.sphere 0 r ↔ ‖a‖ = r
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Syntax →
    Lean.Parser.ModuleParserState →
      Lean.Language.Lean.CommandElaboratingSnapshot →
        Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
          Lean.Language.Lean.CommandParsedSnapshot
-- Mathlib.Data.List.Basic
/-- Consider two lists `l₁` and `l₂` with designated elements `a₁` and `a₂` somewhere in them:
`l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`.
Assume the designated element `a₂` is present in neither `x₁` nor `z₁`.
We conclude that the lists are equal (`l₁ = l₂`) if and only if their respective parts are equal
(`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`).  -/
List.append_cons_inj_of_notMem : ∀ {α : Type u} {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α},
  a₂ ∉ x₁ → a₂ ∉ z₁ → (x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr_mk' : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G),
  (QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Analogue of `Fin.eq_zero_or_eq_succ` for `succAbove`.  -/
Fin.eq_self_or_eq_succAbove : ∀ {n : ℕ} (p i : Fin (n + 1)), i = p ∨ ∃ j, i = p.succAbove j
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (l : Γ → σ → Λ),
  Turing.TM1to1.trNormal dec (Turing.TM1.Stmt.goto l) =
    Turing.TM1to1.read dec fun a => Turing.TM1.Stmt.goto fun x s => Turing.TM1to1.Λ'.normal (l a s)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), U.ι = X.ofRestrict ⋯
-- Batteries.Recycling.RBTree.Basic
/-- The "keys" of the map. This is an `O(1)` wrapper operation, which
can be used in `for` loops or converted to an array or list.
 -/
RBTree.RBMap.values : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → RBTree.RBMap.Values α β cmp
-- Mathlib.Topology.Algebra.ConstMulAction
/-- If an additive action is central, then its right action is continuous when its
left action is.  -/
ContinuousConstVAdd.op : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α], ContinuousConstVAdd Mᵃᵒᵖ α
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The forwards edge of `coherentIso` has an inverse.  -/
SSet.coherentIso.invStructHom : SSet.coherentIso.hom.InvStruct
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.LaxFunctor.mapId' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.LaxFunctor B C) →
          {b : B} →
            (f : b ⟶ b) →
              autoParam (f = CategoryTheory.CategoryStruct.id b) CategoryTheory.LaxFunctor.mapId'._auto_1 →
                (CategoryTheory.CategoryStruct.id (F.obj b) ⟶ F.map f)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- If `𝒮 Z` is `max u v`-small for every `Z`, then the subsheaf generated by `𝒮 Z` has
`max u v`-small sections.  -/
CategoryTheory.Precoverage.small_subsheafify_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)},
  (∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) →
    ∀ (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))),
      (∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)) →
        CategoryTheory.FunctorToTypes.Small.{max u v, w, v, u} (K.subsheafify 𝒮).toFunctor
-- Mathlib.Data.Matrix.Mul
Matrix.mul_apply' : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Mul α]
  [inst_2 : AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n}, (M * N) i k = M i ⬝ᵥ fun j => N j k
-- Mathlib.Algebra.Colimit.Ring
Ring.instAddCommMonoidDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → AddCommMonoid (Ring.DirectLimit G f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.DHashMap.Internal.Raw₀ α fun x => β)
  (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (hma : m.contains a = true),
  Std.DHashMap.Internal.Raw₀.Const.get m a hma = Std.DHashMap.Internal.Raw₀.Const.get m_1 a_1 ⋯
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddMonoidCoeOfAddSubmonoidClass.eq_1 : ∀ {ι : 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 : ι) → AddMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)],
  RestrictedProduct.instAddMonoidCoeOfAddSubmonoidClass R = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within `s`, starting from the last valid
position and iterating towards the first one.

Examples

* `("abc".revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']`

* `("abc".revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]`

* `("ab∀c".revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']`

* `("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]`
 -/
String.revPositions : (s : String) → Std.Iter { p // p ≠ s.endPos }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblY P = P 1 ^ 4
-- Mathlib.Algebra.Group.Hom.Instances
/-- Composition of additive monoid morphisms (`AddMonoidHom.comp`) as an additive
monoid morphism.

Note that unlike `AddMonoidHom.comp_hom'` this requires commutativity of `N`.

This also exists in a `LinearMap` version, `LinearMap.llcomp`.  -/
AddMonoidHom.compHom : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → [inst_2 : AddCommMonoid P] → (N →+ P) →+ (M →+ N) →+ M →+ P
-- Mathlib.Logic.Function.Basic
Function.RightInverse.comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β},
  Function.RightInverse f g → Function.RightInverse h i → Function.RightInverse (h ∘ f) (g ∘ i)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.config : Lean.Meta.Grind.Params → Lean.Grind.Config
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.equivTuple_symm_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : Fin 4 → R),
  (QuaternionAlgebra.equivTuple c₁ c₂ c₃).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
-- Mathlib.RepresentationTheory.Action
Representation.linearizeTrivial_def : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] (X : Type w) (g : G),
  (Representation.linearize k G (Action.trivial G X)) g = LinearMap.id
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.NatTransExtension.app_eq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F₁ F₂ : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : C),
  CategoryTheory.Localization.Construction.NatTransExtension.app τ (W.Q.obj X) = τ.app X
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.analyticAt_relation_zero : ∀ (L : PeriodPair), AnalyticAt ℂ (PeriodPair.relation✝ L) 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.st_eq : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → x.st = r
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.const_vadd` -/
Measurable.fun_const_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {g : α → X} [MeasurableConstVAdd M X], Measurable g → ∀ (c : M), Measurable fun i => c +ᵥ g i
-- Mathlib.Data.Matrix.DMatrix
AddMonoidHom.mapDMatrix_apply : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → AddMonoid (α i j)] {β : m → n → Type w}
  [inst_1 : (i : m) → (j : n) → AddMonoid (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M : DMatrix m n α),
  (AddMonoidHom.mapDMatrix f) M = M.map fun i j => ⇑f
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.vadd_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ), c +ᵥ Metric.ball x r = Metric.ball (c +ᵥ x) r
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_lt_iff : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, ⌈a⌉ < z ↔ a ≤ ↑z - 1
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.IsGalois.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {X : C}
  [toIsConnected : CategoryTheory.PreGaloisCategory.IsConnected X],
  Nonempty
      (CategoryTheory.Limits.IsTerminal
        (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X)))) →
    CategoryTheory.PreGaloisCategory.IsGalois X
-- Mathlib.Topology.Order.Category.AlexDisc
/-- Constructs an equivalence between preorders from an order isomorphism between them.  -/
AlexDisc.Iso.mk : {α β : AlexDisc} → ↑α.toTopCat ≃ₜ ↑β.toTopCat → (α ≅ β)
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `sup_eq_left`. -/
sup_of_le_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b ≤ a → a ⊔ b = a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.ofList l cmp) k = none
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_minValue : Int16.minValue.toNatClampNeg = 0