mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated below from `f x` is countable.  -/
countable_image_gt_image_Ioi : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] (f : β → α) [SecondCountableTopology α],
  {x | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}.Countable
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Model.positionsFrom.eq_1 : ∀ {s : String} (p : s.Pos),
  String.Model.positionsFrom p = if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Model.positionsFrom (p.next h)
-- Mathlib.Data.Nat.Nth
Nat.nth_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, p n → Nat.nth p (Nat.count p n) = n
-- Mathlib.Data.Set.Sigma
Set.Nonempty.sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)},
  s.Nonempty → (∀ (i : ι), (t i).Nonempty) → (s.sigma t).Nonempty
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_finsetSum : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β)
  {f : β → α → ENNReal}, (∀ b ∈ s, Measurable (f b)) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBit.mk : ℕ → {w : ℕ} → Fin w → Std.Tactic.BVDecide.BVBit
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.mk.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (c : Lean.Expr) (gen numCases : ℕ) (splitSource : Lean.Meta.Grind.SplitSource),
  sizeOf { lctx := lctx, c := c, gen := gen, numCases := numCases, splitSource := splitSource } =
    1 + sizeOf lctx + sizeOf c + sizeOf gen + sizeOf numCases + sizeOf splitSource
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.hasZeroObject : ∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C)
-- Init.Grind.AC
Lean.Grind.AC.diseq_norm_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op} {x : Std.Commutative ctx.op}
  (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ac_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs ≠ Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Algebra.Group.Hom.Defs
/-- See note [hom simp lemma priority]  -/
map_pow : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Monoid G] [inst_2 : Monoid H]
  [MonoidHomClass F G H] (f : F) (a : G) (n : ℕ), f (a ^ n) = f a ^ n
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_iff_strictMono_get`. -/
StrictMono.sortedLT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], StrictMono l.get → l.SortedLT
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKey? k = t₂.getKey? k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f)[k]? = Option.map f t[k]?
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↑(CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)))
  (p : ↥(Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f)))),
  HomogeneousLocalization.val (↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom' x) p) =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.val x)
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mk.injEq : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)]
  (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet)
  (pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas)
  (continuous_trivChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source))
  (totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b))
  (pretrivializationAtlas_1 : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivializationAt_1 : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt_1 : ∀ (x : B), x ∈ (pretrivializationAt_1 x).baseSet)
  (pretrivialization_mem_atlas_1 : ∀ (x : B), pretrivializationAt_1 x ∈ pretrivializationAtlas_1)
  (continuous_trivChange_1 :
    ∀ e ∈ pretrivializationAtlas_1,
      ∀ e' ∈ pretrivializationAtlas_1, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source))
  (totalSpaceMk_isInducing_1 : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt_1 b) ∘ Bundle.TotalSpace.mk b)),
  ({ pretrivializationAtlas := pretrivializationAtlas, pretrivializationAt := pretrivializationAt,
        mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, continuous_trivChange := continuous_trivChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
      { pretrivializationAtlas := pretrivializationAtlas_1, pretrivializationAt := pretrivializationAt_1,
        mem_base_pretrivializationAt := mem_base_pretrivializationAt_1,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas_1, continuous_trivChange := continuous_trivChange_1,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing_1 }) =
    (pretrivializationAtlas = pretrivializationAtlas_1 ∧ pretrivializationAt = pretrivializationAt_1)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanModuleQuery.fromJson : Lean.Json → Except String Lean.Lsp.LeanModuleQuery
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_le_logb_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < x → 0 < y → (Real.logb b x ≤ Real.logb b y ↔ y ≤ x)
-- Mathlib.Topology.FiberBundle.Basic
MemTrivializationAtlas.mk : ∀ {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] {e : Bundle.Trivialization F Bundle.TotalSpace.proj},
  e ∈ trivializationAtlas F E → MemTrivializationAtlas e
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The canonical map from multivariate power series to the adic completion of
multivariate polynomials with respect to the ideal spanned by all variables
when the index is finite.  -/
MvPowerSeries.toAdicCompletion : (σ : Type u_3) →
  (R : Type u_4) →
    [Finite σ] →
      [inst : CommRing R] →
        MvPowerSeries σ R →ₐ[MvPolynomial σ R] AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.ext_iff : ∀ {α : Type w} {x y : Std.Iterators.Types.ListIterator α}, x = y ↔ x.list = y.list
-- Mathlib.Order.Filter.Pointwise
Filter.mul_pure : ∀ {α : Type u_2} [inst : Mul α] {f : Filter α} {b : α}, f * pure b = Filter.map (fun x => x * b) f
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
  [inst_2 : DecidableEq β], (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.eq_def : ∀ {α : Type u} (s : Stream'.WSeq α) (x : ℕ),
  s.drop x =
    match x with
    | 0 => s
    | n.succ => (s.drop n).tail
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAddMonoid : {σ : Type u_1} → {R : Type u_2} → [AddMonoid R] → AddMonoid (MvPowerSeries σ R)
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneracy_comp_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory} (θ : { len := n } ⟶ Δ'),
  ¬CategoryTheory.Mono θ → CategoryTheory.CategoryStruct.comp (X.map θ.op) (AlgebraicTopology.DoldKan.PInfty.f n) = 0
-- Init.Control.Except
/-- Transforms exceptions with a function, doing nothing on successful results.

Examples:
* `(pure 2 : Except String Nat).mapError (·.length) = pure 2`
* `(throw "Error" : Except String Nat).mapError (·.length) = throw 5`
 -/
Except.mapError : {ε : Type u} → {ε' : Type u_1} → {α : Type u_2} → (ε → ε') → Except ε α → Except ε' α
-- Mathlib.Data.List.InsertIdx
List.sublist_insertIdx : ∀ {α : Type u} (l : List α) (n : ℕ) (a : α), l.Sublist (l.insertIdx n a)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lift_symm_apply : ∀ (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (X : Type u_9)
  (f : (X →₀ R) →ₗ[R] M) (x : X), (Finsupp.lift M R X).symm f x = f fun₀ | x => 1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_zsmul : ∀ {R : Type u} [inst : Ring R] (a : ℤ) (b : Polynomial R), (a • b).toFinsupp = a • b.toFinsupp
-- Init.Data.Vector.Zip
/-- See also `getElem?_zipWith'` for a variant
using `Option.map` and `Option.bind` rather than a `match`.
 -/
Vector.getElem?_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {as : Vector α n} {bs : Vector β n} {f : α → β → γ} {i : ℕ},
  (Vector.zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- An Akra-Bazzi recurrence is a function that satisfies the recurrence
`T n = (∑ i, a i * T (r i n)) + g n`.  -/
AkraBazziRecurrence : {α : Type u_1} → [Fintype α] → [Nonempty α] → (ℕ → ℝ) → (ℝ → ℝ) → (α → ℝ) → (α → ℝ) → (α → ℕ → ℕ) → Type
-- Mathlib.Data.Finsupp.Single
Finsupp.single.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) (b : M),
  (fun₀ | a => b) = { support := if b = 0 then ∅ else {a}, toFun := Pi.single a b, mem_support_toFun := ⋯ }
-- Mathlib.CategoryTheory.GlueData
/-- The transition maps between the intersection of intersections.  -/
CategoryTheory.GlueData'.t' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData' C) →
      (i j k : self.J) →
        (hij : i ≠ j) →
          (hik : i ≠ k) →
            (hjk : j ≠ k) →
              CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k hik) ⟶
                CategoryTheory.Limits.pullback (self.f j k hjk) (self.f j i ⋯)
-- Lean.Parser.Types
Lean.Parser.ParserState.mk.injEq : ∀ (stxStack : Lean.Parser.SyntaxStack) (lhsPrec : ℕ) (pos : String.Pos.Raw) (cache : Lean.Parser.ParserCache)
  (errorMsg : Option Lean.Parser.Error)
  (recoveredErrors : Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error))
  (stxStack_1 : Lean.Parser.SyntaxStack) (lhsPrec_1 : ℕ) (pos_1 : String.Pos.Raw) (cache_1 : Lean.Parser.ParserCache)
  (errorMsg_1 : Option Lean.Parser.Error)
  (recoveredErrors_1 : Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)),
  ({ stxStack := stxStack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := errorMsg,
        recoveredErrors := recoveredErrors } =
      { stxStack := stxStack_1, lhsPrec := lhsPrec_1, pos := pos_1, cache := cache_1, errorMsg := errorMsg_1,
        recoveredErrors := recoveredErrors_1 }) =
    (stxStack = stxStack_1 ∧
      lhsPrec = lhsPrec_1 ∧ pos = pos_1 ∧ cache = cache_1 ∧ errorMsg = errorMsg_1 ∧ recoveredErrors = recoveredErrors_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α}, ∅.get? a = none
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Sigma.abs.eq_1 : ∀ {n : ℕ} {A : Type u} (F : A → TypeVec.{u} n → Type u) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u} n⦄
  (a : (MvQPF.Sigma.P F).A) (f : ((MvQPF.Sigma.P F).B a).Arrow α),
  MvQPF.Sigma.abs F ⟨a, f⟩ = ⟨a.fst, MvQPF.abs ⟨a.snd, f⟩⟩
-- Mathlib.Algebra.Module.PUnit
PUnit.instDistribMulAction : {R : Type u_1} → [inst : AddMonoid R] → DistribMulAction PUnit.{u_3 + 1} R
-- Mathlib.Algebra.Star.Unitary
Unitary.mul_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), U * star U = 1
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHomClass.toAddMonoidHomClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α} {inst_1 : FunLike F α α}
  [self : CentroidHomClass F α], AddMonoidHomClass F α α
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The sub-dp-ideal of I generated by a family of elements of A.  -/
DividedPowers.SubDPIdeal.span : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → (hI : DividedPowers I) → Set A → hI.SubDPIdeal
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprRaw_mathlib : Lean.ToExpr String.Pos.Raw
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instT4Space : T4Space UpperHalfPlane
-- Mathlib.Data.Finset.Image
/-- Given a finset `s` and a predicate `p`, `s.subtype p` is the finset of `Subtype p` whose
elements belong to `s`.  -/
Finset.subtype : {α : Type u_4} → (p : α → Prop) → [DecidablePred p] → Finset α → Finset (Subtype p)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The product of two elements of a subsemigroup belongs to the subsemigroup.  -/
NonUnitalSubsemiring.mul_mem' : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (self : NonUnitalSubsemiring R) {a b : R},
  a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- A vector in `K` is orthogonal to one in `Kᗮ`.  -/
Submodule.inner_right_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} {u v : E}, u ∈ K → v ∈ Kᗮ → inner 𝕜 u v = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.zeroKernelFork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.kernel.zeroKernelFork f) = 0
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`.  -/
Rep.counitIso : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (M : ModuleCat (MonoidAlgebra k G)) → (Rep.ofModuleMonoidAlgebra.comp Rep.toModuleMonoidAlgebra).obj M ≅ M
-- Mathlib.Topology.DerivedSet
relDerivedSet_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A : Set X), relDerivedSet A = derivedSet A ∩ A
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGT_basis_of_exists_gt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  (∃ b, a < b) → (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioo a)
-- Mathlib.Topology.MetricSpace.Isometry
/-- The natural isometry `(α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)` between the type of maps on a sum of
fintypes `α ⊕ β` and the pairs of functions on the types `α` and `β`.
`Equiv.sumArrowEquivProdArrow` as an `IsometryEquiv`.  -/
IsometryEquiv.sumArrowIsometryEquivProdArrow : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      [inst : PseudoEMetricSpace γ] → [inst_1 : Fintype α] → [inst_2 : Fintype β] → (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_true_iff_exists_minimal_eq_true : ∀ {n : ℕ} (p : Fin n → Bool), (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ j < i, p j = false
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {sieves : (X : C) → Set (CategoryTheory.Sieve X)}
  {top_mem' : ∀ (X : C), ⊤ ∈ sieves X}
  {pullback_stable' :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y}
  {transitive' :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X}
  {sieves_1 : (X : C) → Set (CategoryTheory.Sieve X)} {top_mem'_1 : ∀ (X : C), ⊤ ∈ sieves_1 X}
  {pullback_stable'_1 :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X),
      S ∈ sieves_1 X → CategoryTheory.Sieve.pullback f S ∈ sieves_1 Y}
  {transitive'_1 :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves_1 X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves_1 Y) → R ∈ sieves_1 X},
  { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' } =
      { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
        transitive' := transitive'_1 } →
    sieves = sieves_1
-- Mathlib.Algebra.Order.Group.Action.End
RelHom.smul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f : r →r r) (a : α), f • a = f a
-- Mathlib.Data.Set.Finite.Basic
/-- If `P` is some relation between terms of `γ` and sets in `γ`, such that every finite set
`t : Set γ` has some `c : γ` related to it, then there is a recursively defined sequence `u` in `γ`
so `u n` is related to the image of `{0, 1, ..., n-1}` under `u`.

(We use this later to show sequentially compact sets are totally bounded.)
 -/
Set.seq_of_forall_finite_exists : ∀ {γ : Type u_1} {P : γ → Set γ → Prop},
  (∀ (t : Set γ), t.Finite → ∃ c, P c t) → ∃ u, ∀ (n : ℕ), P (u n) (u '' Set.Iio n)
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measurableSet_isRatStieltjesPoint : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  Measurable f → MeasurableSet {a | ProbabilityTheory.IsRatStieltjesPoint f a}
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Dirac delta measures at two different points are different, assuming the measurable space
separates points.  -/
MeasureTheory.dirac_ne_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α},
  x ≠ y → MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `add_apply`. -/
AddGroupSeminorm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instInhabited.eq_1 : ∀ {α : Type u}, FreeGroup.instInhabited = { default := 1 }
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_sup_right : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G) [K.Normal], K.relIndex (H ⊔ K) = K.relIndex H
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A finite matrix `M : Matrix n n R` is positive semidefinite iff it is
Hermitian and `xᴴ * M * x` is nonnegative for all `x`.  -/
Matrix.posSemidef_iff_dotProduct_mulVec : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.PosSemidef ↔ M.IsHermitian ∧ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x
-- Lean.Declaration
Lean.QuotKind.ctor : Lean.QuotKind
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceSub : Lean.Meta.Simp.DSimproc
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.getJPParams : Lean.IR.LocalContext → Lean.IR.JoinPointId → Option (Array Lean.IR.Param)
-- Mathlib.Algebra.Module.Torsion.Basic
infinite_range_add_nsmul_iff : ∀ {M : Type u_2} [inst : AddCommGroup M] [IsAddTorsionFree M] (x y : M), (Set.range fun n => x + n • y).Infinite ↔ y ≠ 0
-- Lean.Elab.Tactic.Simp
/-- Checks the simp arguments for unused ones, and stores a bitmask of unused ones in the info tree,
to be picked up by the linter.
(This indirection is necessary because the same `simp` syntax may be executed multiple times,
and different simp arguments may be used in each step.)
 -/
Lean.Elab.Tactic.warnUnusedSimpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult) → Lean.Meta.Simp.UsedSimps → Lean.MetaM Unit
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instAlgHomClass : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B], AlgHomClass (A →⋆ₐ[R] B) R A B
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel γ δ) [ProbabilityTheory.IsSFiniteKernel η]
  (x : α × γ), (κ.parallelComp η) x = (κ x.1).prod (η x.2)
-- Init.Data.Vector.Attach
Vector.mk_congr : ∀ {α : Type u_1} {n : ℕ} {xs ys : Array α} (h : xs = ys) {h' : xs.size = n}, Vector.mk xs h' = Vector.mk ys ⋯
-- Mathlib.CategoryTheory.Sums.Basic
_private.Mathlib.CategoryTheory.Sums.Basic.0.CategoryTheory.sum.match_3.splitter : (C : Type u_1) →
  (D : Type u_2) →
    (motive : C ⊕ D → Sort u_3) →
      (X : C ⊕ D) → ((X : C) → motive (Sum.inl X)) → ((X : D) → motive (Sum.inr X)) → motive X
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- The full subcategory where `F.partialLeftAdjoint` shall be defined.  -/
CategoryTheory.Functor.PartialLeftAdjointSource : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → Type u₁
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation_symm_apply : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V),
  (o.rotation θ).symm x = θ.cos • x - θ.sin • o.rightAngleRotation x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.isoMk_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom)
      CategoryTheory.CostructuredArrow.isoMk._auto_1),
  (CategoryTheory.CostructuredArrow.isoMk g w).hom.left = g.hom
-- Mathlib.GroupTheory.SchurZassenhaus
/-- **Schur-Zassenhaus** for normal subgroups:
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
subgroup `K` which is a (left) complement of `H`.  -/
Subgroup.exists_left_complement'_of_coprime : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, H.IsComplement' N
-- Init.Data.String.Termination
String.Slice.Pos.wellFounded_gt : ∀ {s : String.Slice}, WellFounded fun p q => q < p
-- Lean.Server.Rpc.RequestHandling
Lean.Server.RpcProcedure : Type