mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
cfcₙHomSuperset.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s),
  cfcₙHomSuperset ha hs = cfcₙHomSuperset ⋯ hs
-- Mathlib.Data.Set.Disjoint
/-- **Alias** of the reverse direction of `Set.not_disjoint_iff_nonempty_inter`. -/
Set.Nonempty.not_disjoint : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty → ¬Disjoint s t
-- Mathlib.Tactic.Linter.Style
/-- Run the `show` tactic, with a linter warning when one should use `change` instead.  -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.elabShow : Lean.Term → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.finitePresentation_universalFactorizationMap : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  (MvPolynomial.universalFactorizationMap R n m k hn).FinitePresentation
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Whether unexpanding is allowed with this argument.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.canUnexpand : Lean.PrettyPrinter.Delaborator.AppImplicitArg → Bool
-- Mathlib.Order.Partition.Finpartition
/-- Parts of a `Finpartition` are pairwise disjoint under an inf-bot-preserving map.  -/
Finpartition.pairwiseDisjoint_apply : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {β : Type u_2} {f : α → β}
  [inst_2 : SemilatticeInf β] [inst_3 : OrderBot β],
  (∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) → f ⊥ = ⊥ → (↑P.parts).PairwiseDisjoint f
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.sup_factors_of_factors_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B},
  X.Factors f → (X ⊔ Y).Factors f
-- Mathlib.Algebra.Group.Action.Basic
isCancelSMul_iff_eq_one_of_smul_eq : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β],
  IsCancelSMul α β ↔ ∀ (g : α) (x : β), g • x = x → g = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.C_mul_leadingCoeff_monomial_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R),
  MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1 = m.leadingTerm p
-- Mathlib.Data.Finset.Prod
Finset.offDiag_inter : ∀ {α : Type u_1} (s t : Finset α) [inst : DecidableEq α], (s ∩ t).offDiag = s.offDiag ∩ t.offDiag
-- Init.Data.Stream
Std.instToStreamList : {α : Type u_1} → Std.ToStream (List α) (List α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {n : ℤ} {X Y : C} {f₁ f₂ : (t.truncGE n).obj X ⟶ Y},
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₁ =
      CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₂ →
    ∀ [t.IsGE Y n], f₁ = f₂
-- Mathlib.Logic.Equiv.Set
/-- The set `Set.pi Set.univ s` is equivalent to `Π a, s a`.  -/
Equiv.Set.univPi : {α : Type u_3} → {β : α → Type u_4} → (s : (a : α) → Set (β a)) → ↑(Set.univ.pi s) ≃ ((a : α) → ↑(s a))
-- Mathlib.Topology.Order.OrderClosed
isOpen_Iio : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a : α}, IsOpen (Set.Iio a)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.edist_def : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : ↥(MeasureTheory.Lp β 1 μ)), edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
-- Init.WFComputable
/-- A computable version of `fix`.  -/
WellFounded.fixC : {α : Sort u} →
  {C : α → Sort v} → {r : α → α → Prop} → WellFounded r → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → C x
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The sections of a sheaf (i.e. evaluation as a presheaf on `C`).  -/
CategoryTheory.sheafSections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor (CategoryTheory.Sheaf J A) A)
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bindOnSupport_pure : ∀ {α : Type u_1} (p : PMF α), (p.bindOnSupport fun a x => PMF.pure a) = p
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.mk.inj : ∀ {x optType : Lean.Syntax} {codeBlock : Lean.Elab.Term.Do.CodeBlock} {x_1 optType_1 : Lean.Syntax}
  {codeBlock_1 : Lean.Elab.Term.Do.CodeBlock},
  { x := x, optType := optType, codeBlock := codeBlock } =
      { x := x_1, optType := optType_1, codeBlock := codeBlock_1 } →
    x = x_1 ∧ optType = optType_1 ∧ codeBlock = codeBlock_1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.isCyclic : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α] (H : Subgroup α), IsCyclic ↥H
-- Init.Data.BitVec.Basic
BitVec.or_eq : ∀ {w : ℕ} (x y : BitVec w), x.or y = x ||| y
-- Mathlib.Data.Nat.Find
Nat.find_add : ∀ {n : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] {hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n},
  n ≤ Nat.find hₙ → Nat.find hₘ + n = Nat.find hₙ
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two zero-preserving morphisms `f`, `g`,
`f - g` is the additive morphism sending `x` to `f x - g x`.  -/
ZeroHom.instSub : {M : Type u_2} → {N : Type u_3} → [inst : Zero M] → [inst_1 : SubtractionMonoid N] → Sub (ZeroHom M N)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.one.sizeOf_spec : sizeOf FirstOrder.ringFunc.one = 1
-- Init.Data.Bool
Bool.and_not_self : ∀ (x : Bool), (x && !x) = false
-- Mathlib.NumberTheory.Real.Irrational
not_irrational_zero : ¬Irrational 0
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId : ∀ {M S : AlgebraicGeometry.Scheme} [inst : M.Over S],
  AlgebraicGeometry.Scheme.Hom.IsOver (CategoryTheory.Limits.pullback.fst (M ↘ S) (CategoryTheory.CategoryStruct.id S))
    S
-- Init.Data.List.Control
List.forIn'_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : (a : α) → a ∈ [] → β → m (ForInStep β)}
  {b : β}, forIn' [] b f = pure b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorHom_left_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X S U : C} {R T : CategoryTheory.Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ CategoryTheory.Over.mk fS)
  (g : T ⟶ CategoryTheory.Over.mk fU) {Z : C} (h : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd fS fU) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left g) h)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.instIteratorLoopAssocListIteratorIdSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {m : Type (max u v) → Type w''} →
      [Monad m] → Std.IteratorLoop (Std.DHashMap.Internal.AssocList.AssocListIterator α β) Id m
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (property : [].length = 0),
  List.MergeSort.Internal.mergeSortTR.run✝ le ⟨[], property⟩ = []
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_le_abs_eval_T_real : ∀ (n : ℤ) {x : ℝ}, 1 ≤ |x| → 1 ≤ |Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)|
-- Mathlib.Algebra.Group.Pi.Units
AddEquiv.val_neg_piAddUnits_symm_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] (f : (i : ι) → AddUnits (M i)) (x : ι),
  ↑(-AddEquiv.piAddUnits.symm f) x = (f x).neg
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_3.eq_3 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m γ] (it₂ : Std.IterM m γ)
  (motive : it₂.Step → Sort u_3) (h : it₂.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₂' : Std.IterM m γ) →
      (out : γ) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m γ) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_7.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3)
  (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr => h_2 rs k v l_1 r hrb hlr) =
    h_1 hrb hlr
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- A morphism of ring objects.  -/
CategoryTheory.RingObjCat.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.RingObjCat C → CategoryTheory.RingObjCat C → Type v
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Integrable.integral_norm_condKernel : ∀ {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_4 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → F},
  MeasureTheory.Integrable f ρ → MeasureTheory.Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
-- Std.Http.Internal.Char
/-- qdtext = HTAB / SP / %x21 / %x23-5B / %x5D-7E
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.qdtext : Char → Bool
-- Init.Grind.Lemmas
Lean.Grind.Nat.xor_congr : ∀ {a b k₁ k₂ k : ℕ}, a = k₁ → b = k₂ → (k == k₁ ^^^ k₂) = true → a ^^^ b = k
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.lift.congr_simp : ∀ {R : Type u} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal S}
  {M : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (f f_1 : ↥I →ₗ[R] M) (e_f : f = f_1)
  (hf : ∀ (x y : ↥I), f (x * y) = 0), Ideal.Cotangent.lift f hf = Ideal.Cotangent.lift f_1 ⋯
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
/-- The type of closed subgroups of a topological group.  -/
ClosedSubgroup : (G : Type u) → [Group G] → [TopologicalSpace G] → Type u
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.mul : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : LinearOrder α] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring R] {M N : Matrix m m R},
  M.BlockTriangular b → N.BlockTriangular b → (M * N).BlockTriangular b
-- Init.Data.Hashable
instHashableUInt8 : Hashable UInt8
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_one_iff : ∀ {α : Type u} [inst : Preorder α], Order.cof α = 1 ↔ ∃ x, IsTop x
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The module topology, for a module `A` over a topological ring `R`. It's the finest topology
making addition and the `R`-action continuous, or equivalently the finest topology making `A`
into a topological `R`-module. More precisely it's the Inf of the set of
topologies with these properties; theorems `continuousSMul` and `continuousAdd` show
that the module topology also has these properties.  -/
moduleTopology : (R : Type u_1) → [TopologicalSpace R] → (A : Type u_2) → [Add A] → [SMul R A] → TopologicalSpace A
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.quasiIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] ⦃X Y : CochainComplex.Plus C⦄ (x x_1 : X ⟶ Y),
  x = x_1 → CochainComplex.Plus.quasiIso C x = CochainComplex.Plus.quasiIso C x_1
-- Lean.Data.KVMap
Lean.instReprKVMap : Repr Lean.KVMap
-- Init.Data.String.Defs
/-- The underlying byte offset of the `Slice.Pos`.  -/
String.Slice.Pos.offset : {s : String.Slice} → s.Pos → String.Pos.Raw
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_toMultiplicative_apply : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Add M] (x : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.toMultiplicative R M) x).coeff = Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_surjective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → Function.Surjective (AddSubmonoid.comap f)
-- Mathlib.Data.Nat.Count
Nat.count_eq_card_filter_range : ∀ (p : ℕ → Prop) [inst : DecidablePred p] (n : ℕ), Nat.count p n = {x ∈ Finset.range n | p x}.card
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  {X_1 Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y} (g : X_1 ⟶ Y_1),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).map g).left.left =
    CategoryTheory.Over.Hom.left g.left
-- Mathlib.Data.Fin.Fin2
Fin2.toFin_fs : ∀ {n : ℕ} (i : Fin2 n), i.fs.toFin = i.toFin.succ
-- Mathlib.Order.Filter.Pi
Filter.NeBot.coprodᵢ : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} [∀ (i : ι), Nonempty (α i)] {i : ι},
  (f i).NeBot → (Filter.coprodᵢ f).NeBot
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.mk.inj : ∀ {R : Type u_1} {inst : PartialOrder R} {inst_1 : Semiring R} {inst_2 : IsStrictOrderedRing R} {X : Type u_2}
  {Y : Type u_3} {inst_3 : Convexity.ConvexSpace R X} {inst_4 : Convexity.ConvexSpace R Y} {toFun : X → Y}
  {isAffineMap_toFun :
    autoParam (Convexity.IsAffineMap R toFun) Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam}
  {toFun_1 : X → Y}
  {isAffineMap_toFun_1 :
    autoParam (Convexity.IsAffineMap R toFun_1) Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam},
  { toFun := toFun, isAffineMap_toFun := isAffineMap_toFun } =
      { toFun := toFun_1, isAffineMap_toFun := isAffineMap_toFun_1 } →
    toFun = toFun_1
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_injOn : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (S : Set α) {f : α → β},
  Set.InjOn f S → Set.InjOn (Finsupp.mapDomain f) {w | ↑w.support ⊆ S}
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_obj : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)),
  (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C).obj P =
    CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.termS_ : Lean.ParserDescr
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMin'.match_1.splitter : {α : Type u_1} →
  (motive : α × Ordnode α → Sort u_2) → (x : α × Ordnode α) → ((xm : α) → (l' : Ordnode α) → motive (xm, l')) → motive x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Finset`. See
note [pointwise nat action].  -/
Finset.nsmul : {α : Type u_2} → [DecidableEq α] → [Zero α] → [Add α] → SMul ℕ (Finset α)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
MulPosReflectLE.toMulPosReflectLT : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α] [MulPosReflectLE α], MulPosReflectLT α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.trivial_addMon_add : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Init.Data.BitVec.Lemmas
BitVec.intMin_sle : ∀ {w : ℕ} (x : BitVec w), (BitVec.intMin w).sle x = true
-- Std.Time.Format
/-- The Lean Date format, which follows the pattern `uuuu-MM-dd`. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDate : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp_apply : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom
        (groupHomology.mapCycles₂ (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ))))
      x =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ g ψ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` and `y` are both separable elements, then `x - y` is also a separable element.  -/
Field.isSeparable_sub : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
  IsSeparable F x → IsSeparable F y → IsSeparable F (x - y)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
        (𝒰.f i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
        ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j))
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_range : ∀ {G : Type u_3} [inst : AddGroup G] {G' : Type u_5} [inst_1 : AddGroup G'] [AddGroup.FG G] (f : G →+ G'),
  AddGroup.FG ↥f.range
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- The n-ary version of `Set.mem_add`.  -/
Set.mem_finsetSum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (a : α),
  a ∈ ∑ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∑ i ∈ t, g i = a
-- Mathlib.Order.GameAdd
/-- The `Prod.GameAdd` relation on well-founded inputs is well-founded.

In particular, the sum of two well-founded games is well-founded.  -/
WellFounded.prod_gameAdd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop},
  WellFounded rα → WellFounded rβ → WellFounded (Prod.GameAdd rα rβ)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mul_inv' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (u : G₀ˣ), ↑u * (↑u)⁻¹ = 1
-- Mathlib.Order.SupIndep
/-- If the elements of a set are independent, then any element is disjoint from the `sSup` of some
subset of the rest.  -/
sSupIndep.disjoint_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α},
  sSupIndep s → ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → x ∉ y → Disjoint x (sSup y)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_one : ↑1 = 1
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_left_closedEBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal),
  (fun x => a * x) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (a⁻¹ * b) r
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPProofsThreshold : Lean.Options → ℕ
-- Init.Meta.Defs
/-- The transparency mode to use for unfolding  -/
Lean.Meta.Rewrite.Config.transparency : Lean.Meta.Rewrite.Config → Lean.Meta.TransparencyMode
-- Mathlib.Data.Set.Countable
Set.countable_isTop : ∀ (α : Type u_1) [inst : PartialOrder α], {x | IsTop x}.Countable
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_himp_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α}, (⨆ x, f x) ⇨ a = ⨅ x, f x ⇨ a
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  [LawfulMonad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x} {it : Std.IterM m β}
  {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b}
  (PlausibleForInStep : β → γ → ForInStep γ → Prop)
  {f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))},
  Std.IteratorLoop.WellFounded α m PlausibleForInStep →
    Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
      (fun x => lift (Std.Shrink it.Step) γ x it.step) fun s =>
        match s.inflate with
        | ⟨Std.IterStep.yield it' out, h⟩ => do
          let __do_lift ← f out ⋯ init
          match __do_lift with
            | ⟨ForInStep.yield c, property⟩ => Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it' c P ⋯ f
            | ⟨ForInStep.done c, property⟩ => pure c
        | ⟨Std.IterStep.skip it', h⟩ => Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it' init P ⋯ f
        | ⟨Std.IterStep.done, property⟩ => pure init