mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodInverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') (f : CategoryTheory.StructuredArrow S T × CategoryTheory.StructuredArrow S' T'),
  (CategoryTheory.StructuredArrow.prodInverse S S' T T').obj f = CategoryTheory.StructuredArrow.mk (f.1.hom, f.2.hom)
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.glueDist.match_1.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} (motive : X ⊕ Y → X ⊕ Y → Sort u_3) (x y : X)
  (h_1 : (x y : X) → motive (Sum.inl x) (Sum.inl y)) (h_2 : (x y : Y) → motive (Sum.inr x) (Sum.inr y))
  (h_3 : (x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) (h_4 : (x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)),
  (match Sum.inl x, Sum.inl y with
    | Sum.inl x, Sum.inl y => h_1 x y
    | Sum.inr x, Sum.inr y => h_2 x y
    | Sum.inl x, Sum.inr y => h_3 x y
    | Sum.inr x, Sum.inl y => h_4 x y) =
    h_1 x y
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trList.match_1.splitter : (motive : List ℕ → Sort u_1) →
  (x : List ℕ) → (Unit → motive []) → ((n : ℕ) → (ns : List ℕ) → motive (n :: ns)) → motive x
-- Mathlib.Data.Fin.Basic
Fin.val_injective : ∀ {n : ℕ}, Function.Injective Fin.val
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_inj : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x y : HahnSeries Γ R},
  x.coeff = y.coeff ↔ x = y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃_hom_hom₃ : ∀ {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] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₃ : T₁.obj₃ ≅ T₂.obj₃)
  (comm :
    CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map e₁.hom) =
      CategoryTheory.CategoryStruct.comp e₃.hom T₂.mor₃),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃ T₁ T₂ hT₁ hT₂ e₁ e₃ comm).hom.hom₃ = e₃.hom
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ],
  Summable f L →
    ∀ {G : Type u_4} [inst_4 : FunLike G α γ] [AddMonoidHomClass G α γ] (g : G), Continuous ⇑g → Summable (⇑g ∘ f) L
-- Init.Data.Int.Linear
Int.Internal.Linear.emod_nonneg : ∀ (x y : ℤ), (y != 0) = true → -1 * (x % y) ≤ 0
-- Lean.Meta.Tactic.Grind.Core
/-- The fields `target?` and `proof?` in `e`'s `ENode` are encoding a transitivity proof
from `e` to the root of the equivalence class
This method "inverts" the proof, and makes it to go from the root of the equivalence class to `e`.

We use this method when merging two equivalence classes.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.invertTrans : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : Unit → motive none) (a : α),
  x = some a →
    (match x with
      | some a => h_1 a
      | none => h_2 ()) ≍
      h_1 a
-- Mathlib.Tactic.GrindAttrs
/-- The `compactness` attribute is a custom grind-set specialized to prove that sets are compact.
It is called by the `compactness` tactic.  -/
Lean.Parser.Attr.compactness! : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.ext : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {D1 D2 : LieDerivation R L M}, (∀ (a : L), D1 a = D2 a) → D1 = D2
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`.  -/
Submodule.starProjection_le_starProjection_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U.starProjection ≤ V.starProjection ↔ U ≤ V
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.sigmaFinite_of_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α)
  [hs : MeasureTheory.SigmaFinite μ], ν ≤ μ → MeasureTheory.SigmaFinite ν
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey?.isSome = true
-- Lean.LocalContext
Lean.LocalDecl.kind : Lean.LocalDecl → Lean.LocalDeclKind
-- Mathlib.Data.Nat.Find
Nat.findGreatest.eq_2 : ∀ (P : ℕ → Prop) [inst : DecidablePred P] (n : ℕ),
  Nat.findGreatest P n.succ = if P (n + 1) then n + 1 else Nat.findGreatest P n
-- Lean.Elab.BindersUtil
Lean.Elab.Term.clearInMatch : Lean.Syntax → Array Lean.Ident → Lean.MacroM Lean.Syntax
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.integral_simps_proc : Lean.ParserDescr
-- Init.Data.Ord.Basic
instOrdBitVec : {n : ℕ} → Ord (BitVec n)
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.debugAssertions : Lean.Option Bool
-- Mathlib.Analysis.CStarAlgebra.Fuglede
_private.Mathlib.Analysis.CStarAlgebra.Fuglede.0.expMulMulExp_const : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b],
  SemiconjBy x a b → ∀ (z : ℂ), expMulMulExp✝ a b x z = x
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_mono' : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : Preorder M] [MulLeftMono M],
  Monotone fun f => ∏ i, f i
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_dif : ∀ {M : Type u_2} [inst : AddCommMonoid M] {p : Prop} [inst_1 : Decidable p] (f : p → M),
  ∑ᶠ (i : p), f i = if h : p then f h else 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₁_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃) {Z_1 : C}
  (h : A₁ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) h) =
    CategoryTheory.CategoryStruct.comp x₁ h
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.GState.mk.injEq : ∀ (propToFVar propToFVar_1 : Lean.ExprMap Lean.Expr),
  ({ propToFVar := propToFVar } = { propToFVar := propToFVar_1 }) = (propToFVar = propToFVar_1)
-- Lean.Meta.Sym.Pattern
/-- Attempts to solve a unification constraint `t =?= s` where `t` has the form `?m a₁ ... aₙ`
and satisfies the Miller pattern condition (all `aᵢ` are distinct, newly-introduced free variables).

If successful, assigns `?m := fun x₁ ... xₙ => s` and returns `true`.
Returns `false` if:
- `tFn` is not a metavariable
- `t` does not satisfy the Miller pattern condition
- The assignment would violate scope (free variables in `fun x₁ ... xₙ => s` not in scope of `?m`)

The `tFn` parameter must equal `t.getAppFn` (enforced by the proof argument).

Remark: `t` may be of the form `?m`.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryAssignMillerPattern : (tFn t : Lean.Expr) → Lean.Expr → tFn = t.getAppFn → Lean.Meta.Sym.DefEqM✝ Lean.LBool
-- Mathlib.Analysis.Normed.Operator.Extend
ContinuousLinearMap.extend_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : UniformSpace E] [inst_2 : IsUniformAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : UniformSpace F]
  [inst_5 : IsUniformAddGroup F] [inst_6 : T0Space F] [inst_7 : AddCommMonoid Eₗ] [inst_8 : UniformSpace Eₗ]
  [inst_9 : ContinuousAdd Eₗ] [inst_10 : Semiring 𝕜] [inst_11 : Semiring 𝕜₂] [inst_12 : Module 𝕜 E]
  [inst_13 : Module 𝕜₂ F] [inst_14 : Module 𝕜 Eₗ] [inst_15 : ContinuousConstSMul 𝕜 Eₗ]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_17 : CompleteSpace F] {e : E →L[𝕜] Eₗ},
  DenseRange ⇑e → IsUniformInducing ⇑e → ContinuousLinearMap.extend 0 e = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorphOfImageEq_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t), ↑(e.toOpenPartialHomeomorphOfImageEq s hs t h) = ⇑e
-- Lean.Meta.Basic
/-- `whnf` with reducible transparency. -/
Lean.Meta.whnfR : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instSDiffOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → SDiff (Std.DHashMap.Raw α β)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.smul_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} {R : Type u_6} [inst_4 : Semiring R]
  [inst_5 : DistribMulAction R M] [inst_6 : ContinuousConstSMul R M] (r : R),
  v.MutuallySingular w → (r • v).MutuallySingular w
-- Mathlib.Topology.NhdsWithin
nhdsWithin_le_of_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α}, s ∈ nhdsWithin a t → nhdsWithin a t ≤ nhdsWithin a s
-- Mathlib.Logic.Function.Defs
Function.flip_def : ∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {f : α → β → φ}, flip f = fun b a => f a b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ≠ Q 0 * P 2 →
            W.negAddY P Q / W.addZ P Q =
              W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Mathlib.Order.Filter.Lift
Filter.lift_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Set α → Filter β},
  f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.lift g₁ ≤ f₂.lift g₂
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_eq_zero : ∀ {c : Cardinal.{u}}, Cardinal.toNat c = 0 ↔ c = 0 ∨ Cardinal.aleph0 ≤ c
-- Init.Data.String.Defs
String.utf8ByteSize_append : ∀ {s t : String}, (s ++ t).utf8ByteSize = s.utf8ByteSize + t.utf8ByteSize
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` has a formal Taylor series `p` up to order `1` on `{x} ∪ s`, where `s` is a convex set,
and `‖p x 1‖₊ < K`, then `f` is `K`-Lipschitz in a neighborhood of `x` within `s`.  -/
HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {p : E → FormalMultilinearSeries ℝ E F} {s : Set E} {x : E},
  HasFTaylorSeriesUpToOn 1 f p (insert x s) →
    Convex ℝ s → ∀ (K : NNReal), ‖p x 1‖₊ < K → ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_whiskerRight : ∀ {X Y X' : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y') (f : X ⟶ X'),
  (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) = (e₁.map f).tensor e₂
-- Lean.Elab.App
Lean.Elab.Term.ElabElimInfo.mk : Lean.Expr → Lean.Expr → ℕ → Array ℕ → Lean.Elab.Term.ElabElimInfo
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.push : Array Lean.MessageData → Option Lean.MessageData → Array Lean.MessageData
-- Mathlib.Analysis.Calculus.Gradient.Basic
/-- `f` has the gradient `f'` at the point `x` within the subset `s` if
`f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` where `x'` converges to `x` inside `s`.  -/
HasGradientWithinAt : {𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → Set F → F → Prop
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j / f k) κ μ
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `locallyLipschitzOn_inv_iff`. -/
LocallyLipschitzOn.inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E} {s : Set α},
  LocallyLipschitzOn s f → LocallyLipschitzOn s f⁻¹
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
one_lt_pow' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, 1 < a → ∀ {k : ℕ}, k ≠ 0 → 1 < a ^ k
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsTorsionQuot.inf : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {I J K : Ideal A},
  F.IsTorsionQuot I K → F.IsTorsionQuot J K → F.IsTorsionQuot (I ⊓ J) K
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a presheaf on `Stonean` whose postcomposition with the
forgetful functor preserves finite products.
 -/
Condensed.ofSheafForgetStonean : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type u_3} →
          [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_3 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.ReflectsFiniteProducts (CategoryTheory.forget A)] →
                (F : CategoryTheory.Functor Stoneanᵒᵖ A) →
                  [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] → Condensed A
-- Std.Http.Protocol.H1.Error
/-- Request URI is too long.
 -/
Std.Http.Protocol.H1.Error.uriTooLong : Std.Http.Protocol.H1.Error
-- Mathlib.Order.FixedPoints
OrderHom.lfp_le_map : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, OrderHom.lfp f ≤ a → OrderHom.lfp f ≤ f a
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- When `C` has finite products indexed by `J`, `W : MorphismProperty C` contains
identities and is stable under products indexed by `J`,
then any localization functor for `W` preserves finite products indexed by `J`.  -/
CategoryTheory.Localization.preservesProductsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.ContainsIdentities]
  (J : Type) [Finite J] [CategoryTheory.Limits.HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) L
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfToPiQuotient_inj : ∀ {R : Type u} [inst : Ring R] {ι : Type u_1} (I : ι → Ideal R) [inst_1 : ∀ (i : ι), (I i).IsTwoSided],
  Function.Injective ⇑(Ideal.quotientInfToPiQuotient I)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMVarsDelayed : Lean.Options → Bool
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_smul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5}
  [inst_8 : DistribSMul S F] [inst_9 : SMulCommClass 𝕜₂ S F] [inst_10 : ContinuousConstSMul S F] {c : S}
  {f : E →SWOT[σ] F}, (c • f).toCLM = c • f.toCLM
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `K⟮X⟯` is the field of fractions of the polynomials over `K`.  -/
RatFunc.instIsFractionRingPolynomial : ∀ (K : Type u) [inst : CommRing K] [inst_1 : IsDomain K], IsFractionRing (Polynomial K) (RatFunc K)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_def : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α}, s.gcd f = (Multiset.map f s.val).gcd
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.continuousAt : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {a : A}, ContinuousAt (⇑e) a
-- Init.Data.SInt.Lemmas
UInt32.ofBitVec_int32ToBitVec : ∀ (x : Int32), { toBitVec := x.toBitVec } = x.toUInt32
-- Mathlib.Data.Finset.Defs
/-- `val` contains no duplicates  -/
Finset.nodup : ∀ {α : Type u_4} (self : Finset α), self.val.Nodup
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn.eq : ∀ {motive_1 : Lean.Language.SnapshotTree → Sort u}
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u}
  {motive_5 : Task Lean.Language.SnapshotTree → Sort u} (t : Lean.Language.SnapshotTree)
  (F_1 : (t : Lean.Language.SnapshotTree) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_3 t → motive_4 t)
  (F_5 : (t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 = F_1 t (Lean.Language.SnapshotTree.brecOn.go t F_1 F_2 F_3 F_4 F_5).2
-- Init.Data.Subtype.Order
Subtype.instLawfulOrderLT : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {P : α → Prop}, Std.LawfulOrderLT (Subtype P)
-- Mathlib.Data.Fintype.Order
Set.Finite.exists_le : ∀ {α : Type u_2} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {s : Set α}, s.Finite → ∃ M, ∀ i ∈ s, i ≤ M
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.funCongrLeft_id : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type u_10},
  LinearEquiv.funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams.toTextDocumentPositionParams : Lean.Lsp.CompletionParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.measure_ne_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → U.Nonempty → μ U ≠ 0
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.pow : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (n : ℕ), IsUnit a → IsUnit (a ^ n)
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabSimpArg : Lean.Meta.ConfigWithKey →
  Bool → Lean.Elab.Tactic.SimpKind → Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.ElabSimpArgResult
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.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)).QuasiFinite) →
    AlgebraicGeometry.LocallyQuasiFinite f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_alter : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α} {f : Option β → Option β} (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.Const.alter a f t htb).impl.toListModel.Perm
      (Std.Internal.List.Const.alterKey a f t.toListModel)
-- Mathlib.ModelTheory.Substructures
/-- Substructures of a structure form a complete lattice.  -/
FirstOrder.Language.Substructure.instCompleteLattice : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → CompleteLattice (L.Substructure M)
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, Polynomial.toLaurent f = 0 ↔ f = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- The composition of two right exact functors is right exact.  -/
CategoryTheory.Limits.comp_preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits F]
  [CategoryTheory.Limits.PreservesFiniteColimits G], CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- `LeftPreLieRing`s are `NonUnitalNonAssocRing`s such that the `associator` is symmetric in the
first two variables.  -/
LeftPreLieRing : Type u_1 → Type u_1
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.propagateUniversesToConstructors.collectConstraints : ℕ →
  List Lean.InductiveType → Lean.Level → ℤ → StateT (Lean.Elab.Command.AccLevelState✝ × Lean.LMVarIdSet) Lean.MetaM Unit
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.join_map_ret : ∀ {α : Type u} (s : Stream'.WSeq α), (Stream'.WSeq.map Stream'.WSeq.ret s).join ~ʷ s
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- An intermediate field of `E / F` contains the separable closure of `F` in `E`
if `E` is purely inseparable over it.  -/
separableClosure_le : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [h : IsPurelyInseparable (↥L) E], separableClosure F E ≤ L