mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.id_app : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (M : X.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app (CategoryTheory.CategoryStruct.id M) U =
    CategoryTheory.CategoryStruct.id (M.presheaf.obj (Opposite.op U))
-- Mathlib.Analysis.Convex.Star
StarConvex.preimage_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E} {c : 𝕜}, StarConvex 𝕜 (c • x) s → StarConvex 𝕜 x ((fun z => c • z) ⁻¹' s)
-- Mathlib.Algebra.Group.Defs
/-- **Alias** of `pow_two`.

---

Note that most of the lemmas about powers of two refer to it as `sq`.  -/
sq : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 2 = a * a
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_eq_threeMore_iff_toBitVec : ∀ {b : UInt8},
  ByteArray.utf8DecodeChar?.parseFirstByte b = ByteArray.utf8DecodeChar?.FirstByte.threeMore ↔
    BitVec.extractLsb' 3 5 b.toBitVec = 30#5
-- Mathlib.Order.WellFoundedSet
Finset.wellFoundedOn_bUnion : ∀ {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α},
  (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its
`NonUnitalRingHom.srange`.  -/
RingEquiv.sofLeftInverse' : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        {F : Type u_1} →
          [inst_2 : FunLike F R S] →
            [inst_3 : NonUnitalRingHomClass F R S] →
              {g : S → R} → {f : F} → Function.LeftInverse g ⇑f → R ≃+* ↥(NonUnitalRingHom.srange f)
-- Lean.Environment
Lean.Kernel.Exception.other.sizeOf_spec : ∀ (msg : String), sizeOf (Lean.Kernel.Exception.other msg) = 1 + sizeOf msg
-- Mathlib.Order.Compare
/-- **Alias** of the reverse direction of `Ordering.compares_swap`. -/
Ordering.Compares.swap : ∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering}, o.Compares b a → o.swap.Compares a b
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- An arbitrary choice of limit cone for a functor.  -/
CategoryTheory.Limits.limit.cone : {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.HasLimit F] → CategoryTheory.Limits.Cone F
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.OrderHom.ωSup_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α),
  (OmegaCompletePartialOrder.OrderHom.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_5 : HSub Std.Time.Duration Std.Time.Nanosecond.Offset Std.Time.Duration
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] (a : α), -{a} = {-a}
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffOn_prod_module_iff : ∀ {𝕜 : 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_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {s : Set M}
  {n : WithTop ℕ∞} (f : M → F₁ × F₂),
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s ↔
    ContMDiffOn I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) s ∧
      ContMDiffOn I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) s
-- Lean.Meta.Basic
/-- Context for the surrounding `isDefEq` call when the entry was created.  -/
Lean.Meta.PostponedEntry.ctx? : Lean.Meta.PostponedEntry → Option Lean.Meta.DefEqContext
-- Mathlib.Algebra.Homology.Monoidal
/-- Given three homological complexes `K₁`, `K₂`, and `K₃`, this asserts that for
all `j`, the functor `K₁.X i₁` commutes with the coproduct of
the `K₂.X i₂ ⊗ K₃.X i₃` such that `i₂ + i₃ = j`.  -/
HomologicalComplex.HasGoodTensor₂₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {I : Type u_2} →
          [inst_3 : AddMonoid I] →
            {c : ComplexShape I} →
              [c.TensorSigns] → HomologicalComplex C c → HomologicalComplex C c → HomologicalComplex C c → Prop
-- Mathlib.Topology.Order.MonotoneConvergence
SupConvergenceClass.mk : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  (∀ (a : α) (s : Set α), IsLUB s a → Filter.Tendsto Subtype.val Filter.atTop (nhds a)) → SupConvergenceClass α
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitoneOn_toDual_comp_iff`. -/
MonotoneOn.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f) s
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.factorsThroughLocalization : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.homRel C).FactorsThroughLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
-- Std.Async.Basic
Std.Async.instMonadAwaitStateTOfMonad_1 : {m t : Type → Type} → {s : Type} → [Monad m] → [Std.Async.MonadAwait t m] → Std.Async.MonadAwait t (StateT s m)
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieHom.toNonUnitalAlgHom_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], Function.Injective LieHom.toNonUnitalAlgHom
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_le_op_iff : ∀ {M : Type u_2} [inst : AddZeroClass M] {S₁ S₂ : AddSubmonoid M}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The groupoid of all open partial homeomorphisms on a topological space `H`
is closed under restriction.  -/
instClosedUnderRestrictionContinuousGroupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H], ClosedUnderRestriction (continuousGroupoid H)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : AddZeroClass M] [inst_1 : SizeOf M] (toAddSubmonoid : AddSubmonoid M)
  (addSaturated : toAddSubmonoid.AddSaturated),
  sizeOf { toAddSubmonoid := toAddSubmonoid, addSaturated := addSaturated } = 1 + sizeOf toAddSubmonoid
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g),
  LinearMap.snd T (TensorProduct S T P.toExtension.Cotangent)
        (Algebra.Generators.localizationAway T g).toExtension.Cotangent ∘ₗ
      ↑(Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx) =
    Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom
-- Mathlib.RingTheory.RootsOfUnity.Basic
mem_rootsOfUnity_iff_mem_nthRoots : ∀ {R : Type u_4} {k : ℕ} [NeZero k] [inst : CommRing R] [inst_1 : IsDomain R] {ζ : Rˣ},
  ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ Polynomial.nthRoots k 1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcycles_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {A : C} (f₁ f₂ : S.opcycles ⟶ A),
  CategoryTheory.CategoryStruct.comp S.pOpcycles f₁ = CategoryTheory.CategoryStruct.comp S.pOpcycles f₂ → f₁ = f₂
-- Lean.Elab.Binders
/-- The error name for "failed to infer binder type" errors.

We cannot use `logNamedError` here because the error is logged later, after attempting to synthesize
metavariables, in `logUnassignedUsingErrorInfos`.
 -/
Lean.Elab.Term.failedToInferBinderTypeErrorName : Lean.Name
-- Mathlib.Order.Filter.Extr
IsMaxOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → ∀ {g : β → γ}, Antitone g → IsMinOn (g ∘ f) s a
-- Init.Core
/-- `a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. -/
«term_∩_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Divisibility.Basic
IsRightRegular.rightDvd_cancel_right : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, IsRightRegular a → (b * a ∣ᵣ c * a ↔ b ∣ᵣ c)
-- Mathlib.CategoryTheory.Equivalence
/-- Construct an isomorphism `G ≅ F ⋙ H.inverse` from an isomorphism `G ⋙ H.functor ≅ F`.  -/
CategoryTheory.Iso.isoCompInverse : {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 E} →
              {G : CategoryTheory.Functor C D} → {H : D ≌ E} → (G.comp H.functor ≅ F) → (G ≅ F.comp H.inverse)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.inf_iff_not_sup_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n),
  T.Iff (φ ⊓ ψ) (φ.not ⊔ ψ.not).not
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ Std.ExtDTreeMap.Const.insertManyIfNewUnit t l},
      k ∉ t →
        List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
          k ∈ l → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey k' h' = k
-- Mathlib.Algebra.Module.CharacterModule
/-- Linear maps into a character module are exactly characters of the tensor product.
 -/
CharacterModule.homEquiv : {R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → (A →ₗ[R] CharacterModule B) ≃ₗ[R] CharacterModule (TensorProduct R A B)
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_single : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (i : n) (a : A i),
  CoalgebraStruct.comul (Pi.single i a) =
    (TensorProduct.map (LinearMap.single R A i) (LinearMap.single R A i)) (CoalgebraStruct.comul a)
-- Mathlib.Analysis.Complex.Isometry
rotationOf_coe : ∀ (e : ℂ ≃ₗᵢ[ℝ] ℂ), ↑(rotationOf e) = e 1 / ↑‖e 1‖
-- Mathlib.Topology.Order.LeftRight
nhdsGT_le_nhdsNE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), nhdsWithin a (Set.Ioi a) ≤ nhdsWithin a {a}ᶜ
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializeResult : Lean.FromJson Lean.Lsp.InitializeResult
-- Init.Prelude
/-- Packs an array of bytes into a `ByteArray`.

Converting between `Array` and `ByteArray` takes linear time.
 -/
ByteArray.mk : Array UInt8 → ByteArray
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.zero_le_log_iff : ∀ {x : ENNReal}, 0 ≤ x.log ↔ 1 ≤ x
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.mul_pdf_integrable : ∀ {Ω : Type u_2} {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ},
  IsCompact s →
    MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume →
      MeasureTheory.Integrable (fun x_1 => x_1 * (MeasureTheory.pdf X ℙ MeasureTheory.volume x_1).toReal)
        MeasureTheory.volume
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuouAt_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuousAt (-f) a ↔ UpperSemicontinuousAt f a
-- Init.Data.Array.Monadic
List.filterRevM_toArray : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool},
  Array.filterRevM p l.toArray = List.toArray <$> List.filterRevM p l
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `β` is a group, then any function from `α` to `β` extends uniquely to a group homomorphism
from the free group over `α` to `β`  -/
FreeGroup.lift : {α : Type u} → {β : Type v} → [inst : Group β] → (α → β) ≃ (FreeGroup α →* β)
-- Mathlib.Order.DirSupClosed
DirSupClosed.univ : ∀ {α : Type u_1} [inst : Preorder α], DirSupClosed Set.univ
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.pow_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Monoid γ] [inst_4 : ContinuousMul γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)),
  (f ^ n).comp g = f.comp g ^ n
-- Mathlib.Algebra.Category.Ring.FilteredColimits
RingCat.FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ RingCat AddCommGrpCat)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_swap_iff`. -/
Ordinal.principal_swap_iff : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  Ordinal.IsPrincipal (Function.swap op) o ↔ Ordinal.IsPrincipal op o
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mk.injEq : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] (toContinuousMap : C(X, R)) (map_zero' : toContinuousMap 0 = 0)
  (toContinuousMap_1 : C(X, R)) (map_zero'_1 : toContinuousMap_1 0 = 0),
  ({ toContinuousMap := toContinuousMap, map_zero' := map_zero' } =
      { toContinuousMap := toContinuousMap_1, map_zero' := map_zero'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.instInfSet : {M : Type u_1} → [inst : Mul M] → InfSet (Subsemigroup M)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- See `inner_smul_right` for the common special when `𝕜 = 𝕝`.  -/
inner_smul_right_eq_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {𝕝 : Type u_4} [inst_3 : CommSemiring 𝕝] [inst_4 : StarRing 𝕝] [inst_5 : Algebra 𝕝 𝕜] [inst_6 : Module 𝕝 E]
  [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] (x y : E) (r : 𝕝), inner 𝕜 x (r • y) = r • inner 𝕜 x y
-- Mathlib.Data.Sigma.Lex
Sigma.lex_swap : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i},
  Sigma.Lex (Function.swap r) s a b ↔ Sigma.Lex r (fun i => Function.swap (s i)) b a
-- Init.Data.Ord.UInt
UInt64.instLawfulEqOrd : Std.LawfulEqOrd UInt64
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.dense_covering : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X},
  S ∈ CategoryTheory.GrothendieckTopology.dense X ↔
    ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Util.Notation3
/-- Push a delaborated term onto a foldr/foldl array.  -/
Mathlib.Notation3.MatchState.pushFold : Mathlib.Notation3.MatchState → Lean.Name → Lean.Term → Mathlib.Notation3.MatchState
-- Mathlib.Algebra.Group.Basic
zsmul_add_comm : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (m n : ℤ), m • a + n • a = n • a + m • a
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- If `f : X ⟶ S` and `g : Y ⟶ S` are morphisms of schemes and `x : X` and `y : Y` are points such
that `f x = g y`, then there exists `z : X ×[S] Y` lying above `x` and `y`.

In other words, the map from the underlying topological space of `X ×[S] Y` to the fiber product
of the underlying topological spaces of `X` and `Y` over `S` is surjective.
 -/
AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y),
  f x = g y → ∃ z, (CategoryTheory.Limits.pullback.fst f g) z = x ∧ (CategoryTheory.Limits.pullback.snd f g) z = y
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- Special case of `MeromorphicOn.intervalIntegrable_log`: The function `log ∘ cos` is interval
integrable over every interval.
 -/
intervalIntegrable_log_cos : ∀ {a b : ℝ}, IntervalIntegrable (Real.log ∘ Real.cos) MeasureTheory.volume a b
-- Init.PropLemmas
Decidable.not_iff_comm : ∀ {a b : Prop} [Decidable a] [Decidable b], (¬a ↔ b) ↔ (¬b ↔ a)
-- Lean.Environment
Lean.Kernel.Exception.alreadyDeclared.inj : ∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {env_1 : Lean.Kernel.Environment} {name_1 : Lean.Name},
  Lean.Kernel.Exception.alreadyDeclared env name = Lean.Kernel.Exception.alreadyDeclared env_1 name_1 →
    env = env_1 ∧ name = name_1
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Millisecond.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Millisecond.Offset
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.mk : {α : Type} →
  (α → List Lean.HeadIndex) →
    (α → List Lean.HeadIndex → α) →
      (α → Lean.Meta.Grind.Origin) → (α → Lean.Expr) → (α → Array Lean.Name) → Lean.Meta.Grind.TheoremLike α
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.factorsThru_of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S T : CategoryTheory.Presieve X),
  S ≤ T → S.FactorsThru T
-- Mathlib.Logic.Function.FromTypes
/-- The definitional equality between `0`-ary heterogeneous functions into `τ` and `τ`.  -/
Function.fromTypes_zero_equiv : (p : Fin 0 → Type u) → (τ : Type u) → Function.FromTypes p τ ≃ τ
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_pos : ∀ {r : NNReal}, 0 < ↑r ↔ 0 < r
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry.induct_unfolding : ∀ {α : Type u} {β : Type v} (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.isEmpty = false → α × β → Prop),
  (∀ (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x (k, v)) →
    (∀ (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                r_1).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) ⋯
              (Std.DTreeMap.Internal.Impl.Const.minEntry (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              h (Std.DTreeMap.Internal.Impl.Const.minEntry (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α fun x => β) (h : t.isEmpty = false),
        motive t h (Std.DTreeMap.Internal.Impl.Const.minEntry t h)
-- Mathlib.Logic.Nontrivial.Defs
exists_pair_ne : ∀ (α : Type u_3) [Nontrivial α], ∃ x y, x ≠ y
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring homomorphism `f` from `M` to `P`, the kernel of `f` is the
unique ring congruence relation on `M` whose induced map from the quotient of
`M` to `P` is injective.  -/
RingCon.ker_eq_lift_of_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  (H : c ≤ RingCon.ker f), Function.Injective ⇑(c.lift f H) → RingCon.ker f = c
-- Std.Internal.Do.PredTrans
/-- `MonadExceptOf` instance lifted through a state layer:
delegates `throw` and `tryCatch` to the inner `PredTrans l e` instance.  -/
Std.Internal.Do.instMonadExceptOfPredTransForall : {ε : Type u} →
  {Pred : Type v} →
    {EPred : Type w} →
      {σ : Type z} →
        [MonadExceptOf ε (Std.Internal.Do.PredTrans Pred EPred)] →
          MonadExceptOf ε (Std.Internal.Do.PredTrans (σ → Pred) EPred)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasStrictFDerivAt c c' x → HasStrictFDerivAt f f' x → HasStrictFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x
-- Lean.Server.Rpc.RequestHandling
Lean.Server.RpcProcedure.wrapper : Lean.Server.RpcProcedure → UInt64 → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- `U.starProjection` is a star projection.  -/
isStarProjection_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection], IsStarProjection U.starProjection
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The range of a ring homomorphism, as a `NonUnitalSubring` of the target.
See Note [range copy pattern].  -/
NonUnitalRingHom.range : {R : Type u} →
  {S : Type v} → [inst : NonUnitalNonAssocRing R] → [inst_1 : NonUnitalNonAssocRing S] → (R →ₙ+* S) → NonUnitalSubring S
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsUnit.prod_univ_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] {f : ι → M},
  IsUnit (∏ a, f a) ↔ ∀ (a : ι), IsUnit (f a)
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_Icc_one : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.Icc 1 n)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  (Std.ExtDTreeMap.Const.toList t).isEmpty = t.isEmpty