mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_1 ()
-- Aesop.Frontend.RuleExpr
Lean.Parser.Category.Aesop.builder_option : Lean.Parser.Category
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.bsize.match_1.splitter : (motive : Substring.Raw → Sort u_1) →
  (x : Substring.Raw) →
    ((str : String) → (b e : String.Pos.Raw) → motive { str := str, startPos := b, stopPos := e }) → motive x
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State : Type
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- Returns the `n`-th value emitted by `it`, or `none` if `it` terminates earlier.

For monadic iterators, the monadic effects of this operation may differ from manually iterating
to the `n`-th value because `atIdx?` can take shortcuts. By the signature, the return value
is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.

This function is only available for iterators that explicitly support it by implementing
the `IteratorAccess` typeclass.
 -/
Std.IterM.atIdx? : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] → [Std.IteratorAccess α m] → [Monad m] → Std.IterM m β → ℕ → m (Option β)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.sup : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l l' : Filter α}, f' =Θ[l] g' → f' =Θ[l'] g' → f' =Θ[l ⊔ l'] g'
-- Mathlib.RingTheory.Ideal.Maps
/-- Correspondence theorem  -/
Ideal.relIsoOfSurjective : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Ring R] →
        [inst_1 : Ring S] →
          [inst_2 : FunLike F R S] →
            [inst_3 : RingHomClass F R S] → (f : F) → Function.Surjective ⇑f → Ideal S ≃o { p // Ideal.comap f ⊥ ≤ p }
-- Init.PropLemmas
Decidable.predToBool : {α : Sort u_1} → (p : α → Prop) → [DecidablePred p] → CoeDep (α → Prop) p (α → Bool)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.span_ef : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H),
  LieSubalgebra.lieSpan R L (Set.range self.e ∪ Set.range self.f) = ⊤
-- Mathlib.Topology.Convenient.Category
/-- Constructor for morphisms in `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.homMk : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y Z : ContinuousGeneratedByCat X} → (f : ↑Y → ↑Z) → Topology.ContinuousGeneratedBy X f → (Y ⟶ Z)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.card : ∀ {D : Type u_1} {Q : Type u_2} [Finite Q], Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q
-- Mathlib.Algebra.Symmetrized
SymAlg.instMulOfAddOfInvertibleOfNat : {α : Type u_1} → [Add α] → [inst : Mul α] → [inst_1 : One α] → [inst_2 : OfNat α 2] → [Invertible 2] → Mul αˢʸᵐ
-- Mathlib.Computability.Primrec.Basic
/-- `PrimrecPred p` means `p : α → Prop` is a
primitive recursive predicate, which is to say that
`decide ∘ p : α → Bool` is primitive recursive.  -/
PrimrecPred : {α : Type u_1} → [Primcodable α] → (α → Prop) → Prop
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Returns true if the given predicate is true for all items in the RBMap.  -/
RBTree.RBMap.all : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → (α → β → Bool) → Bool
-- Init.Grind.AC
Lean.Grind.AC.superpose_cert : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq →
    Lean.Grind.AC.Seq →
      Lean.Grind.AC.Seq →
        Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Order.Disjoint
Disjoint.le_of_codisjoint : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b c : α}, Disjoint a b → Codisjoint b c → a ≤ c
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Graph.DFSState.mk.sizeOf_spec : ∀ (visited : Std.HashSet ℕ), sizeOf { visited := visited } = 1 + sizeOf visited
-- Init.Data.BitVec.Lemmas
BitVec.and_self : ∀ {w : ℕ} {x : BitVec w}, x &&& x = x
-- Lean.Parser.Basic
Lean.Parser.nodeWithAntiquot : String → Lean.SyntaxNodeKind → Lean.Parser.Parser → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Data.Fintype.Pi
SetLike.instMembership.hcongr_3 : ∀ (A A' : Type u_1),
  A = A' →
    ∀ (B B' : Type u_2),
      B = B' → ∀ (i : SetLike A B) (i' : SetLike A' B'), i ≍ i' → SetLike.instMembership ≍ SetLike.instMembership
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.posRootForm_rootFormIn_posDef : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [IsStrictOrderedRing S] [IsDomain R]
  [inst_10 : Algebra S R] [inst_11 : FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [inst_13 : Module S M]
  [inst_14 : IsScalarTower S R M] [inst_15 : Module S N] [IsScalarTower S R N],
  (LinearMap.BilinMap.toQuadraticMap (P.RootFormIn S)).PosDef
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearIndependent.cardinal_le_rank' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s : Set M}, (LinearIndependent R fun (x : ↑s) => ↑x) → Cardinal.mk ↑s ≤ Module.rank R M
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Two left invariant measures give the same mass to level sets of continuous compactly supported
functions, up to the scalar `haarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure.  -/
MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant] {f : G → ℝ},
  Continuous f → HasCompactSupport f → μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansionFormalMultilinearSeries_radius : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F),
  0 < h →
    Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff ⇑f →
        UpperHalfPlane.IsBoundedAtImInfty ⇑f → 1 ≤ (UpperHalfPlane.qExpansionFormalMultilinearSeries h f).radius
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `S` contains `0` then the localization at `S` is trivial.  -/
LocalizedModule.subsingleton : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  0 ∈ S → Subsingleton (LocalizedModule S M)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- The core logic of guessing the lexicographic order
Given a matrix that for each call and measure indicates whether that measure is
decreasing, equal, less-or-equal or unknown, It finds a sequence of measures
that is lexicographically decreasing.

The matrix is implemented here as an array of monadic query methods only so that
we can fill is lazily. Morally, this is a pure function
 -/
Lean.Elab.WF.GuessLex.solve : {m : Type → Type} →
  {α : Type} → [Monad m] → Array α → Array (α → m Lean.Elab.WF.GuessLex.GuessLexRel) → m (Option (Array α))
-- Mathlib.AlgebraicTopology.SimplicialSet.Presentable
SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex : ∀ (n : SimplexCategory), CategoryTheory.IsFinitelyPresentable (SSet.stdSimplex.obj n)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (↑(m.insertMany l)).getKey! k' = k
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_shiftRight_eq_shiftRight_of_le : ∀ {b c : ℕ}, b ≤ c → ∀ (a : ℤ), a <<< b >>> c = a >>> (c - b)
-- Lean.Meta.Tactic.NormCast
/-- `Label` is a type used to classify `norm_cast` lemmas.
* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
 -/
Lean.Meta.NormCast.Label : Type
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.algebraMap_eval_S : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R) (n : ℤ),
  (algebraMap R R') (Polynomial.eval x (Polynomial.Chebyshev.S R n)) =
    Polynomial.eval ((algebraMap R R') x) (Polynomial.Chebyshev.S R' n)
-- Lean.Elab.Term.TermElabM
/-- Backtrackable state for the `TermElabM` monad.
 -/
Lean.Elab.Term.SavedState : Type
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A submodule has dimension at most `1` if and only if there is a
single vector in the submodule such that the submodule is contained in
its span.  -/
rank_submodule_le_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  (s : Submodule K V) [Module.Free K ↥s], Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀
-- Lean.Meta.Sym.Eta
/-- If `e` is of the form `(fun x₁ ... xₙ => f x₁ ... xₙ)` and `f` does not contain `x₁`, ..., `xₙ`,
then returns `f`. Otherwise, returns `e`.

Returns the original expression when not reducible to enable pointer equality checks.
 -/
Lean.Meta.Sym.etaReduce : Lean.Expr → Lean.Expr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filterMap.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a)),
  Std.DHashMap.Internal.AssocList.filterMap f =
    Std.DHashMap.Internal.AssocList.filterMap.go✝ f Std.DHashMap.Internal.AssocList.nil
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_inter_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.Order.Atoms
Set.isAtom_iff : ∀ {α : Type u_2} {s : Set α}, IsAtom s ↔ ∃ x, s = {x}
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.top : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite R ↥⊤
-- Mathlib.Data.ENat.Basic
ENat.add_lt_top : ∀ {a b : ℕ∞}, a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₁_1 : CategoryTheory.MorphismProperty C)
  (e_W₁ : W₁ = W₁_1) (W₂ W₂_1 : CategoryTheory.MorphismProperty C) (e_W₂ : W₂ = W₂_1) [inst_1 : W₁.IsMultiplicative]
  [inst_2 : W₂.IsMultiplicative] (α : Type u_2) [inst_3 : LinearOrder α] [inst_4 : OrderBot α] [inst_5 : SuccOrder α]
  [inst_6 : WellFoundedLT α], HomotopicalAlgebra.ReedyStructure W₁ W₂ α = HomotopicalAlgebra.ReedyStructure W₁_1 W₂_1 α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_entryAtIdx? : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {i : ℕ} [inst : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx! t i = (Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t i).get!
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.essImage_tilde : ∀ {R : CommRingCat},
  (AlgebraicGeometry.tilde.functor R).essImage = SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_sum_range_succ : ∀ {Ω : Type u_1} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : AddCommMonoid β] [MeasurableAdd₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ℕ), Measurable (f i)) → ∀ (n : ℕ), ProbabilityTheory.CondIndepFun m' hm' (∑ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.Data.Sym.Sym2
Sym2.instDecidableRel' : {α : Type u_1} → [DecidableEq α] → DecidableRel HasEquiv.Equiv
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.toCoalgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A →ₐc[R] B) → A →ₗc[R] B
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The bundled commutative monoid giving the filtered colimit of a diagram.  -/
CommMonCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommMonCat → CommMonCat
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- A doubly stochastic matrix multiplied with the all-ones column vector is 1.  -/
mulVec_one_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R}, M ∈ doublyStochastic R n → M.mulVec 1 = 1
-- Init.Util
/-- `withPtrEq` for `DecidableEq`  -/
withPtrEqDecEq : {α : Type u} → (a b : α) → (Unit → Decidable (a = b)) → Decidable (a = b)
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
/-- The right homology data which allows to show that `K.πTruncGE e`
induces an isomorphism in homology in degrees `j'` such that `e.f j = j'` for some `j`.  -/
HomologicalComplex.truncGE.rightHomologyMapData : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                        {i j k : ι} →
                          {j' : ι'} →
                            (hj' : e.f j = j') →
                              (hi : c.prev j = i) →
                                (hk : c.next j = k) →
                                  (hj : e.BoundaryGE j) →
                                    CategoryTheory.ShortComplex.RightHomologyMapData
                                      ((HomologicalComplex.shortComplexFunctor C c' j').map (K.πTruncGE e))
                                      (CategoryTheory.ShortComplex.RightHomologyData.canonical (K.sc j'))
                                      (HomologicalComplex.extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
                                        (HomologicalComplex.truncGE'.homologyData K e i j k hk hj' hj).right)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_eq_top_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra K E] [inst_5 : Algebra K F] [inst_6 : IsScalarTower K F E]
  {L : IntermediateField F E}, IntermediateField.restrictScalars K L = ⊤ ↔ L = ⊤
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorIso_hom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e : X₁ ≅ X₂)
  (e' : Y₁ ≅ Y₂) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂] (i : I),
  (CategoryTheory.GradedObject.Monoidal.tensorIso e e').hom i =
    CategoryTheory.GradedObject.Monoidal.tensorHom e.hom e'.hom i
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : β → α}
  {a b : α} {x : Filter β} [hx : x.NeBot], Filter.Tendsto f x (nhds a) → (∀ᶠ (c : β) in x, f c ≤ b) → a ≤ b
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMapClass.instCoeTCCocompactMap : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : FunLike F α β] → [CocompactMapClass F α β] → CoeTC F (CocompactMap α β)
-- Mathlib.Tactic.NormNum.NatFib
/-- Given the natural number literal `ex`, returns `Nat.fib ex` as a natural number literal
and an equality proof. Panics if `ex` isn't a natural number literal.  -/
Mathlib.Meta.NormNum.proveNatFib : (en' : Q(ℕ)) → (em : Q(ℕ)) × Q(Nat.fib «$en'» = «$em»)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.comap_pNilradical : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ)
  [IsPRadical i p], Ideal.comap i (pNilradical L p) = pNilradical K p
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.smul_odd : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [inst_1 : Monoid β]
  [inst_2 : AddGroup γ] [inst_3 : DistribMulAction β γ], Function.Even f → Function.Odd g → Function.Odd (f • g)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The bijection `(X ⟶ Y) ≃ (𝟙_ V ⟶ (X ⟶[V] Y))` given by a
`EnrichedOrdinaryCategory` instance.  -/
CategoryTheory.eHomEquiv : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] →
            {X Y : C} → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] Y)
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_filter_ne_zero : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} (z : ι → E) [inst_3 : (i : ι) → Decidable (w i ≠ 0)],
  {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat)
  (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) (y : ↑(Y.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx))
        y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx))
      ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op U))) y)
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.smul_eq_eval : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} {R₀ : Type u_4} [inst : AddCommMonoid M] [inst_1 : Semiring R]
  [inst_2 : Module R M] [inst_3 : Semiring R₀] [inst_4 : Module R₀ M] [inst_5 : Semiring S] [inst_6 : Module S M]
  {l : Mathlib.Tactic.Module.NF R M} {l₀ : Mathlib.Tactic.Module.NF R₀ M} {s : S} {r : R} {x : M},
  x = l₀.eval → l.eval = l₀.eval → r • x = s • x → s • x = (r • l).eval
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- Given a morphism `f : X ⟶ Y` of simplicial set which sends a `0`-simplex `x` to `y`,
this is the pointed morphism `(X, x) ⟶ (Y, y)`.  -/
SSet.RelativeMorphism.ofSimplex₀ : {X Y : SSet} →
  (f : X ⟶ Y) →
    (x : X.obj (Opposite.op { len := 0 })) →
      (y : Y.obj (Opposite.op { len := 0 })) →
        (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x = y →
          SSet.RelativeMorphism (SSet.Subcomplex.ofSimplex x) (SSet.Subcomplex.ofSimplex y) (SSet.const ⟨y, ⋯⟩)
-- Batteries.Control.AlternativeMonad
instAlternativeMonadMetaM : AlternativeMonad Lean.MetaM
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.comm : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (self : M.Hom N) (g : G),
  CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.factor_eval_eq_evalₐ : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {n : ℕ} (x : AdicCompletion I R) (h : I ^ n • ⊤ ≤ I ^ n),
  (Submodule.factor h) ((AdicCompletion.eval I R n) x) = (AdicCompletion.evalₐ I n) x
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.whiskerLeft : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F₁ : CategoryTheory.Functor C D} (G G' : CategoryTheory.Functor D E) (τ'' : G ⟶ G') (A : Type u_5)
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift C A] [inst_5 : CategoryTheory.HasShift D A]
  [inst_6 : CategoryTheory.HasShift E A] [inst_7 : F₁.CommShift A] [inst_8 : G.CommShift A] [inst_9 : G'.CommShift A]
  [CategoryTheory.NatTrans.CommShift τ'' A], CategoryTheory.NatTrans.CommShift (F₁.whiskerLeft τ'') A
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_eq : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f : F), ↑(RingHom.ker f) = ⇑f ⁻¹' {0}
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.sum_obj_obj : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀}
  {D : J → Type u₁} [inst_1 : (j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j)
  (s : I ⊕ J),
  ((CategoryTheory.Pi.sum C).obj X).obj Y s =
    match s with
    | Sum.inl i => X i
    | Sum.inr j => Y j
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.sInf_adj_of_nonempty : ∀ {V : Type u} {a b : V} {s : Set (SimpleGraph V)}, s.Nonempty → ((sInf s).Adj a b ↔ ∀ G ∈ s, G.Adj a b)
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.instIsScalarTowerAtPrimeFractionRing : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] (p : Ideal R) [inst_2 : p.IsPrime],
  IsScalarTower R (Localization.AtPrime p) (FractionRing R)