mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_comp_inf_hom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β),
  { toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
-- Lean.Parser.Basic
Lean.Parser.checkNoWsBeforeFn : String → Lean.Parser.ParserFn
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.lift_card_iSup_le_sum_card : ∀ {ι : Type u} (f : ι → Ordinal.{v}), Cardinal.lift.{u, v} (⨆ i, f i).card ≤ Cardinal.sum fun i => (f i).card
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.refl : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Iff φ φ
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.invOfUnit_eq' : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k) (u : kˣ), PowerSeries.constantCoeff φ = ↑u → φ.invOfUnit u = φ⁻¹
-- Mathlib.Order.InitialSeg
PrincipalSeg.range_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s),
  Set.range ⇑f.toRelEmbedding = {b | s b f.top}
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coeFnMonoidHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Monoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G] (a : ContMDiffMap I I' N G n) (a_1 : N), ContMDiffMap.coeFnMonoidHom a a_1 = a a_1
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.mem_vars_rename : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) {j : τ},
  j ∈ ((MvPolynomial.rename f) φ).vars → ∃ i ∈ φ.vars, f i = j
-- Init.Control.Option
OptionT.instMonadFunctor : {m : Type u → Type v} → MonadFunctor m (OptionT m)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_union_mem_openSegment : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {f : α → E} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      μ s ≠ 0 →
        μ t ≠ 0 →
          μ s ≠ ⊤ →
            μ t ≠ ⊤ →
              MeasureTheory.IntegrableOn f s μ →
                MeasureTheory.IntegrableOn f t μ →
                  ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- The module structure provided by `Semiring.toModule` is free.  -/
Module.Free.self : ∀ (R : Type u) [inst : Semiring R], Module.Free R R
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.op (Opposite.op d) =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.addSubgroupOfEquivOfLe.congr_simp : ∀ {G : Type u_7} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K),
  AddSubgroup.addSubgroupOfEquivOfLe h = AddSubgroup.addSubgroupOfEquivOfLe h
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₁],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y)
  (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
  (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂) {Z : ↑(F.obj { as := Opposite.op Y' })}
  (h : (F.map g.op.toLoc).toFunctor.obj ((F.map f₂.op.toLoc).toFunctor.obj M₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map g.op.toLoc).toFunctor.map φ) h =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).inv.toNatTrans.app M₁)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂)
        (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).hom.toNatTrans.app M₂)
          h))
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_singleton : ∀ {α : Type u_2} {β : Type u_3} (a : α) (s : α → Set β), ⋂ x ∈ {a}, s x = s a
-- Mathlib.Algebra.Notation.Prod
Prod.snd_neg : ∀ {G : Type u_8} {H : Type u_9} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).2 = -p.2
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (x : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D}
  [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [J.HasPullbacks],
  (CategoryTheory.Precoverage.comap F J).HasPullbacks
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fx : γ) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match some fx with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_2 fx
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
_private.Mathlib.Analysis.InnerProductSpace.Rayleigh.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- We say that `y` is a conjugate root of `x` over `K` if the minimal polynomial of `x` is the
same as the minimal polynomial of `y`.
 -/
IsConjRoot : (R : Type u_1) → {A : Type u_5} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → A → Prop
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)
-- Aesop.Script.SpecificTactics
Aesop.applyS : Lean.MVarId → Lean.Expr → Option Lean.Term → Lean.Meta.TransparencyMode → Aesop.ScriptM (Array Lean.MVarId)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.id_onBoundedFormula : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, (FirstOrder.Language.LHom.id L).onBoundedFormula = id
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
/-- **First mean value theorem for interval integrals (arbitrary measure, nonnegativity).**
Let `f g : ℝ → ℝ` and let `μ` be a measure on `ℝ`. Assume that `f` is continuous on `uIcc a b`,
that `g` is interval integrable on `a..b` w.r.t. `μ`, and that `g ≥ 0` on `Ι a b`. Then
`∃ c ∈ uIcc a b, (∫ x in a..b, f x * g x ∂μ) = f c * (∫ x in a..b, g x ∂μ)`.  -/
exists_eq_const_mul_intervalIntegral_of_nonneg : ∀ {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  ContinuousOn f (Set.uIcc a b) →
    IntervalIntegrable g μ a b →
      (∀ x ∈ Set.uIoc a b, 0 ≤ g x) →
        ∃ c ∈ Set.uIcc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
-- Init.Data.Char.Lemmas
Char.isDigit_iff_toNat : ∀ {c : Char}, c.isDigit = true ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Lean.Data.Json.Basic
Lean.Json.obj.inj : ∀ {kvPairs kvPairs_1 : Std.TreeMap.Raw String Lean.Json compare},
  Lean.Json.obj kvPairs = Lean.Json.obj kvPairs_1 → kvPairs = kvPairs_1
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntryD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a),
  Std.Internal.List.getEntryD a fallback [] = fallback
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instInjectiveXIntAsHomologicalComplexUpHomotopicObjPlusObjPlusQuotientOfCochainComplexPlus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex.Plus C) (n : ℤ) [CategoryTheory.Injective (K.obj.X n)],
  CategoryTheory.Injective (((HomotopyCategory.Plus.quotient C).obj K).obj.as.X n)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.subset_isBasis'_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Indep I → I ⊆ X → ∃ J, M.IsBasis' J X ∧ I ⊆ J
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_top : ∀ {V : Type u_1} {u v : V} [inst : DecidableEq V], ⊤.edist u v = if u = v then 0 else 1
-- Mathlib.Algebra.Notation.Defs
instHVAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β], instHVAdd = { hVAdd := VAdd.vadd }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → a ∉ t
-- Lean.Message
/-- See `Lean.inlineExpr`. This variation is to be used when the expression is the trailing element of a
message; it does not append a newline or space after the expression.
 -/
Lean.inlineExprTrailing : Lean.Expr → optParam ℕ 30 → Lean.MessageData
-- Mathlib.Tactic.GrindAttrs
/-- `compactness` is a simple tactic that tries various lemmas to prove that a set is compact.
It is implemented using `grind`, and has the same configuration options as `grind`.

Use `grind only [compactness, closedness]` instead if you want to prove that the closure of sets are
compact.

It also exists as a grind attribute, and can be combined with other grind attributes using
`grind only [compactness, ...]`.
 -/
compactnessTac : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) (J : Type u_3) [inst_1 : CategoryTheory.Category.{v_3, u_3} J]
  (f : CategoryTheory.Arrow (CategoryTheory.Functor J C)) (j : J),
  ((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).obj j =
    (data.factorizationData (f.hom.app j)).Z
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.neZero_of_mem' : ∀ (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B], n ∈ S → NeZero ↑n
-- Mathlib.Order.BourbakiWitt
/-- `y` is an extreme point for `x : α` and `f : α → α` if it is in the bottom admissible set and
`y` is larger than `f z` for any `z < y` in the bottom admissible set.
This definition comes from [serge_lang_algebra]  -/
ChainCompletePartialOrder.IsExtremePt : {α : Type u_1} → [ChainCompletePartialOrder α] → α → (α → α) → α → Prop
-- Lean.Parser.Do
Lean.Parser.Term.doTry.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.Exponent
add_notMem_of_addOrderOf_eq_two : ∀ {G : Type u} [inst : AddGroup G] {x y : G}, addOrderOf x = 2 → addOrderOf y = 2 → x ≠ y → x + y ∉ {x, y, 0}
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.of_exponent_ge : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal} {f : (i : α) → E i},
  Memℓp f q → q ≤ p → Memℓp f p
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation)
  (c : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (p_1 : Lean.Grind.CommRing.Poly)
  (d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) (c_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p d c =
      Lean.Meta.Grind.Arith.CommRing.PolyDerivation.normEq0 p_1 d_1 c_1) =
    (p = p_1 ∧ d = d_1 ∧ c = c_1)
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousNegAddOpposite : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Neg α] [ContinuousNeg α], ContinuousNeg αᵃᵒᵖ
-- Mathlib.GroupTheory.OrderOfElement
nsmul_injOn_Iio_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, Set.InjOn (fun x_1 => x_1 • x) (Set.Iio (addOrderOf x))
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instZero : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → Zero (CompactlySupportedContinuousMap α β)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin_fst : ∀ {𝕜 : 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] {p : E × F}
  {s : Set (E × F)}, UniqueDiffWithinAt 𝕜 s p → fderivWithin 𝕜 Prod.fst s p = ContinuousLinearMap.fst 𝕜 E F
-- Mathlib.Probability.Distributions.Beta
/-- The pdf of the beta distribution, as a function valued in `ℝ≥0∞`.  -/
ProbabilityTheory.betaPDF : ℝ → ℝ → ℝ → ENNReal
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.one_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α],
  ↑1 = 1
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is stable under composition, cobase change and satisfies pre-cancellation,
`Under.forget P ⊤ X` creates pushouts.  -/
CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderWalkingSpanForgetOfHasPushoutsOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [CategoryTheory.Limits.HasPushouts T] →
          [P.IsStableUnderComposition] →
            [P.IsStableUnderCobaseChange] →
              [P.HasOfPrecompProperty P] →
                CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingSpan
                  (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
-- Mathlib.GroupTheory.OrderOfElement
mem_zmultiples_iff_mem_range_addOrderOf : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G} [Finite G] [inst_2 : DecidableEq G],
  y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equiv.trans : ∀ {X Y : AlgebraicGeometry.Scheme} {f g h : X.PartialMap Y}, f.equiv g → g.equiv h → f.equiv h
-- Mathlib.FieldTheory.SeparableDegree
PerfectField.splits_of_natSepDegree_eq_one : ∀ {E : Type v} [inst : Field E] {K : Type w} [inst_1 : Field K] [PerfectField K] {f : Polynomial E} (i : E →+* K),
  f.natSepDegree = 1 → (Polynomial.map i f).Splits
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- In a compactly generated space `X`, a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
CompactlyGeneratedSpace.isClosed' : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X},
  (∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
      Continuous f → IsClosed (f ⁻¹' s)) →
    IsClosed s
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- **Alias** of `Ultrafilter.sdiff_mem_iff`. -/
Ultrafilter.diff_mem_iff : ∀ {α : Type u} {s t : Set α} (f : Ultrafilter α), s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
-- Init.Data.SInt.Lemmas
Int64.toBitVec_neg : ∀ (x : Int64), (-x).toBitVec = -x.toBitVec
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_ψ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ),
  (W.baseChange B).ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).ψ n)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_injective : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Injective Module.Basis.repr
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreSetComm_oreNum : ∀ {R : Type u_2} [inst : CommMonoid R] (S : Submonoid R) (r : R) (s : ↥S), OreLocalization.oreNum r s = r
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFactor.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.convexBodySumFactor K = NumberField.mixedEmbedding.convexBodySumFactor K
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} →
      (obj : (U : C) → Submonoid ↑(M.obj U)) →
        autoParam (∀ {U V : C} (i : U ⟶ V), obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj V))
            CategoryTheory.SubmonoidFunctor.map._autoParam →
          CategoryTheory.SubmonoidFunctor M
-- Mathlib.Algebra.Group.ULift
ULift.add.eq_1 : ∀ {α : Type u} [inst : Add α], ULift.add = { add := fun f g => { down := f.down + g.down } }
-- Mathlib.GroupTheory.CoprodI
/-- A map out of the free product corresponds to a family of maps out of the summands. This is the
universal property of the free product, characterizing it as a categorical coproduct.  -/
Monoid.CoprodI.lift : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {N : Type u_3} → [inst_1 : Monoid N] → ((i : ι) → M i →* N) ≃ (Monoid.CoprodI M →* N)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_le_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Unbundled bounded linear functions are `C^n`.  -/
IsBoundedLinearMap.contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞},
  IsBoundedLinearMap 𝕜 f → ContDiff 𝕜 n f
-- Mathlib.RingTheory.Localization.FractionRing
/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is an
integral domain.  -/
IsFractionRing.isDomain : ∀ (A : Type u_4) [inst : CommRing A] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra A K] [IsFractionRing A K]
  [IsDomain A], IsDomain K
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mk.congr_simp : ∀ {X : Type u} [inst : PartialOrder X] (finset finset_1 : Finset X) (e_finset : finset = finset_1)
  (nonempty : finset.Nonempty) (comparable : ∀ (a b : ↥finset), a ≤ b ∨ b ≤ a),
  { finset := finset, nonempty := nonempty, comparable := comparable } =
    { finset := finset_1, nonempty := ⋯, comparable := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpOptions : Lean.ToJson Lean.Lsp.SignatureHelpOptions
-- Aesop.Search.SearchM
Aesop.NormSimpContext.toContext : Aesop.NormSimpContext → Lean.Meta.Simp.Context
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.reflectsIsomorphisms_forget : ∀ {R : Type u} [inst : CommRing R], (CategoryTheory.forget (CommBialgCat R)).ReflectsIsomorphisms
-- Mathlib.Algebra.Lie.Basic
LieEquiv.instLinearEquivClass : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂], LinearEquivClass (L₁ ≃ₗ⁅R⁆ L₂) R L₁ L₂
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.coe_mapRingHom_eq_coe_map : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : RingHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  ⇑(RatFunc.mapRingHom φ hφ) = ⇑(RatFunc.map φ hφ)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_card_finite_toFinset : ∀ {α : Type u_1} {s : Set α} (hs : s.Finite), Nat.card ↑s = hs.toFinset.card
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- The arithmetic-geometric mean of two `NNReal`s, defined as the infimum of arithmetic means.  -/
NNReal.agm : NNReal → NNReal → NNReal
-- Mathlib.Data.Real.Pointwise
Real.mul_iInf_of_nonpos : ∀ {ι : Sort u_1} {r : ℝ}, r ≤ 0 → ∀ (f : ι → ℝ), r * ⨅ i, f i = ⨆ i, r * f i
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.smul_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε} {c : ENNReal},
  MeasureTheory.MemLp f p μ → c ≠ ⊤ → MeasureTheory.MemLp f p (c • μ)