mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Sylow
Sylow.stabilizer_eq_normalizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G), MulAction.stabilizer G P = Subgroup.normalizer ↑P
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.image : ∀ {α : Type u} {β : Type v} {s : Set α} (f : α → β), s.Finite → (f '' s).Finite
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_singleton_append : ∀ {m n : ℤ}, m + 1 < n → (m<...n).toArray = #[m + 1] ++ ((m + 1)<...n).toArray
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instBEqKey : BEq Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuousAt_infty' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] {f : OnePoint X → Y},
  ContinuousAt f OnePoint.infty ↔
    Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) (nhds (f OnePoint.infty))
-- Mathlib.Topology.ShrinkingLemma
/-- A family of sets that form a partial refinement of `u`.  -/
ShrinkingLemma.PartialRefinement.toFun : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} → {s : Set X} → {p : Set X → Prop} → ShrinkingLemma.PartialRefinement u s p → ι → Set X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The comparison morphism for the coequalizer of `f,g`.  -/
CategoryTheory.Limits.coequalizerComparison : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) →
        {D : Type u₂} →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
            (G : CategoryTheory.Functor C D) →
              [inst_2 : CategoryTheory.Limits.HasCoequalizer f g] →
                [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] →
                  CategoryTheory.Limits.coequalizer (G.map f) (G.map g) ⟶ G.obj (CategoryTheory.Limits.coequalizer f g)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverage : AlgebraicGeometry.Scheme.proetalePrecoverage ≤ AlgebraicGeometry.Scheme.fpqcPrecoverage
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_and : ∀ (a b : UInt64), (a &&& b).toUInt16 = a.toUInt16 &&& b.toUInt16
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instRespectsIsoLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], (W.limitsOfShape J).RespectsIso
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Add.toVAddAddOpposite` is faithful when there is a (left) identity.  -/
instFaithfulVAddAddOpposite : ∀ (R : Type u_4) [inst : AddZeroClass R], FaithfulVAdd Rᵃᵒᵖ R
-- Mathlib.Algebra.Group.Support
Function.support_sub : ∀ {α : Type u_1} {G : Type u_3} [inst : SubtractionMonoid G] (f g : α → G),
  (Function.support fun x => f x - g x) ⊆ Function.support f ∪ Function.support g
-- Init.Data.List.Sublist
List.Sublist.of_sublist_append_left : ∀ {α : Type u_1} {l l₂ l₁ : List α}, (∀ a ∈ l, a ∉ l₂) → l.Sublist (l₁ ++ l₂) → l.Sublist l₁
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.normedMk_apply : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (a : M),
  SeparationQuotient.normedMk a = (↑SeparationQuotient.mkAddMonoidHom).toFun a
-- Mathlib.NumberTheory.Modular
/-- Classify possible `d` when `c = 1`.  -/
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.cases_d_of_c_eq_one : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    ‖UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤
        1 →
      ↑g 1 0 = 1 → |↑g 1 1| ≤ 1
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoidHom.toAddEquiv_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (g : N →+ M)
  (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N), ⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobiMatrix_reindex : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ)
  [inst_3 : Fintype σ'] [inst_4 : DecidableEq σ'] [inst_5 : Fintype σ] [inst_6 : DecidableEq σ],
  (P.reindex e f).jacobiMatrix = ((Matrix.reindex f.symm f.symm) P.jacobiMatrix).map ⇑(MvPolynomial.rename ⇑e.symm)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_sub_C_ne_zero : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] (r : R), Polynomial.X - Polynomial.C r ≠ 0
-- Init.Data.List.Perm
List.Perm.flatMap_right : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (f : α → List β),
  l₁.Perm l₂ → (List.flatMap f l₁).Perm (List.flatMap f l₂)
-- Mathlib.Data.Rel
SetRel.isRefl_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsRefl], SetRel.IsRefl (Prod.map f f ⁻¹' R)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- subsemigroups of a monoid form a complete lattice.  -/
Subsemigroup.instCompleteLattice : {M : Type u_1} → [inst : Mul M] → CompleteLattice (Subsemigroup M)
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Law of cosines** (cosine rule), vector angle form.  -/
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (InnerProductGeometry.angle x y)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- The colimit module functor from the category of presheaves of modules
over a presheaf of rings `R` on a cofiltered category to the category
of modules over a colimit of `R`.  -/
PresheafOfModules.colimitFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      [CategoryTheory.IsCofiltered C] →
        [CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              CategoryTheory.Limits.IsColimit cR → CategoryTheory.Functor (PresheafOfModules R) (ModuleCat ↑cR.pt)
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.permMark : Lean.Meta.Grind.TopSort.State → Std.HashSet Lean.Expr
-- Mathlib.Algebra.Group.Defs
/-- A `SubNegMonoid` where `-0 = 0`.  -/
SubNegZeroMonoid : Type u_2 → Type u_2
-- Std.Time.DateTime.PlainDateTime
Std.Time.instReprPlainDateTime : Repr Std.Time.PlainDateTime
-- Mathlib.Algebra.DirectSum.Ring
/-- The `Ring` derived from `GSemiring A`.  -/
DirectSum.nonAssocRing : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] →
        [inst_1 : Add ι] → [DirectSum.GNonUnitalNonAssocSemiring A] → NonUnitalNonAssocRing (DirectSum ι fun i => A i)
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr.match_1.splitter : {α : Type u_1} →
  {γ : Type u_3} →
    (motive : List α → γ → Sort u_2) →
      (x : List α) →
        (x_1 : γ) → ((c : γ) → motive [] c) → ((y : α) → (yr : List α) → (c : γ) → motive (y :: yr) c) → motive x x_1
-- Mathlib.MeasureTheory.Measure.Regular
/-- Given a weakly regular measure, any measurable set of finite mass can be approximated from
inside by closed sets.  -/
MeasurableSet.measure_eq_iSup_isClosed_of_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] ⦃A : Set α⦄, MeasurableSet A → μ A ≠ ⊤ → μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsClosed K), μ K
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ : Std.IterM m (Std.IterM m β)},
  it₁.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := none } } Std.IterStep.done
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inl_leftDistrib_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C]
  {X Y Z Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inl) h
-- Mathlib.Order.Category.PartOrd
/-- The underlying `OrderHom`.  -/
PartOrd.Hom.hom' : {X Y : PartOrd} → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_image_coe_quotient : ∀ {G : Type u_1} [inst : AddCommGroup G] (s : Set G),
  AddAction.stabilizer (G ⧸ AddAction.stabilizer G s) (QuotientAddGroup.mk '' s) = ⊥
-- Mathlib.Data.List.Basic
List.forall_mem_iff_getElem : ∀ {α : Type u} {l : List α} {p : α → Prop}, (∀ x ∈ l, p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]
-- Mathlib.Order.BourbakiWitt
/-- **Alias** of `ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_isAdmissible`. -/
ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_isAdmissible : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → ChainCompletePartialOrder.IsAdmissible x f {y | ChainCompletePartialOrder.IsExtremePt x f y}
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.isSublist.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((x : List α) → motive [] x) →
        ((x : List α) → (x = [] → False) → motive x []) →
          ((hd₁ : α) → (tl₁ : List α) → (hd₂ : α) → (tl₂ : List α) → motive (hd₁ :: tl₁) (hd₂ :: tl₂)) → motive x x_1
-- Mathlib.Analysis.Complex.Tietze
TietzeExtension.of_tvs : ∀ (𝕜 : Type v) [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E]
  [CompleteSpace 𝕜] [TietzeExtension 𝕜], TietzeExtension E
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_mk' : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  (M : AddSubgroup H) [inst_2 : M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G),
  (QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = ↑(f x)
-- Init.Prelude
instDecidableEqBitVec : {w : ℕ} → DecidableEq (BitVec w)
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_mul_zpow : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a * b ^ n) (a * b ^ (n + 1)))
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.trans_toCoalgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] {e₁₂ : A ≃ₐc[R] B}
  {e₂₃ : B ≃ₐc[R] C}, ↑(e₁₂.trans e₂₃) = (↑e₁₂).trans ↑e₂₃
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_le_one_iff : ∀ {n : ℕ}, UniqueFactorizationMonoid.radical n ≤ 1 ↔ n ≤ 1
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- See `NormedSpace.toLocallyConvexSpace'` for a slightly stronger version which is not an
instance.  -/
NormedSpace.toLocallyConvexSpace : ∀ {E : Type u_6} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], LocallyConvexSpace ℝ E
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Extensionality lemma for algebra maps out of `A'[X]` over a smaller base ring than `A'`
 -/
Polynomial.algHom_ext' : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f g : Polynomial A →ₐ[R] B},
  f.comp Polynomial.CAlgHom = g.comp Polynomial.CAlgHom → f Polynomial.X = g Polynomial.X → f = g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → (∀ (k : α), Std.DTreeMap.Raw.Const.get? t₁ k = Std.DTreeMap.Raw.Const.get? t₂ k) → t₁.Equiv t₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedDeclValue.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.DeclValue pu
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A proof term provided directly to a call to `simp [ref, ...]` where `ref`
is the provided simp argument (of kind `Parser.Tactic.simpLemma`).
The `id` is a unique identifier for the call.
 -/
Lean.Meta.Origin.stx : Lean.Name → Lean.Syntax → Lean.Meta.Origin
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f : X₁ ⟶ X₂` and `g : X₂ ⟶ X₃` in the category
of cochain complexes, this is the canonical triangle
`mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧`
in the homotopy category. It is a distinguished triangle,
see `HomotopyCategory.mappingConeCompTriangleh_distinguished`.  -/
CochainComplex.mappingConeCompTriangleh : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (X₁ ⟶ X₂) → (X₂ ⟶ X₃) → CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- Variant of `fourδ₄Toδ₃` for preorders.  -/
CategoryTheory.ComposableArrows.fourδ₄Toδ₃' : {ι : Type u_1} →
  [inst : Preorder ι] →
    (i₀ i₁ i₂ i₃ i₄ : ι) →
      (hi₀₁ : i₀ ≤ i₁) →
        (hi₁₂ : i₁ ≤ i₂) →
          (hi₂₃ : i₂ ≤ i₃) →
            (hi₃₄ : i₃ ≤ i₄) →
              CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                  (CategoryTheory.homOfLE hi₂₃) ⟶
                CategoryTheory.ComposableArrows.mk₃ (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                  (CategoryTheory.homOfLE ⋯)
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
instFintypeUnitsOfDecidableEq : {α : Type u_1} → [inst : Monoid α] → [Fintype α] → [DecidableEq α] → Fintype αˣ
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.sum : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {ι : Type} {t : Finset ι} {f : ι → M → E'} {f' : ι → TangentSpace I z →L[𝕜] E'},
  (∀ i ∈ t, HasMFDerivAt% (f i) z (f' i)) → HasMFDerivAt% (∑ i ∈ t, f i) z (∑ i ∈ t, f' i)
-- Mathlib.Analysis.Convex.Intrinsic
ContinuousAffineEquiv.intrinsicClosure_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup W] [inst_3 : Module 𝕜 V] [inst_4 : Module 𝕜 W] [inst_5 : TopologicalSpace P]
  [inst_6 : TopologicalSpace Q] [inst_7 : AddTorsor V P] [inst_8 : AddTorsor W Q] (φ : P ≃ᴬ[𝕜] Q) (s : Set P),
  intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
-- Std.Http.Data.URI.Basic
Std.Http.URI.mk.injEq : ∀ (scheme : Std.Http.URI.Scheme) (authority : Option Std.Http.URI.Authority) (path : Std.Http.URI.Path)
  (query : Std.Http.URI.Query) (fragment : Option String) (scheme_1 : Std.Http.URI.Scheme)
  (authority_1 : Option Std.Http.URI.Authority) (path_1 : Std.Http.URI.Path) (query_1 : Std.Http.URI.Query)
  (fragment_1 : Option String),
  ({ scheme := scheme, authority := authority, path := path, query := query, fragment := fragment } =
      { scheme := scheme_1, authority := authority_1, path := path_1, query := query_1, fragment := fragment_1 }) =
    (scheme = scheme_1 ∧ authority = authority_1 ∧ path = path_1 ∧ query = query_1 ∧ fragment = fragment_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_reindex_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b)
      (CategoryTheory.Limits.Sigma.reindex ε f).hom =
    CategoryTheory.Limits.Sigma.ι f (ε b)
-- Init.Data.Repr
/-- Turn a value of type `α` into a `Format` at a given precedence. The precedence value can be used
to avoid parentheses if they are not necessary.
 -/
Repr.reprPrec : {α : Type u} → [self : Repr α] → α → ℕ → Std.Format
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.containsThenInsert k v).2 = t.insert k v
-- Init.Data.SInt.Lemmas
Int8.toInt_le_iSizeMaxValue : ∀ (x : Int8), x.toInt ≤ ISize.maxValue.toInt
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.id_apply : ∀ (R : Type u) [inst : CommRing R] (A : AlgCat R) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Context.mk.sizeOf_spec : ∀ (ctx : Lean.Meta.Simp.Context) (simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result),
  sizeOf { ctx := ctx, simp := simp } = 1 + sizeOf ctx
-- Lean.Util.Sorry
Lean.Declaration.hasSorry : Lean.Declaration → Bool
-- Mathlib.Analysis.Complex.Circle
Real.continuous_probChar : Continuous ⇑Real.probChar
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Bijective ⇑x)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ioc_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ ≤ b₂ → Finset.Ioc a b₁ ⊆ Finset.Ioc a b₂
-- Lean.Widget.TaggedText
/-- Like `mapM` but allows rewriting the whole subtree at `tag` nodes.  -/
Lean.Widget.TaggedText.rewriteM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      [Monad m] →
        (α → Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)) →
          Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)
-- Mathlib.Topology.UniformSpace.Defs
refl_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], Filter.principal SetRel.id ≤ uniformity α
-- Mathlib.Topology.Order.Compact
IsCompact.isLeast_sInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → IsLeast s (sInf s)
-- Init.Data.Array.Attach
Array.pmap_empty : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β), Array.pmap f #[] ⋯ = #[]
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Alternative constructor for `PreservesLeftKanExtension`, phrased in terms of
`LeftExtension.IsUniversal` instead. See `PreservesLeftKanExtension.mk_of_preserves_isUniversal`
for a similar constructor taking as input a single `LeftExtension`.  -/
CategoryTheory.Functor.PreservesLeftKanExtension.mk' : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C),
  (∀ {E : L.LeftExtension F} (a : CategoryTheory.StructuredArrow.IsUniversal E),
      Nonempty
        (CategoryTheory.StructuredArrow.IsUniversal
          ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E))) →
    G.PreservesLeftKanExtension F L
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.mk.sizeOf_spec : ∀ {γ : Type} [inst : SizeOf γ] (builtinName name : Lean.Name) (descr : String) (valueTypeName : Lean.Name)
  (evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key)
  (onAdded : Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit),
  sizeOf
      { builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey,
        onAdded := onAdded } =
    1 + sizeOf builtinName + sizeOf name + sizeOf descr + sizeOf valueTypeName
-- Mathlib.Order.Defs.PartialOrder
lt_or_eq_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → a < b ∨ a = b
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h_1) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) h_1))
-- Mathlib.Data.PEquiv
PEquiv.single_trans_of_mem : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : DecidableEq γ]
  (a : α) {b : β} {c : γ} {f : β ≃. γ}, c ∈ f b → (PEquiv.single a b).trans f = PEquiv.single a c
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.adapt_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε ε' α : Type u} {x : ExceptT ε m α} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] (f : ε → ε') (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' ps)),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => Q.2.1 (f e), Q.2.2)⦄ ExceptT.adapt f x ⦃Q⦄
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.RightFraction₂.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C} {X Y X' : C}
  {s : X' ⟶ X} {hs : W s} {f f' : X' ⟶ Y} {X'_1 : C} {s_1 : X'_1 ⟶ X} {hs_1 : W s_1} {f_1 f'_1 : X'_1 ⟶ Y},
  { X' := X', s := s, hs := hs, f := f, f' := f' } = { X' := X'_1, s := s_1, hs := hs_1, f := f_1, f' := f'_1 } →
    X' = X'_1 ∧ s ≍ s_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1
-- Init.Data.List.Pairwise
List.pairwise_map : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1} {R : α_1 → α_1 → Prop} {l : List α},
  List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l
-- Mathlib.Data.Part
Part.mem_bind_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {b : β}, b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_apply_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (x : E), U.starProjection x ∈ U
-- Mathlib.Data.ZMod.Units
ZMod.coe_int_val_inv_mul : ∀ {n : ℕ} [NeZero n] {m : ℤ}, IsCoprime m ↑n → ↑(↑m)⁻¹.val * ↑m = 1
-- Mathlib.Topology.Order
NontrivialTopology.ne_top : ∀ (α : Type u_2) {inst : TopologicalSpace α} [self : NontrivialTopology α], inst ≠ ⊤