mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  {a b : α}, b ≤ a → variationOnFromTo f s a b = -(eVariationOn f (s ∩ Set.Icc b a)).toReal
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAt.matches_slice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos),
  String.Slice.Pattern.Model.PatternModel.Matches pat (s.slice startPos endPos ⋯).copy
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every cokernel cofork `s` is isomorphic (actually, equal) to `cofork.ofπ (cofork.π s) _`.  -/
CategoryTheory.Limits.isoOfπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → {f : X ⟶ Y} → (s : CategoryTheory.Limits.Cofork f 0) → s ≅ CategoryTheory.Limits.Cofork.ofπ s.π ⋯
-- Mathlib.Algebra.Ring.Ext
Ring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : Ring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Algebra.Tropical.Lattice
instLatticeTropical : {R : Type u_1} → [Lattice R] → Lattice (Tropical R)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.coe_equalizer : ∀ {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] (ϕ ψ : A →ₐ[R] B), ↑(ϕ.equalizer ψ) = {a | ϕ a = ψ a}
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_symm_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (s : S₁),
  (MvPolynomial.sumRingEquiv R S₁ S₂).symm (MvPolynomial.X s) = MvPolynomial.X (Sum.inl s)
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.ofList_nil : ∀ {R : Type u_1} [inst : Semiring R], Ideal.ofList [] = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) h)
-- Mathlib.Topology.FiberBundle.Basic
/-- Associate to a trivialization index `i : ι` the corresponding trivialization, i.e., a bijection
between `proj ⁻¹ (baseSet i)` and `baseSet i × F`. As the fiber above `x` is `F` but read in the
chart with index `index_at x`, the trivialization in the fiber above x is by definition the
coordinate change from i to `index_at x`, so it depends on `x`.
The local trivialization will ultimately be an open partial homeomorphism. For now, we only
introduce the partial equivalence version, denoted with a prime.
In further developments, avoid this auxiliary version, and use `Z.local_triv` instead.  -/
FiberBundleCore.localTrivAsPartialEquiv : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → ι → PartialEquiv Z.TotalSpace (B × F)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) {Z : C} (h : r.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom
      (CategoryTheory.CategoryStruct.comp (Q.desc r) h) =
    CategoryTheory.CategoryStruct.comp (P.desc r) h
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.diff_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₁.diff m₂ = ↑(Std.DHashMap.Internal.Raw₀.diff ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The Gram operator T†T is symmetric. See `LinearMap.isSymmetric_adjoint_comp_self` for a version
where the domain and codomain are distinct.  -/
LinearMap.isSymmetric_adjoint_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E), (LinearMap.adjoint T * T).IsSymmetric
-- Init.Data.UInt.Bitwise
USize.shiftLeft_add : ∀ {a b c : USize},
  b < USize.ofNat System.Platform.numBits →
    c < USize.ofNat System.Platform.numBits →
      b + c < USize.ofNat System.Platform.numBits → a <<< (b + c) = a <<< b <<< c
-- Mathlib.Tactic.CongrExclamation
/-- Try to apply `Subsingleton.helim` if the goal is a `HEq`. Tries synthesizing a `Subsingleton`
instance for both the LHS and the RHS.

If successful, this reduces proving `@HEq α x β y` to proving `α = β`.
 -/
Lean.MVarId.subsingletonHelim? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Addition by a scalar with an element of the set remains in the set.  -/
VAddMemClass.vadd_mem : ∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} {inst : VAdd R M} {inst_1 : SetLike S M}
  [self : VAddMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ m ∈ s
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.self_trans_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.trans e.symm = AffineIsometryEquiv.refl 𝕜 P
-- Mathlib.Topology.GDelta.Basic
/-- Subsets of meagre sets are meagre.  -/
IsMeagre.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, t ⊆ s → IsMeagre s → IsMeagre t
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.erase_ne : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) {n i : ℕ},
  i ≠ n → (SkewPolynomial.erase n p).coeff i = p.coeff i
-- Mathlib.Data.ZMod.Defs
Fin.instCommMonoid : (n : ℕ) → [NeZero n] → CommMonoid (Fin n)
-- Std.Time.Date.Unit.Year
Std.Time.Year.Era.noConfusionType : Sort v✝ → Std.Time.Year.Era → Std.Time.Year.Era → Sort v✝
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (left : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left)
  (right : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right)
  (left_1 : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left)
  (right_1 : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right),
  ({ left := left, right := right } = { left := left_1, right := right_1 }) = (left = left_1 ∧ right = right_1)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.eq_1 : ∀ (f : (i : ℕ) → i < 0 → Bool), Nat.any 0 f = false
-- Mathlib.Data.Set.Image
Disjoint.preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β}, Disjoint s t → Disjoint (f ⁻¹' s) (f ⁻¹' t)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
  [MeasurableMul₂ M], Measurable f → Measurable g → Measurable (f * g)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.borelMarkovFromReal.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [inst : Nonempty Ω] [inst_1 : MeasurableSpace Ω]
  [inst_2 : StandardBorelSpace Ω] (η : ProbabilityTheory.Kernel α ℝ),
  ProbabilityTheory.Kernel.borelMarkovFromReal Ω η =
    (ProbabilityTheory.Kernel.piecewise ⋯ η
          (ProbabilityTheory.Kernel.deterministic (fun x => Exists.choose ⋯) ⋯)).comapRight
      ⋯
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Endowing the space `WithLp p (α × β)` with the `L^p` distance. We register this instance
separate from `WithLp.instProdPseudoMetricSpace` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future metric-like structure on `WithLp p (α × β)` for
`p < 1` satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*.  -/
WithLp.instProdDist : (p : ENNReal) → (α : Type u_2) → (β : Type u_3) → [Dist α] → [Dist β] → Dist (WithLp p (α × β))
-- Mathlib.FieldTheory.Finiteness
/-- In a Noetherian module over a division ring,
if a basis is indexed by a set, that set is finite.  -/
IsNoetherian.finite_basis_index : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  {s : Set ι} [IsNoetherian K V] (b : Module.Basis (↑s) K V), s.Finite
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffAddOfNatWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I 2 G], ContMDiffAdd I 1 G
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k a : α} [inst_3 : Inhabited (β a)], (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper.inj : ∀ {c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {c₃ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr}
  {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {c₃_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁ c₂ c₃ =
      Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁_1 c₂_1 c₃_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ c₃ = c₃_1
-- Mathlib.Order.Ideal
Order.Ideal.mk.sizeOf_spec : ∀ {P : Type u_2} [inst : LE P] [inst_1 : SizeOf P] (toLowerSet : LowerSet P) (nonempty' : toLowerSet.carrier.Nonempty)
  (directed' : DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier),
  sizeOf { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' } =
    1 + sizeOf toLowerSet + sizeOf nonempty'
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K]
  {F : CategoryTheory.Functor K C}
  [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj],
  CategoryTheory.Limits.PreservesColimit F J.yoneda
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- Consider a von Neumann algebra acting on a Hilbert space `H` as a \*-subalgebra of `H →L[ℂ] H`.
(That is, we forget that it is equal to its double commutant
or equivalently that it is closed in the weak and strong operator topologies.)
 -/
VonNeumannAlgebra.toStarSubalgebra : {H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [inst_2 : CompleteSpace H] → VonNeumannAlgebra H → StarSubalgebra ℂ (H →L[ℂ] H)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂)[k]! = default
-- Lean.Elab.Do.Basic
/-- Prepare the context for elaborating the body of a `finally` block.
There is no support for `mut` vars, `break`, `continue` or `return` in a `finally` block.
 -/
Lean.Elab.Do.enterFinally : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_def : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ),
  MvPowerSeries.X s = (MvPowerSeries.monomial fun₀ | s => 1) 1
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.branching : USize
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.isoEquivHomeo_apply : ∀ {X Y : CompactlyGenerated} (f : X ≅ Y), CompactlyGenerated.isoEquivHomeo f = CompactlyGenerated.homeoOfIso f
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- A *Coxeter matrix* is a symmetric matrix of natural numbers whose diagonal entries are equal to
1 and whose off-diagonal entries are not equal to 1.  -/
CoxeterMatrix : Type u_1 → Type u_1
-- Mathlib.Data.Fin.SuccPred
Fin.pred_castSucc_lt : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a.castSucc ≠ 0), a.castSucc.pred ha < a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → a ∉ m
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.extendRCLikeₗ_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F), Module.Dual.extendRCLikeₗ fr = fr.extendRCLike
-- Lean.Elab.ConfigEval.Util
_private.Lean.Elab.ConfigEval.Util.0.Lean.Elab.ConfigEval.planDerivation.go : Lean.Name →
  (Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) →
    Array Lean.Expr → Lean.ExprSet → Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Mathlib.Order.Filter.SmallSets
Filter.HasBasis.eventually_smallSets : ∀ {α : Type u_4} {ι : Sort u_5} {p : ι → Prop} {l : Filter α} {s : ι → Set α} {q : Set α → Prop} {hl : l.HasBasis p s},
  (∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s) → ((∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ i, p i ∧ q (s i))
-- Mathlib.Algebra.Group.Basic
div_eq_iff_comm : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a / b = c ↔ a / c = b
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.mkAlgHom_surjective : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Surjective ⇑(RingCon.mkₐ R (DividedPowerAlgebra.ringCon R M))
-- Mathlib.Analysis.ODE.PicardLindelof
/-- If the time-dependent vector field `f` is $C^n$ and the curve `α` is continuous, then
`picard f t₀ x₀ α` is also $C^n$. This version works for `n : ℕ`.  -/
ODE.contDiffOn_nat_picard_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {t₀ tmin tmax : ℝ},
  t₀ ∈ Set.Icc tmin tmax →
    ∀ {n : ℕ},
      ContDiffOn ℝ (↑n) (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u) →
        ContinuousOn α (Set.Icc tmin tmax) →
          (∀ t ∈ Set.Icc tmin tmax, α t ∈ u) →
            ∀ (x₀ : E),
              (∀ t ∈ Set.Icc tmin tmax, α t = ODE.picard f t₀ x₀ α t) →
                ContDiffOn ℝ (↑n) (ODE.picard f t₀ x₀ α) (Set.Icc tmin tmax)
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_accepts_iff_exists_path : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {x : List α},
  x ∈ M.accepts ↔ ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv (CategoryTheory.CategoryStruct.comp U.toSpecΓ h) = h
-- Mathlib.Algebra.Order.Group.Int.Sum
/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `Ico` version.  -/
Finset.sum_Ico_le_sum : ∀ {s : Finset ℤ} {c : ℤ}, (∀ x ∈ s, c ≤ x) → ∑ x ∈ Finset.Ico c (c + ↑s.card), x ≤ ∑ x ∈ s, x
-- Mathlib.Algebra.Category.Ring.Basic
/-- This prevents `RingCat.of R` being printed as `{ carrier := R, ring := ... }` by
`delabStructureInstance`.  -/
RingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.SInt.Basic
/-- Obtain the `BitVec` that contains the 2's complement representation of the `Int64`.
 -/
Int64.toBitVec : Int64 → BitVec 64
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.one_def : ∀ {α : Type u_1} {r : α → α → Prop}, 1 = RelEmbedding.refl r
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.one_apply : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : One β], (UniformOnFun.ofFun 𝔖) 1 = 1
-- Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Meta.NormNum.isNat_descFactorial_zero : ∀ {n x l y : ℕ} (z : ℕ),
  Mathlib.Meta.NormNum.IsNat n x →
    Mathlib.Meta.NormNum.IsNat l y → y = z + x + 1 → Mathlib.Meta.NormNum.IsNat (n.descFactorial l) 0
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  [inst_4 : TopologicalSpace H'] [inst_5 : TopologicalSpace M'] [inst_6 : ChartedSpace H' M']
  [inst_7 : ChartedSpace H H'] (x : M'), extChartAt I x = (chartAt H' x).trans (extChartAt I (↑(chartAt H' x) x))
-- Mathlib.LinearAlgebra.Charpoly.Basic
/-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a linear map, applied
to the linear map itself, is zero.

See `Matrix.aeval_self_charpoly` for the equivalent statement about matrices.  -/
LinearMap.aeval_self_charpoly : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M), (Polynomial.aeval f) f.charpoly = 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (S.map f.left) Y.hom = X.hom
-- Mathlib.Data.Rel
SetRel.inter_dom_subset_preimage_image : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α}, s ∩ R.dom ⊆ R.preimage (R.image s)
-- Mathlib.CategoryTheory.CatCommSq
/-- A variant of `hComp` where both squares can be explicitly provided.  -/
CategoryTheory.CatCommSq.hComp' : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₅ : Type u_5} →
          {C₆ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆] →
                        {T₁ : CategoryTheory.Functor C₁ C₂} →
                          {T₂ : CategoryTheory.Functor C₂ C₃} →
                            {V₁ : CategoryTheory.Functor C₁ C₄} →
                              {V₂ : CategoryTheory.Functor C₂ C₅} →
                                {V₃ : CategoryTheory.Functor C₃ C₆} →
                                  {B₁ : CategoryTheory.Functor C₄ C₅} →
                                    {B₂ : CategoryTheory.Functor C₅ C₆} →
                                      CategoryTheory.CatCommSq T₁ V₁ V₂ B₁ →
                                        CategoryTheory.CatCommSq T₂ V₂ V₃ B₂ →
                                          CategoryTheory.CatCommSq (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.nilradical_pow_eq_iInf : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R] (n : ℕ), nilradical R ^ n = ⨅ I, I.asIdeal ^ n
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.mk : {η : Type u_5} →
  {α : Type u_6} →
    {ι : Type u_7} → (idxFun : ι → α ⊕ η) → (∀ (e : η), ∃ i, idxFun i = Sum.inr e) → Combinatorics.Subspace η α ι
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.colimitCommMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommMonCat),
  CommMonCat.FilteredColimits.colimitCommMonoid F = { toMonoid := (CommMonCat.FilteredColimits.M F).str, mul_comm := ⋯ }
-- Mathlib.Data.EReal.Basic
EReal.toReal_bot : ⊥.toReal = 0
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.instOrderedSub : ∀ {α : Type u_1} [inst : DecidableEq α], OrderedSub (Multiset α)
-- Mathlib.SetTheory.Ordinal.Basic
WellOrder.mk.inj : ∀ {α : Type u} {r : α → α → Prop} {wo : IsWellOrder α r} {α_1 : Type u} {r_1 : α_1 → α_1 → Prop}
  {wo_1 : IsWellOrder α_1 r_1}, { α := α, r := r, wo := wo } = { α := α_1, r := r_1, wo := wo_1 } → α = α_1 ∧ r ≍ r_1
-- Mathlib.Analysis.Matrix.LDL
LDL.lowerInv_triangular : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef) {i j : n},
  i < j → LDL.lowerInv hS i j = 0
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_monic : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  (Matrix.charpoly.univ R n).Monic
-- Mathlib.Data.ZMod.Basic
ZMod.cast_natCast : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (k : ℕ), (↑k).cast = ↑k
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform equiv given a uniform embedding.  -/
UniformEquiv.ofIsUniformEmbedding : {α : Type u} →
  {β : Type u_1} →
    [inst : UniformSpace α] → [inst_1 : UniformSpace β] → (f : α → β) → IsUniformEmbedding f → α ≃ᵤ ↑(Set.range f)
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.eq_startPos_iff : ∀ {t₁ t₂ : String} {s : String.Slice} {p : s.Pos}, p.Splits t₁ t₂ → (p = s.startPos ↔ t₁ = "")
-- Mathlib.Topology.Bornology.Absorbs
Absorbent.mono : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t : Set α},
  Absorbent M s → s ⊆ t → Absorbent M t
-- Mathlib.GroupTheory.OreLocalization.Basic
_private.Mathlib.GroupTheory.OreLocalization.Basic.0.OreLocalization.smul''.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r : R) (s : ↥S),
  OreLocalization.smul''✝ r s = OreLocalization.liftExpand (OreLocalization.smul'✝ r s) ⋯
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps.mk : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx → ProofWidgets.InteractiveExprProps
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.exists_basis : ∀ (R : Type u) (M : Type v) {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Free R M], Nonempty ((I : Type v) × Module.Basis I R M)