mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.mk : {R : Type u_2} →
  [inst : NonUnitalNonAssocRing R] →
    (toRingSeminorm : RingSeminorm R) → (∀ (x : R), toRingSeminorm.toFun x = 0 → x = 0) → RingNorm R
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithZero.map f = Option.map f
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.keepAliveTimeMs : ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCircuit_map_iff_of_injective : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u},
  Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsCircuit ↔ p.IsCircuit)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.rightUnitor_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (m : ↑M) (r : R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.tendsto_nhds_one : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
-- Mathlib.Data.List.Find
_private.Mathlib.Data.List.Find.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.reverse_e0 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), CliffordAlgebra.reverse (CliffordAlgebra.EquivEven.e0 Q) = CliffordAlgebra.EquivEven.e0 Q
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` and `K` are equivalent, then if `J` is preconnected then `K` is as well.  -/
CategoryTheory.isPreconnected_of_equivalent : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.IsPreconnected J] (e : J ≌ K), CategoryTheory.IsPreconnected K
-- Init.Data.FloatArray.Basic
FloatArray.set! : FloatArray → ℕ → Float → FloatArray
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- The degree of the minimal polynomial of an element `a ∈ L` equals
`ringExpChar K ^ elemExponent K a`.  -/
IsPurelyInseparable.minpoly_natDegree_eq : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (a : L),
  (minpoly K a).natDegree = ringExpChar K ^ IsPurelyInseparable.elemExponent K a
-- Mathlib.RingTheory.Jacobson.Ideal
TwoSidedIdeal.jacobson.eq_1 : ∀ {R : Type u} [inst : Ring R] (I : TwoSidedIdeal R), I.jacobson = (TwoSidedIdeal.asIdeal I).jacobson.toTwoSided
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNatCast_1 : {α : Type u} →
  [inst : TopologicalSpace α] → {R : Type u_1} → [inst_1 : SeminormedRing R] → NatCast (BoundedContinuousFunction α R)
-- Mathlib.CategoryTheory.Sites.Pullback
/-- The constructed `sheafPullback G A J K` is left adjoint
to `G.sheafPushforwardContinuous A J K`.  -/
CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type u₁) →
            [inst_2 : CategoryTheory.Category.{v₁, u₁} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsContinuous J K] →
                    [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] →
                      [inst_5 : CategoryTheory.HasWeakSheafify K A] →
                        CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback G A J K ⊣
                          G.sheafPushforwardContinuous A J K
-- Lean.Parser.Attr
Lean.Parser.priorityParser : optParam ℕ 0 → Lean.Parser.Parser
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.mk : Option Lean.Lsp.ModuleHierarchyOptions → Option Lean.Lsp.RpcOptions → Lean.Lsp.LeanServerCapabilities
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] (i : R →+* T) (x : T) (hx : Polynomial.eval₂ i x f = 0),
  h.lift i x hx =
    { toFun := fun z => Polynomial.eval₂ i x (h.repr z), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.convs'Aux.match_1.eq_1 : ∀ {K : Type u_1} (motive : Stream'.Seq (GenContFract.Pair K) → ℕ → Sort u_2) (x : Stream'.Seq (GenContFract.Pair K))
  (h_1 : (x : Stream'.Seq (GenContFract.Pair K)) → motive x 0)
  (h_2 : (s : Stream'.Seq (GenContFract.Pair K)) → (n : ℕ) → motive s n.succ),
  (match x, 0 with
    | x, 0 => h_1 x
    | s, n.succ => h_2 s n) =
    h_1 x
-- Init.Data.Vector.Lemmas
/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array.  -/
Vector.getElem_append_right' : ∀ {α : Type u_1} {m n i : ℕ} (xs : Vector α m) {ys : Vector α n} (hi : i < n), ys[i] = (xs ++ ys)[i + m]
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.bot : {α : Type u_1} → [inst : HeytingAlgebra α] → Bot (Heyting.Regular α)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.eq_of_eq_union_iUnion : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (I J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)),
  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j → I = J
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_4 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁₁ l₁₂ : Lean.Level) (k₁ : ℕ) (l₂₁ l₂₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match l₁₁.imax l₁₂, k₁, l₂₁.imax l₂₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_4 (l₁₁.imax l₁₂) l₁₁ l₁₂ ⋯ k₁ (l₂₁.imax l₂₂) l₂₁ l₂₂ ⋯ k₂
-- Mathlib.Analysis.Meromorphic.Order
/-- If the order of a meromorphic function is zero, then this function converges to a nonzero
limit at this point. See also the iff version `tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero`.  -/
tendsto_ne_zero_of_meromorphicOrderAt_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → meromorphicOrderAt f x = 0 → ∃ c, c ≠ 0 ∧ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ}
  (h : AlgebraicTopology.NormalizedMooreComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) h
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_pow_iff_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ}
  [ZeroLEOneClass M₀], 0 ≤ a → n ≠ 0 → (1 ≤ a ^ n ↔ 1 ≤ a)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.mk.injEq : ∀ {γ : Type} (defn : Lean.KeyedDeclsAttribute.Def γ) (tableRef : IO.Ref (Lean.KeyedDeclsAttribute.Table γ))
  (ext : Lean.KeyedDeclsAttribute.Extension γ) (defn_1 : Lean.KeyedDeclsAttribute.Def γ)
  (tableRef_1 : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)) (ext_1 : Lean.KeyedDeclsAttribute.Extension γ),
  ({ defn := defn, tableRef := tableRef, ext := ext } = { defn := defn_1, tableRef := tableRef_1, ext := ext_1 }) =
    (defn = defn_1 ∧ tableRef = tableRef_1 ∧ ext = ext_1)
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `coeff g` as an additive monoid/group homomorphism  -/
HahnSeries.coeff.addMonoidHom : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddMonoid R] → Γ → HahnSeries Γ R →+ R
-- Mathlib.Data.Tree.Basic
BinaryTree.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf BinaryTree.nil = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.Order.CompactlyGenerated.Basic
Directed.disjoint_iSup_left : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {f : ι → α} [IsCompactlyGenerated α] {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pushforward_mono : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] {f g : CompactlySupportedContinuousMap B ℝ},
  f ≤ g → (H.pushforward μA) f ≤ (H.pushforward μA) g
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂), ψ.op.φH = ψ.φH.op
-- Mathlib.Logic.Basic
forall_or_left : ∀ {α : Sort u_1} {q : Prop} {p : α → Prop}, (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
-- Mathlib.Topology.Continuous
continuousAt_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, ContinuousAt id x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_eq_mk_iff' : ∀ {α : Type u_1} [inst : CommMonoid α] [IsCancelMul α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
  Localization.mk a₁ a₂ = Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁
-- Std.Async.Timer
/-- If:
- `i` is not yet running start it and return an `Async` computation that completes right away as the 0th
  multiple of `duration` has elapsed.
- `i` is already running and:
  - the tick from the last call of `i` has not yet finished return the same `Async` computation as the last
    call
  - the tick from the last call of `i` has finished return a new `Async` computation that waits for the
    closest next tick from the time of calling this function.
- `i` is not running anymore this is a no-op.
 -/
Std.Async.Interval.tick : Std.Async.Interval → Std.Async.Async Unit
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- A finite measure coerced into a real function is a signed measure.  -/
MeasureTheory.Measure.toSignedMeasure : {α : Type u_1} →
  {m : MeasurableSpace α} →
    (μ : MeasureTheory.Measure α) → [hμ : MeasureTheory.IsFiniteMeasure μ] → MeasureTheory.SignedMeasure α
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity `l`, and its derivative is nonnegative, then the
integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
`integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and
continuity at `a⁺`.  -/
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  ContinuousWithinAt g (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, 0 ≤ g' x) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
-- Init.Data.List.ToArray
Array.getLast_toList : ∀ {α : Type u_1} (xs : Array α) (h : xs.toList ≠ []), xs.toList.getLast h = xs.back ⋯
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f + gp, g) = Res(f, g)` if `deg g + deg p ≤ deg f`.  -/
Polynomial.resultant_add_mul_left : ∀ {R : Type u_1} [inst : CommRing R] (f g p : Polynomial R) (m n : ℕ),
  p.natDegree + n ≤ m → g.natDegree ≤ n → (f + g * p).resultant g m n = f.resultant g m n
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.lie_h_f_nsmul : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L}, IsSl2Triple h e f → ⁅h, f⁆ = -(2 • f)
-- Batteries.Util.Pickle
/-- Load an object from disk.
Note: The returned `CompactedRegion` can be used to free the memory behind the value
of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are
released). Ignoring the `CompactedRegion` results in the data being leaked.
Use `withUnpickle` to call `CompactedRegion.free` automatically.

This function is unsafe because the data being loaded may not actually have type `α`, and this
may cause crashes or other bad behavior.
 -/
unpickle : (α : Type) → System.FilePath → IO (α × Lean.CompactedRegion)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.smul_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] [inst_8 : LieAlgebra R L] [inst_9 : LieModule R L N] (t : R)
  (f : M →ₗ⁅R,L⁆ N) (m : M), (t • f) m = t • f m
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.completionProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.CompletionOptions
-- Mathlib.Data.Complex.Basic
/-- Reduce `Complex.I ^ n` to `Complex.I ^ (n % 4)` when `n` is a literal natural number at
least `4`. Combined with `Nat.reduceMod` this normalises every literal power of `I` to one of
`I ^ 0`, `I ^ 1`, `I ^ 2`, `I ^ 3`, which the existing `@[simp]` lemmas dispatch.  -/
Complex.I_pow_eq_pow_mod' : Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {f g h : Polynomial R}, (AdjoinRoot.mk f) g = (AdjoinRoot.mk f) h ↔ f ∣ g - h
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_normedSpace_dom : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕝] [inst_1 : AddCommGroup F]
  [inst_2 : NormedField 𝕝₂] [inst_3 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (E : Type u_11)
  [inst_5 : SeminormedAddCommGroup E] [inst_6 : NormedSpace 𝕝 E] [inst_7 : TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F},
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), (∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E) → Continuous ⇑f
-- Mathlib.CategoryTheory.Subobject.Presheaf
Subobject.presheaf_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] (X : Cᵒᵖ),
  (Subobject.presheaf C).obj X = CategoryTheory.Subobject (Opposite.unop X)
-- Init.Data.Nat.Lemmas
Nat.div_eq_zero_iff : ∀ {a b : ℕ}, a / b = 0 ↔ b = 0 ∨ a < b
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_equiv_zero' : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv},
  f ≈ 0 → f * g ≈ 0
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
AlgHom.fieldRange_eq_map : ∀ {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 F K] (f : E →ₐ[F] K), f.fieldRange = IntermediateField.map f ⊤
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid is closed under multiplication.  -/
Submonoid.mul_mem : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.tendsto_setToFun_approxOn_of_measurable : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) [inst_4 : MeasurableSpace E]
  [inst_5 : BorelSpace E] {f : α → E} {s : Set E} [inst_6 : TopologicalSpace.SeparableSpace ↑s],
  MeasureTheory.Integrable f μ →
    ∀ (hfm : Measurable f),
      (∀ᵐ (x : α) ∂μ, f x ∈ closure s) →
        ∀ {y₀ : E} (h₀ : y₀ ∈ s),
          MeasureTheory.Integrable (fun x => y₀) μ →
            Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT ⇑(MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n))
              Filter.atTop (nhds (MeasureTheory.setToFun μ T hT f))
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_inv_id_hom_assoc : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A)
  {Z : CategoryTheory.Functor C D} (h : F.functor n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.hom n) (CategoryTheory.CategoryStruct.comp (e.inv.hom n) h) = h
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.Regular.neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [ContinuousNeg G] [μ.Regular], μ.neg.Regular
-- Lean.Message
Lean.MessageData.withNamingContext.sizeOf_spec : ∀ (a : Lean.NamingContext) (a_1 : Lean.MessageData),
  sizeOf (Lean.MessageData.withNamingContext a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `upperSemicontinuous_iff_IsClosed_hypograph`. -/
UpperSemicontinuous.IsClosed_hypograph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIicTopology γ] {f : α → γ}, UpperSemicontinuous f → IsClosed {p | p.2 ≤ f p.1}
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedInClass.mk : {B : Type u_5} →
  {E : outParam (Type u_6)} →
    {F : outParam (Type u_7)} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedSpace ℝ F] →
              {n : outParam ℕ∞} →
                {K : outParam (TopologicalSpace.Compacts E)} →
                  [toDFunLike : DFunLike B E fun x => F] →
                    (∀ (f : B), ContDiff ℝ ↑n ⇑f) →
                      (∀ (f : B), Set.EqOn (⇑f) 0 (↑K)ᶜ) → ContDiffMapSupportedInClass B E F n K
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The natural group hom from an additive subgroup of `AddGroup` `G` to `G`.  -/
AddSubgroupClass.subtype : {G : Type u_1} →
  [inst : AddGroup G] → {S : Type u_4} → (H : S) → [inst_1 : SetLike S G] → [inst_2 : AddSubgroupClass S G] → ↥H →+ G
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The map from the original ring into the Cauchy completion.  -/
CauSeq.Completion.ofRat : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → β → CauSeq.Completion.Cauchy abv
-- Lean.Meta.Basic
/-- Runs `k` in a local environment with the `fvarIds` erased.
 -/
Lean.Meta.withErasedFVars : {n : Type → Type} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] → {α : Type} → [Lean.MonadLCtx n] → [MonadLiftT Lean.MetaM n] → Array Lean.FVarId → n α → n α
-- Init.Data.SInt.Basic
/-- Bitwise left shift for 32-bit signed integers. Usually accessed via the `<<<` operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.shiftLeft : Int32 → Int32 → Int32
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A countably compact Lindelöf set is compact.  -/
IsLindelof.isCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsCountablyCompact A → IsLindelof A → IsCompact A
-- Mathlib.Order.WithBot
WithTop.lattice : {α : Type u_1} → [Lattice α] → Lattice (WithTop α)
-- Mathlib.RingTheory.Derivation.ToSquareZero
diffToIdealOfQuotientCompEq.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) (f₁ f₁_1 : A →ₐ[R] B) (e_f₁ : f₁ = f₁_1)
  (f₂ f₂_1 : A →ₐ[R] B) (e_f₂ : f₂ = f₂_1) (e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂),
  diffToIdealOfQuotientCompEq I f₁ f₂ e = diffToIdealOfQuotientCompEq I f₁_1 f₂_1 ⋯
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Inclusion of `𝓓^{n}_{K}(E, F)` into the space `E →ᵇ F` of bounded continuous maps
as a `𝕜`-linear map.

This is subsumed by `toBoundedContinuousFunctionCLM`, which also bundles the continuity.  -/
ContDiffMapSupportedIn.toBoundedContinuousFunctionLM : (𝕜 : 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] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    {n : ℕ∞} →
                      {K : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n K →ₗ[𝕜] BoundedContinuousFunction E F
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes`.

---

The first uniqueness theorem for primary decomposition, Theorem 4.5 in Atiyah-Macdonald:
In any minimal primary decomposition `I = ⨅ i, q_i`, the ideals `radical (q_i.colon M)` are exactly
the associated primes of `I`.  -/
Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t → (fun J => (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasCoproductsOfShape_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂)
  [CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ], CategoryTheory.Limits.HasCoproductsOfShape X C