mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.instLawfulFunctorObj : ∀ (P : PFunctor.{uA, uB}), LawfulFunctor ↑P
-- Init.Data.ByteArray.Basic
ByteArray.decEq : (lhs rhs : ByteArray) → Decidable (lhs = rhs)
-- Mathlib.Algebra.DirectSum.Decomposition
/-- A convenience method to construct a decomposition from an `AddMonoidHom`, such that the proofs
of left and right inverse can be constructed via `ext`.  -/
DirectSum.Decomposition.ofAddHom : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) →
                (decompose : M →+ DirectSum ι fun i => ↥(ℳ i)) →
                  (DirectSum.coeAddMonoidHom ℳ).comp decompose = AddMonoidHom.id M →
                    decompose.comp (DirectSum.coeAddMonoidHom ℳ) = AddMonoidHom.id (DirectSum ι fun i => ↥(ℳ i)) →
                      DirectSum.Decomposition ℳ
-- Mathlib.Algebra.Lie.Weights.Linear
/-- A typeclass encoding the fact that a given Lie module has linear weights, vanishing on the
derived ideal.  -/
LieModule.LinearWeights : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → [LieRing.IsNilpotent L] → Prop
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s)
  {Z : CategoryTheory.MorphismProperty.LeftFraction.Localization W}
  (h : (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s) h) =
    h
-- Mathlib.Data.Sym.Sym2
/-- The members of an unordered pair are members of the corresponding finite set.  -/
Sym2.mem_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {x : α} {z : Sym2 α}, x ∈ z.toFinset ↔ x ∈ z
-- Mathlib.GroupTheory.Congruence.Opposite
Con.op.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M),
  c.op = { r := fun a b => c (MulOpposite.unop b) (MulOpposite.unop a), iseqv := ⋯, mul' := ⋯ }
-- Mathlib.Order.Closure
/-- A closure operator on the preorder `α` is a monotone function which is extensive (every `x`
is less than its closure) and idempotent.  -/
ClosureOperator : (α : Type u_1) → [Preorder α] → Type u_1
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_eq_two_iff'`.  -/
Subgroup.relIindex_eq_two_iff' : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (a * b ∈ H) (b ∈ H)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedState.default : Lean.Elab.Tactic.State
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω),
  μ ≠ 0 → ∀ (s : Set Ω), μ.normalize s = μ.mass⁻¹ * μ s
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMapLinear_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : Semiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N]
  [inst_6 : ContinuousAdd N] [inst_7 : Module A M] [inst_8 : Module A N] [inst_9 : Module R N]
  [inst_10 : ContinuousConstSMul R N] [inst_11 : SMulCommClass A R N] (self : M [⋀^ι]→L[A] N),
  ContinuousAlternatingMap.toContinuousMultilinearMapLinear self = self.toContinuousMultilinearMap
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format the next expression.  -/
Lean.Meta.RefinedDiscrTree.keysAsPattern.go : Array Lean.Meta.RefinedDiscrTree.Key →
  optParam Bool true → StateRefT' IO.RealWorld (List Lean.Meta.RefinedDiscrTree.Key) Lean.CoreM Lean.MessageData
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.vertexSet_eq : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H ≤s G → H.vertexSet = G.vertexSet
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X)
      ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
      ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instMembership : {α : Type u} → {cmp : α → α → Ordering} → Membership α (Std.TreeSet.Raw α cmp)
-- Mathlib.Data.List.Lattice
List.Subset.inter_eq_left : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs ⊆ ys → xs ∩ ys = xs
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.congrN!.post : Congr!.Config → Lean.MVarId → CongrMetaM Unit
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.num_le_mul_inv : ∀ {K : Type u_3} [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K), ↑I.num ≤ I * I⁻¹
-- Mathlib.Topology.Compactification.StoneCech
/-- The natural map from α to its pre-Stone-Čech compactification.  -/
preStoneCechUnit : {α : Type u} → [inst : TopologicalSpace α] → α → PreStoneCech α
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_sSup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)},
  ↑(sSup S) = closure (⋃₀ (SetLike.coe '' S))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey!_modifyKey_eq_minKey! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  [inst_5 : Inhabited α] {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      Std.Internal.List.minKey! (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.minKey! l
-- Mathlib.Order.Filter.Prod
Filter.prod_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Filter α) (g : Filter β) (h : Filter γ),
  Filter.map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
-- Lean.Meta.Sym.Simp.SimpM
/-- Cache for context-independent results. Survives across binder entry and
across `simp` invocations within a `sym =>` block.
 -/
Lean.Meta.Sym.Simp.State.persistentCache : Lean.Meta.Sym.Simp.State → Lean.Meta.Sym.Simp.Cache
-- Mathlib.Data.Fintype.Sets
Set.toFinset_ssubset_univ : ∀ {α : Type u_1} [inst : Fintype α] {s : Set α} [inst_1 : Fintype ↑s], s.toFinset ⊂ Finset.univ ↔ s ⊂ Set.univ
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBound?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  (∃ y, t.upperBound? x = some y) ↔ ∃ y ∈ t, cmp x y ≠ Ordering.gt
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.flag_succ : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) (k : Fin n), b.flag k.succ = R ∙ b k ⊔ b.flag k.castSucc
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Slice.0.String.Slice.contains.match_1.congr_eq_2 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x) (x_1 : String.Slice.Pattern.SearchStep s),
  x = x_1 →
    (∀ (startPos endPos : s.Pos), x_1 = String.Slice.Pattern.SearchStep.matched startPos endPos → False) →
      (match x with
        | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
        | x => h_2 x) ≍
        h_2 x_1
-- Mathlib.Data.Set.MemPartition
finite_memPartition : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ), (memPartition f n).Finite
-- Mathlib.GroupTheory.Index
/-- The subgroup has finite index;
recall that `Subgroup.index` returns 0 when the index is infinite.  -/
Subgroup.FiniteIndex.index_ne_zero : ∀ {G : Type u_1} {inst : Group G} {H : Subgroup G} [self : H.FiniteIndex], H.index ≠ 0
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.toOrdinal.inj : ∀ {a b : Std.Time.Weekday}, a.toOrdinal = b.toOrdinal → a = b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_H0Iso_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (groupHomology.H0Iso A).inv = groupHomology.H0π A
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- The functor which sends a bicomplex to its associated graded object.  -/
HomologicalComplex₂.toGradedObjectFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (CategoryTheory.GradedObject (I₁ × I₂) C)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `Semiring` is a `Semiring`.  -/
SubsemiringClass.toSemiring : {S : Type v} →
  (s : S) → {R : Type u_1} → [inst : Semiring R] → [inst_1 : SetLike S R] → [SubsemiringClass S R] → Semiring ↥s
-- Lean.Data.Lsp.Extra
/-- `textDocument/waitForDiagnostics` client->server request.

Yields a response when all the diagnostics for a version of the document greater or equal to the
specified one have been emitted. If the request specifies a version above the most recently
processed one, the server will delay the response until it does receive the specified version.
Exists for synchronization purposes, e.g. during testing or when external tools might want to use
our LSP server.  -/
Lean.Lsp.WaitForDiagnosticsParams : Type
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- A subgroup of a seminormed additive group is also a seminormed additive group,
with the restriction of the norm.  -/
AddSubgroupClass.seminormedAddGroup : {E : Type u_1} →
  [inst : SeminormedAddGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [AddSubgroupClass S E] → (s : S) → SeminormedAddGroup ↥s
-- Mathlib.Data.Int.Cast.Lemmas
MonoidHom.ext_mint : ∀ {M : Type u_5} [inst : Monoid M] {f g : Multiplicative ℤ →* M},
  f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1) → f = g
-- Init.Data.String.Basic
String.Pos.Raw.IsValid.toSlice : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.IsValid s p → String.Pos.Raw.IsValidForSlice s.toSlice p
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLT! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
multipliable_pnat_iff_multipliable_nat : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G},
  (Multipliable fun n => f ↑n) ↔ Multipliable f
-- Mathlib.Dynamics.OmegaLimit
Flow.isInvariant_omegaLimit : ∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddMonoid τ] {α : Type u_2} [inst_2 : TopologicalSpace α]
  (f : Filter τ) (ϕ : Flow τ α) (s : Set α),
  (∀ (t : τ), Filter.Tendsto (fun x => t + x) f f) → IsInvariant ϕ.toFun (omegaLimit f ϕ.toFun s)
-- Mathlib.Order.Interval.Basic
instInhabitedInterval : (α : Type u_1) → [inst : LE α] → Inhabited (Interval α)
-- Init.Data.Float.Model.Unpacked.Round
/-- Extracts the mantissa, rounded according to the data in the residual bits.
 -/
Float.Model.UnpackedFloat.ExtendedMantissa.roundedMantissa : Float.Model.UnpackedFloat.ExtendedMantissa → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.Copy.minDegree_mono`. -/
SimpleGraph.Copy.minDegree_le : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj] {f : G.Copy H},
  Function.Surjective ⇑f → G.minDegree ≤ H.minDegree
-- Mathlib.Topology.Compactness.Compact
/-- A variant of `generalized_tube_lemma` that only replaces the set in one direction.  -/
generalized_tube_lemma_right : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsCompact s →
    ∀ {t t' : Set Y},
      IsCompact t → ∀ {n : Set (X × Y)}, n ∈ nhdsSetWithin (s ×ˢ t) (s ×ˢ t') → ∃ u ∈ nhdsSetWithin t t', s ×ˢ u ⊆ n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is continuous on `t : Set X` and `0 ≤ a x` for all `x ∈ t`.
Suppose further that `s : X → Set ℝ≥0` is a family of sets with `s x` compact when
`x ∈ t` such that `s x₀` contains the spectrum of `a x` for all sufficiently close `x ∈ t`.
If `f : ℝ≥0 → ℝ≥0` is continuous on `s x`, for each `x ∈ t`, then `fun x ↦ cfc f (a x)` is
continuous on `t`.  -/
ContinuousOn.cfc_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X},
  (∀ x ∈ t, IsCompact (s x)) →
    ContinuousOn a t →
      (∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s x₀) →
        (∀ x ∈ t, 0 ≤ a x) →
          autoParam (∀ x ∈ t, ContinuousOn f (s x)) ContinuousOn.cfc_nnreal._auto_1 →
            ContinuousOn (fun x => cfc f (a x)) t
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-- The function `z ^ w` is continuous in `(z, w)` provided that `z` does not belong to the interval
`(-∞, 0]` on the real line. See also `Complex.continuousAt_cpow_zero_of_re_pos` for a version that
works for `z = 0` but assumes `0 < re w`.  -/
continuousAt_cpow : ∀ {p : ℂ × ℂ}, p.1 ∈ Complex.slitPlane → ContinuousAt (fun x => x.1 ^ x.2) p
-- Mathlib.SetTheory.Ordinal.Notation
NONote.repr_opow : ∀ (a b : NONote), (a.opow b).repr = a.repr ^ b.repr
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {x y : E} (n : ℕ) (t : Finset (Fin n)),
  have s := FormalMultilinearSeries.changeOriginIndexEquiv.symm ⟨n, t⟩;
  (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y) =
    (p n) (t.piecewise (fun x_1 => x) fun x => y)
-- Mathlib.Topology.Separation.Basic
/-- Removing a finset from a dense set in a space without isolated points, one still
obtains a dense set.  -/
Dense.sdiff_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X},
  Dense s → ∀ (t : Finset X), Dense (s \ ↑t)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.arrayLit : Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.coe_restrictScalars_symm' : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B), ⇑(AlgEquiv.restrictScalars R f).symm = ⇑f.symm
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f₁ f₂ : E →L[𝕜] E)
  (g₁ g₂ : F →L[𝕜] F), TensorProduct.mapL (f₁ * f₂) (g₁ * g₂) = TensorProduct.mapL f₁ g₁ * TensorProduct.mapL f₂ g₂
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_eq_univ : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, ↑U = Set.univ ↔ U = ⊤
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.thursday.sizeOf_spec : sizeOf Std.Time.Weekday.thursday = 1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology data for a short complex consists of two compatible left and
right homology data  -/
CategoryTheory.ShortComplex.HomologyData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Type (max u v)
-- Mathlib.Order.Grade
Flag.isMax_coe : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Flag α} {a : ↥s}, IsMax ↑a ↔ IsMax a
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_apply_apply : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (x : ℕ),
  (Polynomial.derivativeFinsupp p) x = (⇑Polynomial.derivative)^[x] p
-- Mathlib.CategoryTheory.GlueData
/-- The index type `J` of a gluing datum  -/
CategoryTheory.GlueData.J : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → CategoryTheory.GlueData C → Type v
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Unit.borelSpace : BorelSpace Unit
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.instFullCatTypeToCat : CategoryTheory.typeToCat.Full
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- The action of `stabilizer M a` is one-less preprimitive.  -/
AddAction.isMultiplyPreprimitive_ofStabilizer : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] [AddAction.IsPretransitive M α] {n : ℕ}
  {a : α} [AddAction.IsMultiplyPreprimitive M α n.succ],
  AddAction.IsMultiplyPreprimitive (↥(AddAction.stabilizer M a)) (↥(SubAddAction.ofStabilizer M a)) n
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.scale : ℕ → Mathlib.Tactic.Linarith.CompSource → Mathlib.Tactic.Linarith.CompSource
-- Mathlib.NumberTheory.SmoothNumbers
/-- The set of `k`-rough numbers `≤ N` can be written as the union of the sets of multiples `≤ N`
of primes `k ≤ p ≤ N`.  -/
Nat.roughNumbersUpTo_eq_biUnion : ∀ (N k : ℕ),
  N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun p => {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.natAbs_ediv_le_natAbs.aux : ∀ (a : ℤ) (n : ℕ), (a / ↑n).natAbs ≤ a.natAbs
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.lift_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S' : CategoryTheory.SubmonoidFunctor M') (hp : CategoryTheory.SubmonoidFunctor.image p ⊤ ≤ S') (U : C),
  (CategoryTheory.SubmonoidFunctor.lift p S' hp).app U =
    MonCat.ofHom ((MonCat.Hom.hom (p.app U)).codRestrict (S'.obj U) ⋯)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.
 -/
CategoryTheory.Limits.HasColimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [CommSemiring R] → CommSemiring (l.Germ R)
-- Lean.Environment
Lean.Kernel.instNonemptyEnvironment : Nonempty Lean.Kernel.Environment
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H),
  (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).hom = ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The precomposition of an homotopy with a relative morphism.  -/
SSet.RelativeMorphism.Homotopy.precomp : {X Y Z : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {C : Z.Subcomplex} →
          {ψ : B.toSSet ⟶ C.toSSet} →
            {f' g' : SSet.RelativeMorphism B C ψ} →
              f'.Homotopy g' →
                (f : SSet.RelativeMorphism A B φ) →
                  {φψ : A.toSSet ⟶ C.toSSet} →
                    (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) → (f.comp f' fac).Homotopy (f.comp g' fac)
-- Batteries.Data.MLList.Basic
/-- Constructs an `MLList` recursively. If `f` returns `none` the list will terminate.

Returns the initial value as the first element.
 -/
MLList.fix? : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → m (Option α)) → α → MLList m α
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp.eq_1 : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (χ : MulChar R R') (f : R' →+* R''),
  χ.ringHomComp f = { toFun := fun a => f (χ a), map_one' := ⋯, map_mul' := ⋯, map_nonunit' := ⋯ }
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_iSup : ∀ {R : Type u} [inst : Semiring R] (I : Ideal R) {ι : Sort u_1} (J : ι → Ideal R), I * ⨆ i, J i = ⨆ i, I * J i
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRank_le_finrank : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [Nontrivial R],
  φ.nilRank ≤ Module.finrank R M