mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.minKey?.isSome = true
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.id_apply : ∀ (X : GrpCat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `r` is less than the Hausdorff dimension of a set `s` in an (extended) metric space with
second countable topology, then there exists a point `x ∈ s` such that every neighborhood
`t` of `x` within `s` has Hausdorff dimension greater than `r`.  -/
exists_mem_nhdsWithin_lt_dimH_of_lt_dimH : ∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] {s : Set X} {r : ENNReal},
  r < dimH s → ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, r < dimH t
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_compl_mul_self : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f : α → M), sᶜ.mulIndicator f * s.mulIndicator f = f
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map_fun : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F],
  ProbabilityTheory.HasGaussianLaw X P → ∀ (L : E →L[ℝ] F), ProbabilityTheory.HasGaussianLaw (fun ω => L (X ω)) P
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.isoMk_inv_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f.f],
  (CategoryTheory.Center.isoMk f).inv.f = CategoryTheory.inv f.f
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.map_map : ∀ {S T : SSet.Truncated 2} (f : S ⟶ T) {X Y : SSet.OneTruncation₂ S} (e : X ⟶ Y),
  (SSet.OneTruncation₂.map f).map e = SSet.Truncated.Edge.map e f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
_private.Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections.0.TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj.match_1.eq_1 : ∀ {ι : Type u_1} (motive : CategoryTheory.Pairwise ι → Sort u_2) (i : ι)
  (h_1 : (i : ι) → motive (CategoryTheory.Pairwise.single i))
  (h_2 : (i j : ι) → motive (CategoryTheory.Pairwise.pair i j)),
  (match CategoryTheory.Pairwise.single i with
    | CategoryTheory.Pairwise.single i => h_1 i
    | CategoryTheory.Pairwise.pair i j => h_2 i j) =
    h_1 i
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.mk.injEq : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  (toRelations : Module.Relations A) (toSolution : toRelations.Solution M)
  (toIsPresentation : toSolution.IsPresentation) (toRelations_1 : Module.Relations A)
  (toSolution_1 : toRelations_1.Solution M) (toIsPresentation_1 : toSolution_1.IsPresentation),
  ({ toRelations := toRelations, toSolution := toSolution, toIsPresentation := toIsPresentation } =
      { toRelations := toRelations_1, toSolution := toSolution_1, toIsPresentation := toIsPresentation_1 }) =
    (toRelations = toRelations_1 ∧ toSolution ≍ toSolution_1)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_inf : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (q q' : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂), Submodule.comap f (q ⊓ q') = Submodule.comap f q ⊓ Submodule.comap f q'
-- Init.Control.EState
/-- Converts a state monad action into a state monad action with exceptions.

The resulting action does not throw an exception.
 -/
EStateM.fromStateM : {ε σ α : Type} → StateM σ α → EStateM ε σ α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.isOpen' : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (self : OpenAddSubgroup G), IsOpen (↑self).carrier
-- Aesop.Index.RulePattern
/-- A map from rule names to rule pattern substitutions. When run on a goal,
the rule pattern index returns such a map.  -/
Aesop.RulePatternSubstMap : Type
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.symPrios : Lean.Meta.Grind.Params → Lean.Meta.Grind.SymbolPriorities
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin_val : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (s : Set K) [inst_4 : Finite ↑s],
  (FiniteGaloisIntermediateField.adjoin k s).toIntermediateField =
    IntermediateField.normalClosure k (↥(IntermediateField.adjoin k s)) K
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Roc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Roc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Algebra.Equiv
/-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence.  -/
AlgEquiv.toLinearEquiv : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ ≃ₗ[R] A₂
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- `LinearIndepOn.extend` adds vectors to a linear independent set `s ⊆ t` until it spans
all elements of `t`.  -/
LinearIndepOn.extend : {ι : Type u'} →
  {K : Type u_3} →
    {V : Type u} →
      [inst : DivisionRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] → {v : ι → V} → {s t : Set ι} → LinearIndepOn K v s → s ⊆ t → Set ι
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterWithPostcondition.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := false })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := false }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_1 h'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldl.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (a : α) → β a → δ) (init : δ)
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.foldl f init t =
    (Std.DTreeMap.Internal.Impl.foldlM (fun x1 x2 x3 => pure (f x1 x2 x3)) init t).run
-- Mathlib.CategoryTheory.Sites.Sieves
/-- When `hg : Sieve.ofArrows Y f g`, this is a choice of `i` such that `g`
factors through `f i`.  -/
CategoryTheory.Sieve.ofArrows.i : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {I : Type u_1} →
      {X : C} →
        {Y : I → C} → {f : (i : I) → Y i ⟶ X} → {W : C} → {g : W ⟶ X} → (CategoryTheory.Sieve.ofArrows Y f).arrows g → I
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_mul : ∀ {R : Type u_1} {a b : R} [inst : Mul R] [inst_1 : Add R] (z w : QuadraticAlgebra R a b),
  (z * w).re = z.re * w.re + a * z.im * w.im
-- Mathlib.Logic.Function.Defs
Function.dcomp_apply : ∀ {ι : Sort u_3} {β : ι → Sort u_1} {φ : {i : ι} → β i → Sort u_2} (f : {i : ι} → (y : β i) → φ y) (g : (i : ι) → β i)
  (i : ι), (f ∘' g) i = f (g i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_pt : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  (CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom V F₁ F₂).pt =
    CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size_balanceL : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l' l.size ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r.size r' ∧ Ordnode.BalancedSz l.size r') →
            (l.balanceL x r).size = l.size + r.size + 1
-- Mathlib.Algebra.Group.Action.Pi
Function.update_smul : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [inst_1 : DecidableEq ι] (c : M)
  (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i), Function.update (c • f₁) i (c • x₁) = c • Function.update f₁ i x₁
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.maxDegreeOf : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Var → ℕ
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- Remainder of polynomial division. See `Polynomial.modByMonic` for more details.  -/
Polynomial.mod : {R : Type u} → [inst : Field R] → Polynomial R → Polynomial R → Polynomial R
-- Init.Core
flip.eq_1 : ∀ {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) (b : β) (a : α), flip f b a = f a b
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.LipschitzWith.integrable_comp_iff_of_antilipschitz : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {K K' : NNReal} {f : α → β} {g : β → γ},
  LipschitzWith K g →
    AntilipschitzWith K' g → g 0 = 0 → (MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.Order.SuccPred.Basic
Order.le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] (a : α), a ≤ Order.succ a
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.prev.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x : List α) → (x_1 : α) → x_1 ∈ x → Sort u_2) (y x : α) (x_1 : x ∈ [y])
  (h_1 : (x : α) → (h : x ∈ []) → motive [] x h) (h_2 : (y x : α) → (x_2 : x ∈ [y]) → motive [y] x x_2)
  (h_3 : (y z : α) → (xs : List α) → (x : α) → (h : x ∈ y :: z :: xs) → motive (y :: z :: xs) x h),
  (match [y], x, x_1 with
    | [], x, h => h_1 x h
    | [y], x, x_2 => h_2 y x x_2
    | y :: z :: xs, x, h => h_3 y z xs x h) =
    h_2 y x x_1
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findWithLeadingToken? : (Option Lean.Syntax → Lean.Syntax → Bool) → Lean.Syntax → Option Lean.Syntax
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minEntry? (Std.Internal.List.insertEntryIfNew k v l)).isSome = true
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polarSym2_map_smul : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (g : ι → M) (l : ι → R)
  (p : Sym2 ι),
  QuadraticMap.polarSym2 (⇑Q) (Sym2.map (l • g) p) = (Sym2.map l p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map g p)
-- Mathlib.Order.BourbakiWitt
NonemptyChain.mk : {α : Type u_4} →
  [inst : LE α] → (carrier : Set α) → carrier.Nonempty → IsChain (fun x1 x2 => x1 ≤ x2) carrier → NonemptyChain α
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.elabGrindSuggestions : Lean.Meta.Grind.Params → optParam (Array Lean.LibrarySuggestions.Suggestion) #[] → Lean.MetaM Lean.Meta.Grind.Params
-- Mathlib.CategoryTheory.Opposites
/-- Whenever possible, it is advisable to use the isomorphism `rightOpLeftOpIso`
instead of this equality of functors.  -/
CategoryTheory.Functor.rightOp_leftOp_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D), F.rightOp.leftOp = F
-- Mathlib.Algebra.Regular.Basic
IsAddLeftRegular.nsmul_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} {n : ℕ}, 0 < n → (IsAddLeftRegular (n • a) ↔ IsAddLeftRegular a)
-- Mathlib.Computability.ContextFreeGrammar
/-- Given a context-free grammar `g` and a string `s`
`g.Generates s` means that `g` can transform its initial nonterminal to `s` in some number of
rewriting steps.  -/
ContextFreeGrammar.Generates : {T : Type u_1} → (g : ContextFreeGrammar T) → List (Symbol T g.NT) → Prop
-- Mathlib.Order.WithBot
WithBot.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (WithBot α)
-- Mathlib.CategoryTheory.Equivalence
/-- Promoting `Equivalence.congrRight` to a functor.  -/
CategoryTheory.Equivalence.congrRightFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            CategoryTheory.Functor (C ≌ D) (CategoryTheory.Functor E C ≌ CategoryTheory.Functor E D)
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.References.mk : Std.HashSet Lean.Syntax.Range →
  Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition →
    Std.HashSet Lean.FVarId →
      Std.HashMap Lean.FVarId Lean.FVarId →
        Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr) → Lean.Linter.UnusedVariables.References
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_addMonoidHom_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective AddMonoidHomClass.toAddMonoidHom
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.apply_lt_nfpFamily_iff : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Nonempty ι] [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) →
    ∀ {a b : Ordinal.{u}}, (∀ (i : ι), f i b < Ordinal.nfpFamily f a) ↔ b < Ordinal.nfpFamily f a
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.add : {R : Type u} → {M : Type v} → [Add R] → [Add M] → Add (TrivSqZeroExt R M)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c), (HomologicalComplex.opcyclesFunctor C c i).obj K = K.opcycles i
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getProduceMotiveAndRecursive : Array Lean.Expr → ℕ → ℕ → ℕ → Lean.Expr → Lean.MetaM (List Bool × Bool)
-- Init.Data.Bool
Bool.and_eq_decide : ∀ (p q : Bool), (p && q) = decide (p = true ∧ q = true)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.verbose.sizeOf_spec : sizeOf Lean.Lsp.Trace.verbose = 1
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.range_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {α : Sort u_13}
  (h : Diffeomorph I J M N n) (f : α → M), Set.range (⇑h ∘ f) = ⇑h.symm ⁻¹' Set.range f
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_def_of_mem : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) {q : Polynomial K}
  (hq : q ∈ nonZeroDivisors (Polynomial K)),
  RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p ⟨q, hq⟩ }
-- Mathlib.Computability.Partrec
Computable.ofNat : ∀ (α : Type u_5) [inst : Denumerable α], Computable (Denumerable.ofNat α)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULiftHom.up_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : C),
  CategoryTheory.ULiftHom.up.obj A = CategoryTheory.ULiftHom.objUp A
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_le_card_addGroup : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite G], Nat.card ↥H ≤ Nat.card G
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.internalHom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] (X : Cᵒᵖ),
  CategoryTheory.MonoidalClosed.internalHom.obj X = CategoryTheory.ihom (Opposite.unop X)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k k' : α} {f : β k → β k},
  (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_zero : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α], Multiset.inf 0 = ⊤
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inr f) F
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenrange.eq_1 : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ∞), f.genEigenrange μ k = ⨅ l, ⨅ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).range
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_ext_iff : ∀ {M N : AddCommMonCat} {f g : M ⟶ N}, f = g ↔ AddCommMonCat.Hom.hom f = AddCommMonCat.Hom.hom g
-- Init.Data.Array.Lemmas
Array.flatMap_singleton' : ∀ {α : Type u_1} (xs : Array α), Array.flatMap (fun x => #[x]) xs = xs
-- Mathlib.Order.BoundedOrder.Monotone
forall_le_iff : ∀ {α : Type u} [inst : Preorder α] {P : α → Prop} {x₀ : α}, Antitone P → ((∀ x ≤ x₀, P x) ↔ P x₀)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax left unity.  -/
CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X)) h)
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.quotientFunc_mk : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [inst_1 : SlashInvariantFormClass F 𝒢 k] (h : ↥ℋ), SlashInvariantForm.quotientFunc f ⟦h⟧ = SlashAction.map k (↑h)⁻¹ ⇑f
-- Mathlib.Data.List.TakeDrop
List.take_one_drop_eq_of_lt_length : ∀ {α : Type u} {l : List α} {n : ℕ} (h : n < l.length), List.take 1 (List.drop n l) = [l.get ⟨n, h⟩]
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.top_one : ⊤.HolderConjugate 1
-- Mathlib.Topology.Specialization
Specialization.ofEquiv_toEquiv : ∀ {α : Type u_1} (a : α), Specialization.ofEquiv (Specialization.toEquiv a) = a
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instIsEquivalenceGeneratedByTopCatToGeneratedByTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.toGeneratedByTopCat.IsEquivalence
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.mk.inj : ∀ {ι : Type u_1} {toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex ι}
  {singleton_mem : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex.faces}
  {toPreAbstractSimplicialComplex_1 : PreAbstractSimplicialComplex ι}
  {singleton_mem_1 : ∀ (v : ι), {v} ∈ toPreAbstractSimplicialComplex_1.faces},
  { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, singleton_mem := singleton_mem } =
      { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex_1, singleton_mem := singleton_mem_1 } →
    toPreAbstractSimplicialComplex = toPreAbstractSimplicialComplex_1
-- Mathlib.Order.Lattice.Nat
Nat.sInf_eq_zero : ∀ {s : Set ℕ}, sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
-- Mathlib.Data.Multiset.Bind
Multiset.fold_bind : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} (s : Multiset ι)
  (t : ι → Multiset α) (b : ι → α) (b₀ : α),
  Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (s.bind t) =
    Multiset.fold op b₀ (Multiset.map (fun i => Multiset.fold op (b i) (t i)) s)
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_mul_left_right : ∀ (a b c : ℤ), a.lcm b ∣ a.lcm (c * b)
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_add_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x : G),
  Filter.comap (fun x_1 => x_1 + -x) (nhds 0) = nhds x
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.set_mul_subset : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R} {I : TwoSidedIdeal R}, s ⊆ ↑I → ∀ (t : Set R), t * s ⊆ ↑I
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.refl_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G) (a : E), (GroupExtension.Equiv.refl S) a = a