mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_fun_mul_natCast : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.lpNorm (fun x => f x * ↑n) p μ = MeasureTheory.lpNorm f p μ * ↑n
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indToCoindAux_self : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g : G) (a : ↑A),
  (A.indToCoindAux g) a g = a
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis : ∀ {R : Type u_4} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι],
  B.Nondegenerate →
    ∀ (b : Module.Basis ι S M),
      B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections are uniformly bounded.  -/
SchauderBasis.exists_norm_proj_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X], ∃ C, ∀ (n : ℕ), ‖b.proj n‖ ≤ C
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Evaluation as a `MonoidHom`  -/
LocallyConstant.evalMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : MulOneClass Y] → X → LocallyConstant X Y →* Y
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.instPreadditivePullbackShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.PullbackShift C φ)
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- The root of an arborescence.  -/
Quiver.root : (V : Type u) → [inst : Quiver V] → [Quiver.Arborescence V] → V
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSetIso_apply : ∀ (o : Ordinal.{u_1}), Ordinal.toZFSetIso o = ⟨o.toZFSet, ⋯⟩
-- Mathlib.NumberTheory.FrobeniusNumber
/-- The **Chicken McNugget theorem** stating that the Frobenius number
of positive numbers `m` and `n` is `m * n - m - n`.  -/
frobeniusNumber_pair : ∀ {m n : ℕ}, m.Coprime n → 1 < m → 1 < n → FrobeniusNumber (m * n - m - n) {m, n}
-- Mathlib.Tactic.Explode.Datatypes
/-- The row in the Fitch table.  -/
Mathlib.Explode.Entry : Type
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.exists : ∀ {σs : List (Type u)} {α : Sort u_1} {Q : Std.Do.SPred σs} {ψ : α → Std.Do.SPred σs} {T : Std.Do.SPred σs},
  (∀ (a : α), Q ∧ ψ a ⊢ₛ T) → (Q ∧ ∃ a, ψ a) ⊢ₛ T
-- Mathlib.Data.Seq.Computation
/-- `Promises s a`, or `s ~> a`, asserts that although the computation `s`
may not terminate, if it does, then the result is `a`.  -/
Computation.Promises : {α : Type u} → Computation α → α → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.cast.eq_1 : ∀ {α β : Type u_6} [i₁ : MeasurableSpace α] [i₂ : MeasurableSpace β] (h : α = β) (hi : i₁ ≍ i₂),
  MeasurableEquiv.cast h hi = { toEquiv := Equiv.cast h, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Order.Interval.Set.Fin
Fin.image_rev_fun : ∀ {n : ℕ}, Set.image Fin.rev = Set.preimage Fin.rev
-- Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit
/-- The functor `X.N ⥤ SSet` which sends `x : X.N` to `Δ[x.dim]`.  -/
SSet.functorN' : (X : SSet) → [X.Nonsingular] → CategoryTheory.Functor X.N SSet
-- Mathlib.Data.Finset.Image
/-- If all elements of a `Finset` satisfy the predicate `p`,
`s.subtype p` converts back to `s` with `Embedding.subtype`.  -/
Finset.subtype_map_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α},
  (∀ x ∈ s, p x) → Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = s
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.IsNatPowT.bit1 : ∀ {a b c : ℕ}, Mathlib.Meta.NormNum.IsNatPowT (a.pow b = c) a (2 * b + 1) (c.mul (c.mul a))
-- Mathlib.Topology.UniformSpace.Cauchy
/-- Given a Cauchy filter `f` and a sequence `U` of entourages, `set_seq` provides
an antitone sequence of sets `s n ∈ f` such that `s n ×ˢ s n ⊆ U`.  -/
SequentiallyComplete.setSeq : {α : Type u} →
  [uniformSpace : UniformSpace α] →
    {f : Filter α} → Cauchy f → {U : ℕ → SetRel α α} → (∀ (n : ℕ), U n ∈ uniformity α) → ℕ → Set α
-- Mathlib.Algebra.Group.Action.Pi
Function.hasSMul.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : Type u_7} [inst : SMul M α], Function.hasSMul = Pi.instSMul
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.terminalNesting : Lean.VersoModuleDocs.Snippet → Option ℕ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit F G).inv
      (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j) =
    G.whiskerLeft (CategoryTheory.Limits.limit.π F j)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.step.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) →
          (x : Turing.TM2.Cfg Γ Λ σ) →
            ((var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk }) →
              ((l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }) → motive x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (↑m).keys.contains k = m.contains k
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.findSomeRevM?.find.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (val : β) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Aesop.Options.Public
Aesop.Strategy.depthFirst.sizeOf_spec : sizeOf Aesop.Strategy.depthFirst = 1
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.blockTriangular_transpose_iff : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} [inst : LT α] [inst_1 : Zero R] {b : m → αᵒᵈ},
  M.transpose.BlockTriangular b ↔ M.BlockTriangular (⇑OrderDual.ofDual ∘ b)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_ofAdd_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  a ≤ ↑(Multiplicative.ofAdd b) ↔ Multiplicative.toAdd (WithZero.unzero ha) ≤ b
-- Init.Data.Iterators.Basic
/-- `Rel` is well-founded.  -/
Std.Iterators.ProductivenessRelation.wf : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (self : Std.Iterators.ProductivenessRelation α m), WellFounded self.Rel
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
Prod.instMeasurableSpace.eq_1 : ∀ {α : Type u_6} {β : Type u_7} [m₁ : MeasurableSpace α] [m₂ : MeasurableSpace β], Prod.instMeasurableSpace = m₁.prod m₂
-- Lean.DocString.Syntax
Lean.Doc.Syntax.block.quot : Lean.ParserDescr
-- Mathlib.Topology.Order.LiminfLimsup
OrderBot.to_BoundedGENhdsClass : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [OrderBot α], BoundedGENhdsClass α
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_mul_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), a / b * b = a
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.logEmbeddingQuot_injective : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Function.Injective ⇑(NumberField.Units.logEmbeddingQuot K)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_id : ∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
  [OpensMeasurableSpace α] [SecondCountableTopology α], MeasureTheory.StronglyMeasurable id
-- Mathlib.Data.Seq.Parallel
Computation.terminates_parallel.aux : ∀ {α : Type u} {l : List (Computation α)} {S : Stream'.WSeq (Computation α)} {c : Computation α},
  c ∈ l → c.Terminates → (Computation.corec Computation.parallel.aux1✝ (l, S)).Terminates
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.injOn_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M) (k : ℕ∞),
  Set.InjOn (fun x => (f.genEigenspace x) k) {μ | (f.genEigenspace μ) k ≠ ⊥}
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.mk.inj : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} {obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U)}
  {map :
    ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
      obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj V)}
  {obj_1 : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U)}
  {map_1 :
    ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
      obj_1 U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj_1 V)},
  { obj := obj, map := map } = { obj := obj_1, map := map_1 } → obj = obj_1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 5`.  -/
CategoryTheory.ComposableArrows.homMk₅ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {f g : CategoryTheory.ComposableArrows C 5} →
      (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) →
        (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝) →
          (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) →
            (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝) →
              (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) →
                (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝) →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝) app₁ =
                        CategoryTheory.CategoryStruct.comp app₀
                          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
                      _auto_439✝ →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
                          CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
                        _auto_441✝ →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
                            CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
                          _auto_443✝ →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
                              CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
                            _auto_445✝ →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
                                CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
                              _auto_447✝ →
                            (f ⟶ g)
-- Init.Data.Fin.Lemmas
Fin.mk_le_of_le_val : ∀ {n : ℕ} {b : Fin n} {a : ℕ} (h : a ≤ ↑b), ⟨a, ⋯⟩ ≤ b
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coeFnAddMonoidHom_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (v : Π₀ (i : ι), β i),
  DFinsupp.coeFnAddMonoidHom v = ⇑v
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfSurjective_symm_apply : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f) (x : R),
  (RingHom.quotientKerEquivOfSurjective hf).symm (f x) = (Ideal.Quotient.mk (RingHom.ker f)) x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.beta.injEq : ∀ (e e_1 : Lean.Expr), (Lean.Meta.Grind.SplitSource.beta e = Lean.Meta.Grind.SplitSource.beta e_1) = (e = e_1)
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.isLocalization : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [h : Algebra.EssFiniteType R S], IsLocalization (Algebra.EssFiniteType.submonoid R S) S
-- Mathlib.Data.Rat.Cast.Order
Rat.natCast_lt_cast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ}, ↑m < ↑n ↔ ↑m < n
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getElem!_filter` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getElem!_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  (Std.ExtTreeMap.filter f t)[k]! = (Option.filter (f k) t[k]?).get!
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_coeff : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.eq_coeff_cert p p' k = true →
    Int.Internal.Linear.Poly.denote' ctx p ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p' ≠ 0
-- Mathlib.Order.Ideal
/-- `idealOfCofinals p 𝒟` is `𝒟`-generic.  -/
Order.cofinal_meets_idealOfCofinals : ∀ {P : Type u_1} [inst : Preorder P] (p : P) {ι : Type u_2} [inst_1 : Encodable ι] (𝒟 : ι → Order.Cofinal P) (i : ι),
  ∃ x ∈ 𝒟 i, x ∈ Order.idealOfCofinals p 𝒟
-- Mathlib.Topology.GDelta.MetrizableSpace
/-- **Alias** of `IsGδ.setOfPred_continuousAt`. -/
IsGδ.setOf_continuousAt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.PseudoMetrizableSpace Y] (f : X → Y), IsGδ {x | ContinuousAt f x}
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_id : ∀ {R : RingCat}, RingCat.Hom.hom (CategoryTheory.CategoryStruct.id R) = RingHom.id ↑R
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.left_inv : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (x : TensorProduct R A (Polynomial R)), PolyEquivTensor.invFun R A ((PolyEquivTensor.toFunAlgHom R A) x) = x
-- Mathlib.Algebra.Ring.MinimalAxioms
/-- Define a `CommRing` structure on a Type by proving a minimized set of axioms.
Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub`
See note [reducible non-instances].  -/
CommRing.ofMinimalAxioms : {R : Type u} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      [inst_2 : Neg R] →
        [inst_3 : Zero R] →
          [inst_4 : One R] →
            (∀ (a b c : R), a + b + c = a + (b + c)) →
              (∀ (a : R), 0 + a = a) →
                (∀ (a : R), -a + a = 0) →
                  (∀ (a b c : R), a * b * c = a * (b * c)) →
                    (∀ (a b : R), a * b = b * a) →
                      (∀ (a : R), 1 * a = a) → (∀ (a b c : R), a * (b + c) = a * b + a * c) → CommRing R
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.toGL_injective : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Function.Injective ⇑Matrix.SpecialLinearGroup.toGL
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β}
  (f : β → α) {s : Set γ}, Set.InjOn g s → ∑' (x : ↑(g '' s)), f ↑x = ∑' (x : ↑s), f (g ↑x)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mk.injEq : ∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (toProd : (A →L[𝕜] A) × (A →L[𝕜] A)) (central : ∀ (x y : A), toProd.2 x * y = x * toProd.1 y)
  (toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A)) (central_1 : ∀ (x y : A), toProd_1.2 x * y = x * toProd_1.1 y),
  ({ toProd := toProd, central := central } = { toProd := toProd_1, central := central_1 }) = (toProd = toProd_1)
-- Mathlib.Order.Antisymmetrization
lt_of_lt_of_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], a < b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a < c
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_one_sub : ∀ {R : Type u} [inst : CommRing R] (e : ↑{e | IsIdempotentElem e}),
  PrimeSpectrum.isIdempotentElemEquivClopens ⟨1 - ↑e, ⋯⟩ = (PrimeSpectrum.isIdempotentElemEquivClopens e)ᶜ
-- Std.Async.IO
Std.Async.IO.AsyncStream.mk : {α : Type} → {β : outParam Type} → (α → Std.Async.Selector β) → (α → IO Unit) → Std.Async.IO.AsyncStream α β
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : Std.DTreeMap.Internal.Impl α β}, l.minEntry? = l.minEntry?ₘ
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Summand in the series for the Jacobi theta function.  -/
jacobiTheta₂_term : ℤ → ℂ → ℂ → ℂ
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coe_congrLinearEquiv : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} {N : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (N i)]
  [inst_2 : (i : ι) → Module R (N i)] {P : ι → Type u_4} [inst_3 : (i : ι) → AddCommMonoid (P i)]
  [inst_4 : (i : ι) → Module R (P i)] (u : (i : ι) → N i ≃ₗ[R] P i),
  ⇑(DirectSum.congrLinearEquiv u) = ⇑(DirectSum.lmap fun i => ↑(u i))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval_πs_image' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂),
  (∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁) →
    Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) ''
        {m | m < l} =
      ⇑(Profinite.NobelingProof.πs' C h) ''
        Profinite.NobelingProof.Products.eval
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ''
          {m | m < l}
-- Mathlib.Data.Nat.Squarefree
Nat.divisors_filter_squarefree_of_squarefree : ∀ {n : ℕ}, Squarefree n → {d ∈ n.divisors | Squarefree d} = n.divisors
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso_ancestralRel_iff : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  (x y : ↑P.II),
  (P.ofIso e hA).AncestralRel ⟨(SSet.Subcomplex.N.orderIsoOfIso e hA).symm ↑x, ⋯⟩
      ⟨(SSet.Subcomplex.N.orderIsoOfIso e hA).symm ↑y, ⋯⟩ ↔
    P.AncestralRel x y
-- Lean.Parser.Syntax
Lean.Parser.Command.elabTail.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.SameCycle.exists_pow_eq : ∀ {α : Type u_2} {x y : α} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  f.SameCycle x y → ∃ i, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- `HasSheafify` means that the inclusion functor from sheaves to presheaves admits a left exact
left adjoint (sheafification).

Given a functor, preserving finite limits, `F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A` and an adjunction
`adj : F ⊣ sheafToPresheaf J A`, use `HasSheafify.mk'` to construct a `HasSheafify` instance.
 -/
CategoryTheory.HasSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C → (A : Type u₂) → [CategoryTheory.Category.{v₂, u₂} A] → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The composition of cochains.  -/
CochainComplex.HomComplex.Cochain.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G K : CochainComplex C ℤ} →
        {n₁ n₂ n₁₂ : ℤ} →
          CochainComplex.HomComplex.Cochain F G n₁ →
            CochainComplex.HomComplex.Cochain G K n₂ → n₁ + n₂ = n₁₂ → CochainComplex.HomComplex.Cochain F K n₁₂
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.henstock_le_riemann : BoxIntegral.IntegrationParams.Henstock ≤ BoxIntegral.IntegrationParams.Riemann
-- Mathlib.AlgebraicGeometry.Noetherian
/-- A Noetherian scheme has a finite number of irreducible components.  -/
AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X], (irreducibleComponents ↥X).Finite
-- Mathlib.Order.Compare
cmp_swap : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] (a b : α), (cmp a b).swap = cmp b a
-- Mathlib.Computability.Encoding
/-- A "proxy type" equivalent to `Computability.Γ'` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `Computability.Γ'.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
Computability.Γ'.proxyType : Type
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist`.

---

The minimal edistance of a point to a set  -/
EMetric.infEdist : {α : Type u} → [PseudoEMetricSpace α] → α → Set α → ENNReal
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalGroup.toContinuousMul : ∀ {G : Type u_4} {inst : TopologicalSpace G} {inst_1 : Group G} [self : IsTopologicalGroup G], ContinuousMul G
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E7 : ADEInequality.Admissible ADEInequality.E7
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.sdiff : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsUpperSet s → (∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) → IsUpperSet (s \ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.eqToHom_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {j j' : J} (w : j = j') {Z : C} (h : ∐ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f j') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f j) h