mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_toInt64 : ∀ (n : ISize) (h : System.Platform.numBits = 32), n.toInt64.toBitVec = BitVec.signExtend 64 (n.toBitVec32 h)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.LocQuiver.mk : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} → C → CategoryTheory.Localization.Construction.LocQuiver W
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂AlgHom_apply : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (g : σ → S₁) (P : MvPolynomial σ R), (MvPolynomial.eval₂AlgHom R g) P = (MvPolynomial.eval₂Hom (algebraMap R S₁) g) P
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_congr : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Ring S] [inst_3 : LinearOrder S]
  [inst_4 : FloorRing R] [inst_5 : FloorRing S] {a : R} {b : S}, (∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b) → ⌊a⌋ = ⌊b⌋
-- Mathlib.GroupTheory.Finiteness
/-- A finitely generated monoid has a minimal generating set.  -/
AddSubmonoid.exists_minimal_closure_eq_top : ∀ (M : Type u_1) [inst : AddMonoid M] [AddMonoid.FG M], ∃ S, Minimal (fun S => AddSubmonoid.closure ↑S = ⊤) S
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsCocontinuousOverMapOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.Over.map f).IsCocontinuous (J.over X) (J.over Y)
-- Mathlib.Algebra.Order.Module.Defs
smulPosMono_iff_smulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : LinearOrder α] [inst_2 : LinearOrder β] [inst_3 : Zero β],
  SMulPosMono α β ↔ SMulPosReflectLT α β
-- Mathlib.Algebra.Order.ToIntervalMod
_private.Mathlib.Algebra.Order.ToIntervalMod.0.toIxxMod_trans : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {x₁ x₂ x₃ x₄ : α},
  toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁ →
    toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂ →
      toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₁
-- Std.Http.Data.Status
Std.Http.Status.tooManyRequests.sizeOf_spec : sizeOf Std.Http.Status.tooManyRequests = 1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_le_lift : ∀ {α : Type u} {β : Type v} {f : α → β},
  Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) ≤ Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] M) (n : ℕ),
  LinearMap.rTensor N f ^ n = LinearMap.rTensor N (f ^ n)
-- Lean.Environment
/-- Phases for which the import's IR is available.  -/
Lean.EffectiveImport.irPhases : Lean.EffectiveImport → Lean.IRPhases
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a.tdiv b
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
/-- If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
satisfying `p` cover the space arbitrarily well, then `μ` is inner regular with respect to
predicates `p` and `q`.
 -/
MeasureTheory.innerRegularWRT_of_exists_compl_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
  (∀ (A B : Set α), p A → q B → p (A ∩ B)) → (∀ (ε : ENNReal), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) → μ.InnerRegularWRT p q
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  (S : NonUnitalStarSubalgebra R B) (f : F), ↑(NonUnitalStarSubalgebra.comap f S) = ⇑f ⁻¹' ↑S
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.fixedReduce_eq_one : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (e : V ≃ₗ[R] V),
  e.fixedReduce = LinearEquiv.refl R (V ⧸ (↑e).fixedSubmodule) ↔ ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Ioo : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.image (Fin.castLE h) (Finset.Ioo a b) = Finset.Ioo (Fin.castLE h a) (Fin.castLE h b)
-- Mathlib.CategoryTheory.Action.Monoidal
/-- An isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on `Gⁿ⁺¹` and
`G` but trivially on `Gⁿ`. The map sends `(g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`,
and the inverse is `(g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).`  -/
Action.diagonalSuccIsoTensorTrivial : (G : Type u) →
  [inst : Group G] →
    (n : ℕ) →
      Action.diagonal G (n + 1) ≅
        CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G (Fin n → G))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array
/-- Simplification procedure for `#[...][n]!` for `n` a `Nat` literal.  -/
Array.reduceGetElem! : Lean.Meta.Simp.DSimproc
-- Batteries.Tactic.GeneralizeProofs
/-- Runs `x` with an increased recursion depth and the initial local context, clearing `fvars`.  -/
Batteries.Tactic.GeneralizeProofs.MAbs.withRecurse : {α : Type} → Batteries.Tactic.GeneralizeProofs.MAbs α → Batteries.Tactic.GeneralizeProofs.MAbs α
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqTo_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (j : ι), CategoryTheory.Arrow.Hom.left (f.sqTo j) = f.prev j
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.tgt_eq : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) e.edge = x₁
-- Mathlib.Topology.Maps.Basic
IsClosedMap.lift'_closure_map_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → Continuous f → ∀ (F : Filter X), (Filter.map f F).lift' closure = Filter.map f (F.lift' closure)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.one : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] → [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → One (M₁ →L[R₁] M₁)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.mk : {R : Type u_1} → {A : Type u_2} → R × A → Unitization R A
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t t_1 : Std.DTreeMap α β cmp) (e_t : t = t_1)
  (h : t.isEmpty = false), t.maxKey h = t_1.maxKey ⋯
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_compHom : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z) (x : ↥X) (hx : x ∈ (f.compHom g).domain),
  (f.compHom g).fromSpecStalkOfMem hx = CategoryTheory.CategoryStruct.comp (f.fromSpecStalkOfMem hx) g
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.Scheme.Hom.app_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ [AlgebraicGeometry.IsClosedImmersion f],
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U))
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.congr.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} (e : (i : ι) → G i ≃+ G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)),
  AddCommGroup.DirectLimit.congr e he =
    (AddCommGroup.DirectLimit.map (fun x => ↑(e x)) he).toAddEquiv
      (AddCommGroup.DirectLimit.map (fun i => ↑(e i).symm) ⋯) ⋯ ⋯
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseQuery : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.Query
-- Mathlib.Algebra.Group.Graph
/-- **Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
monoid isomorphism `f' : H ≃ I`.  -/
AddMonoidHom.exists_addEquiv_mrange_eq_mgraph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : AddMonoid G] [inst_1 : AddMonoid H] [inst_2 : AddMonoid I]
  {f : G →+ H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, AddMonoidHom.mrange f = e.toAddMonoidHom.mgraph
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.extend_comp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f : α ↪ δ) (g : BoundedContinuousFunction α β)
  (h : BoundedContinuousFunction δ β), ⇑(BoundedContinuousFunction.extend f g h) ∘ ⇑f = ⇑g
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.epimorphisms.infer_property : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.Epi f],
  CategoryTheory.MorphismProperty.epimorphisms C f
-- Init.GetElem
List.instGetElemNatLtLength : {α : Type u_1} → GetElem (List α) ℕ α fun as i => i < as.length
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h i)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) h_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonLocationLink : Lean.FromJson Lean.Lsp.LocationLink
-- Lean.PrettyPrinter.Delaborator.DeclWithSig
Lean.PrettyPrinter.Delaborator.declSigWithId.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm_inv_mul_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `ZeroHomClass F M N` into an actual
`ZeroHom`. This is declared as the default coercion from `F` to `ZeroHom M N`.  -/
ZeroHomClass.toZeroHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : Zero M] → [inst_1 : Zero N] → [inst_2 : FunLike F M N] → [ZeroHomClass F M N] → F → ZeroHom M N
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mul_bddBelow_range_add : ∀ {E : Type u_3} [inst : CommGroup E] {p q : GroupSeminorm E} {x : E}, BddBelow (Set.range fun y => p y + q (x / y))
-- Init.Data.Nat.Basic
Nat.lt_add_of_pos_left : ∀ {k n : ℕ}, 0 < k → n < k + n
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.mk.sizeOf_spec : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} [inst_2 : SizeOf G] [inst_3 : SizeOf H]
  (toEquiv : G ≃ H) (map_add_const' : ∀ (x : G), toEquiv.toFun (x + a) = toEquiv.toFun x + b),
  sizeOf { toEquiv := toEquiv, map_add_const' := map_add_const' } = 1 + sizeOf toEquiv
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If any finite measure has a Lebesgue decomposition with respect to `ν`,
then the same is true for any s-finite measure.  -/
MeasureTheory.Measure.HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite μ],
  (∀ (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ], μ.HaveLebesgueDecomposition ν) →
    μ.HaveLebesgueDecomposition ν
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induce_bot : ∀ {V : Type u_1} (s : Set V), SimpleGraph.induce s ⊥ = ⊥
-- Mathlib.Data.PNat.Factors
PNat.factorMultiset_pow : ∀ (n : ℕ+) (m : ℕ), (n ^ m).factorMultiset = m • n.factorMultiset
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_eq_zero_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin (n + 1)} {b : Fin n}, a ≠ 0 → (a.succAbove b = 0 ↔ b = 0)
-- Init.Data.List.Attach
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`.  -/
List.map_attach_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : { x // x ∈ l } → β},
  List.map f l.attach = List.pmap (fun a h => f ⟨a, h⟩) l ⋯
-- Mathlib.Algebra.Group.Invertible.Basic
commute_invOf : ∀ {M : Type u_1} [inst : One M] [inst_1 : Mul M] (m : M) [inst_2 : Invertible m], Commute m ⅟m
-- Lean.Server.AsyncList
Lean.AsyncList.cons.injEq : ∀ {ε : Type u} {α : Type v} (hd : α) (tl : Lean.AsyncList ε α) (hd_1 : α) (tl_1 : Lean.AsyncList ε α),
  (Lean.AsyncList.cons hd tl = Lean.AsyncList.cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instRepr : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Repr α] → [(a : α) → Repr (β a)] → Repr (Std.DTreeMap α β cmp)
-- Mathlib.CategoryTheory.Action.Concrete
/-- Given a family `F` of types with `G`-actions, this is the limit cone demonstrating that the
product of `F` as types is a product in the category of `G`-sets.  -/
Action.ofMulActionLimitCone : {ι : Type v} →
  (G : Type (max v u)) →
    [inst : Monoid G] →
      (F : ι → Type (max v u)) →
        [inst_1 : (i : ι) → MulAction G (F i)] →
          CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun i => Action.ofMulAction G (F i))
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- The property of objects that are *equal* to `colimit F` for some
functor `F : J ⥤ C` where all `F.obj j` satisfy `P`.  -/
CategoryTheory.ObjectProperty.strictColimitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → CategoryTheory.ObjectProperty C
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.nnnorm_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : StarRing A]
  [CStarRing A] (a : DoubleCentralizer 𝕜 A), ‖a.toProd.2‖₊ = ‖a‖₊
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_one_inj : ∀ {ι : Type u_1} (M₀ : Type u_4) [inst : MulZeroOneClass M₀] {s t : Set ι} [Nontrivial M₀],
  s.indicator 1 = t.indicator 1 → s = t
-- Init.Data.Repr
instReprAtomUInt8 : ReprAtom UInt8
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.sub_mem_iff_right : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, x ∈ p → (x - y ∈ p ↔ y ∈ p)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrRight` as a `RingEquiv`.  -/
LocallyConstant.congrRightRingEquiv : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        [inst_1 : Semiring Y] → [inst_2 : Semiring Z] → Y ≃+* Z → LocallyConstant X Y ≃+* LocallyConstant X Z
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.lift_π : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] (c : CategoryTheory.Limits.Cone F) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.lift F c)
      (CategoryTheory.Limits.weakLimit.π F j) =
    c.π.app j
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
/-- An integral domain $R$ is integrally closed if there exists a set of prime ideals $S$ such that
$\bigcap_{\mathfrak{p} \in S} R_{\mathfrak{p}} = R$ and for every $\mathfrak{p} \in S$,
$R_{\mathfrak{p}}$ is integrally closed.  -/
IsIntegrallyClosed.of_localization : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (S : Set (PrimeSpectrum R)),
  (∀ p ∈ S, IsIntegrallyClosed (Localization.AtPrime p.asIdeal)) →
    ⨅ p ∈ S, Localization.subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯ = ⊥ → IsIntegrallyClosed R
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If a function is continuous outside of a countable set, then it is strongly measurable.  -/
ContinuousOn.stronglyMeasurable_of_countable_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [MeasurableSingletonClass α] [inst_4 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  [h : SecondCountableTopologyEither α β] {f : α → β} {s : Set α},
  ContinuousOn f s → sᶜ.Countable → MeasureTheory.StronglyMeasurable f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} (k_beq : (k == k') = true) {v : β k},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
        ⟨k, v⟩ ∈ toInsert →
          Std.Internal.List.getValueCast? k' (Std.Internal.List.insertList l toInsert) = some (cast ⋯ v)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SMulMemClass.mk : ∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [inst : SMul R M] [inst_1 : SetLike S M],
  (∀ {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s) → SMulMemClass S R M
-- Lean.Message
Lean.MessageLog.errorsToInfos : Lean.MessageLog → Lean.MessageLog
-- Mathlib.Lean.Meta
/-- Get the type the given metavariable after instantiating metavariables and cleaning up
annotations.  -/
Lean.MVarId.getType'' : Lean.MVarId → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.category_comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (α : X.Hom Y)
  (β : Y.Hom Z) (a : X.I), (CategoryTheory.CategoryStruct.comp α β).f a = β.f (α.f a)
-- Init.Data.List.Perm
List.Pairwise.perm : ∀ {α : Type u_1} {R : α → α → Prop} {l l' : List α},
  List.Pairwise R l → l.Perm l' → (∀ {x y : α}, R x y → R y x) → List.Pairwise R l'
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real sine function, defined as the real part of the complex sine  -/
Real.sin : ℝ → ℝ
-- Mathlib.Analysis.Calculus.FDeriv.Pow
HasFDerivWithinAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → ∀ (n : ℕ), HasFDerivWithinAt (fun x => f x ^ n) ((n • f x ^ (n - 1)) • f') s x
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_id_eq_join₁ : ∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R], MvPolynomial.aeval id = MvPolynomial.join₁
-- Mathlib.Data.NNReal.Defs
NNReal.mulLeftMono : MulLeftMono NNReal
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.exists_eq : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.Scheme.JointlySurjective K] (𝒰 : AlgebraicGeometry.Scheme.Cover K X) (x : ↥X), ∃ i y, (𝒰.f i) y = x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.min?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], t₁.Equiv t₂ → t₁.min? = t₂.min?
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The projection map from `functorObj M N n` to `M m`, when `m < n`  -/
CategoryTheory.Limits.SequentialProduct.functorObjProj_pos : {C : Type u_1} →
  {M N : ℕ → C} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasCountableProducts C] →
        (n m : ℕ) → m < n → (CategoryTheory.Limits.SequentialProduct.functorObj M N n ⟶ M m)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.i_mul_j : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (self : QuaternionAlgebra.Basis A c₁ c₂ c₃), self.i * self.j = self.k
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.isLUB_Iio : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], Order.IsSuccPrelimit a → IsLUB (Set.Iio a) a
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.congr_arg : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) {x y : A}, x = y → f x = f y
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_subset_compl : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.neighborSet v ⊆ {v}ᶜ
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.mk.sizeOf_spec : ∀ (name : List Lean.Name) (stx selection : Lean.Syntax) (prevSiblings : Array Lean.Lsp.DocumentSymbol),
  sizeOf { name := name, stx := stx, selection := selection, prevSiblings := prevSiblings } =
    1 + sizeOf name + sizeOf stx + sizeOf selection + sizeOf prevSiblings
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.top_join : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.join Lean.Order.top P = Lean.Order.top
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for group homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`.  -/
MonoidHom.exists_range_eq_graph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : Group I] {f : G →* H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', f.range = f'.graph
-- Mathlib.Order.Antisymmetrization
AntisymmRel.image : ∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : Preorder β],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → ∀ {f : α → β}, Monotone f → AntisymmRel (fun x1 x2 => x1 ≤ x2) (f a) (f b)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Type of the semantic token.  -/
Lean.Server.FileWorker.LeanSemanticToken.type : Lean.Server.FileWorker.LeanSemanticToken → Lean.Lsp.SemanticTokenType