mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- A matrix `A` is primitive if it is entrywise nonnegative
and some positive power has all entries strictly positive.  -/
Matrix.IsPrimitive : {n : Type u_1} → {R : Type u_2} → [Ring R] → [LinearOrder R] → [Fintype n] → [DecidableEq n] → Matrix n n R → Prop
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} (x : CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))),
  ∃ S y, x = CategoryTheory.GrothendieckTopology.Plus.mk y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare ((Std.DTreeMap.Internal.Impl.insert! k v t).minKeyD fallback) k).isLE = true
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
isClosedMap_iff_upperHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsClosedMap f ↔ UpperHemicontinuous fun x => f ⁻¹' {x}
-- Lean.Parser.Extension
Lean.Parser.addTrailingParser : Lean.Parser.ParserCategories →
  Lean.Name → Lean.Name → Lean.Parser.TrailingParser → ℕ → Except String Lean.Parser.ParserCategories
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_right_comm`.  -/
Option.map_map₂_distrib_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {β' : Type u_6} {g : γ → δ} {f' : α → β' → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' a (g' b)) → Option.map g (Option.map₂ f a b) = Option.map₂ f' a (Option.map g' b)
-- Mathlib.Algebra.Free
FreeMagma.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β), FreeMagma.map f = FreeMagma.lift (FreeMagma.of ∘ f)
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
_private.Mathlib.MeasureTheory.Measure.Haar.Quotient.0.termπ_2 : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.le_def : ∀ {X : SSet} {s t : X.S}, s ≤ t ↔ s.subcomplex ≤ t.subcomplex
-- Mathlib.Topology.Compactness.Lindelof
instLindelofSpaceSigmaOfCountable : ∀ {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), LindelofSpace (X i)], LindelofSpace ((i : ι) × X i)
-- Lean.Parser.Basic
Lean.Parser.nodeInfo : Lean.SyntaxNodeKind → Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.supp_inj : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C D : G.ComponentCompl K}, C.supp = D.supp ↔ C = D
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.instStarMulId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → StarMul (E →ₗ[𝕜] E)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] [inst_1 : Inhabited α]
  {k : α}, m.contains k = true → m.get! k = k
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.Abelian.instIsStableUnderCobaseChangeMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderCobaseChange
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag.eq_1 : ∀ (n : ℕ),
  (Int.ofNat n).divisorsAntidiag =
    (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion
      (Finset.map
        ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap
          (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
        n.divisorsAntidiagonal)
      ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.instMeasurableConstSMul : ∀ {M : Type u_2} {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableConstSMul M (α i)],
  MeasurableConstSMul M ((i : ι) → α i)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofRepr.inj : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  {repr repr_1 : M ≃ₗ[R] ι →₀ R}, { repr := repr } = { repr := repr_1 } → repr = repr_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj ⋯) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuous_sin : Continuous Real.sin
-- Batteries.Data.List.Perm
List.Subperm.diff_right : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁.Subperm l₂ → ∀ (t : List α), (l₁.diff t).Subperm (l₂.diff t)
-- Mathlib.Data.Setoid.Partition
IndexedPartition.mk : {ι : Type u_1} →
  {α : Type u_2} →
    {s : ι → Set α} →
      (∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j) →
        (some : ι → α) → (∀ (i : ι), some i ∈ s i) → (index : α → ι) → (∀ (x : α), x ∈ s (index x)) → IndexedPartition s
-- Lean.Data.Lsp.Internal
/-- Whether this `decl` matched the query exactly.  -/
Lean.Lsp.LeanIdentifier.isExactMatch : Lean.Lsp.LeanIdentifier → Bool
-- Mathlib.Analysis.InnerProductSpace.Completion
Inseparable.inner_eq_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x₁ x₂ y₁ y₂ : E}, Inseparable x₁ x₂ → Inseparable y₁ y₂ → inner 𝕜 x₁ y₁ = inner 𝕜 x₂ y₂
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderAddMonoidHom_bijective : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] [Nontrivial G], Function.Bijective ⇑(LocallyFiniteOrder.orderAddMonoidHom G)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] (Ω Ω_1 : C),
  Ω = Ω_1 → CategoryTheory.SubobjectRepresentableBy Ω = CategoryTheory.SubobjectRepresentableBy Ω_1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapSnd_inv_app : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} A']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'}
  {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'}
  (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.mapSnd β α).inv.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position several bytes back.

If asked to go back more bytes than available, stops at the beginning of the array.
 -/
ByteArray.Iterator.prevn : ByteArray.Iterator → ℕ → ByteArray.Iterator
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ProbabilityTheory.IsSFiniteKernel κ] [∀ (a : α), NeZero (κ a)],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd κ) ↔ μ.AbsolutelyContinuous ν
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.isSuccLimit : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Order.IsSuccLimit c
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.toSubsemiring_le_toSubsemiring : ∀ {R : Type u_1} [inst : CommRing R] {P₁ P₂ : RingPreordering R}, ↑P₁ ≤ ↑P₂ ↔ P₁ ≤ P₂
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_prod : ∀ {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)}
  [inst : Γ.HasDetPlusMinusOne] (F : (i : ι) → ModularForm Γ (k i)), ⇑(ModularForm.prod m hm F) = ∏ i ∈ s, ⇑(F i)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.right_le_sup : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F)
  (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y), g ≤ f.sup g h
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk : ∀ {R : CommRingCat} (M : ModuleCat ↑R) (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)),
  IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (AlgebraicGeometry.tilde.toStalk M x))
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.coe_compl : ∀ {R : Type u_1} [inst : NonAssocRing R] (a : { a // IsIdempotentElem a }), ↑aᶜ = 1 - ↑a
-- Mathlib.Algebra.Algebra.Pi
/-- When `R` is commutative and permits an `algebraMap`, `Pi.constRingHom` is equal to that
map.  -/
Pi.constRingHom_eq_algebraMap : ∀ (R : Type u_2) [inst : CommSemiring R] (A : Type u_5), Pi.constRingHom A R = algebraMap R (A → R)
-- Aesop.EMap
Aesop.EMap.empty : {α : Type u_1} → Aesop.EMap α
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.PiInjective.sampleableExt : Plausible.SampleableExt { f // Function.Injective f }
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {E' : Type u_3} {inst_3 : NormedAddCommGroup E'} {inst_4 : NormedSpace 𝕜 E'} {H : Type u_5}
  {inst_5 : TopologicalSpace H} {H' : Type u_6} {inst_6 : TopologicalSpace H'} {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} {inst_7 : TopologicalSpace M} {inst_8 : ChartedSpace H M}
  {M' : Type u_10} {inst_9 : TopologicalSpace M'} {inst_10 : ChartedSpace H' M'} {n : WithTop ℕ∞} {toEquiv : M ≃ M'}
  {contMDiff_toFun : ContMDiff I I' n ⇑toEquiv} {contMDiff_invFun : ContMDiff I' I n ⇑toEquiv.symm} {toEquiv_1 : M ≃ M'}
  {contMDiff_toFun_1 : ContMDiff I I' n ⇑toEquiv_1} {contMDiff_invFun_1 : ContMDiff I' I n ⇑toEquiv_1.symm},
  { toEquiv := toEquiv, contMDiff_toFun := contMDiff_toFun, contMDiff_invFun := contMDiff_invFun } =
      { toEquiv := toEquiv_1, contMDiff_toFun := contMDiff_toFun_1, contMDiff_invFun := contMDiff_invFun_1 } →
    toEquiv = toEquiv_1
-- Init.Tactics
/-- `mleft` is like `left`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
  mintro HP
  mleft
  mexact HP
```
 -/
Lean.Parser.Tactic.mleftMacro : Lean.ParserDescr
-- Lean.Message
Lean.instToMessageDataMVarId : Lean.ToMessageData Lean.MVarId
-- Mathlib.Data.Finsupp.Multiset
Finsupp.coe_orderIsoMultiset : ∀ {ι : Type u_3} [inst : DecidableEq ι], ⇑Finsupp.orderIsoMultiset = ⇑Finsupp.toMultiset
-- Mathlib.Tactic.Linter.TextBased
/-- Find the first style exception in `exceptions` (if any) which covers a style exception `e`.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.find?_comparable : Mathlib.Linter.TextBased.ErrorContext✝ →
  Array Mathlib.Linter.TextBased.ErrorContext✝ → Option Mathlib.Linter.TextBased.ErrorContext✝
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsAffineXSchemeCover : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.AffineCover P S) (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.cover.X i)
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sq_le_one : ∀ (x : ℝ), Real.sin x ^ 2 ≤ 1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instAddCommGroupHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → AddCommGroup (T₁ ⟶ T₂)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (base : 𝒮)
  (fiber : ↑(F.obj { as := Opposite.op base })) (base_1 : 𝒮) (fiber_1 : ↑(F.obj { as := Opposite.op base_1 })),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Mathlib.Data.Multiset.FinsetOps
/-- `ndunion s t` is the lift of the list `union` operation. This operation
does not respect multiplicities, unlike `s ∪ t`, but it is suitable as
a union operation on `Finset`. (`s ∪ t` would also work as a union operation
on finset, but this is more efficient.)  -/
Multiset.ndunion : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α → Multiset α
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι},
  UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => -f n.1 z + f n.2 z) 0 (l ×ˢ l) s
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.isMonoidalDistrib.of_symmetric_monoidal_closed : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.SymmetricCategory C]
  [CategoryTheory.MonoidalClosed C], CategoryTheory.IsMonoidalDistrib C
-- Mathlib.Data.List.Forall2
List.forall₂_drop_append : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : List α) (l₁ l₂ : List β),
  List.Forall₂ R l (l₁ ++ l₂) → List.Forall₂ R (List.drop l₁.length l) l₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (k c : ℕ),
  p.powC k c =
    match k with
    | 0 => Lean.Grind.CommRing.Poly.num 1
    | 1 => p
    | k.succ => p.mulC (p.powC k c) c
-- Mathlib.Data.List.NodupEquivFin
/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
an equivalence between `Fin l.length` and `α`.

See `List.Nodup.getBijectionOfForallMemList` for a version without decidable equality.  -/
List.Nodup.getEquivOfForallMemList : {α : Type u_1} → [DecidableEq α] → (l : List α) → l.Nodup → (∀ (x : α), x ∈ l) → Fin l.length ≃ α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Rci α → Std.DTreeMap.Internal.Unit.RciSliceData α
-- Mathlib.Combinatorics.Quiver.Path
/-- A bounded path is a path with a uniform bound on its length.  -/
Quiver.Path.BoundedPaths : {V : Type u_1} → [Quiver V] → V → V → ℕ → Type (max 0 u_1 u_2)
-- Mathlib.Topology.Bases
TopologicalSpace.countable_cover_nhdsWithin : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α} {s : Set α},
  (∀ x ∈ s, f x ∈ nhdsWithin x s) → ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
-- Mathlib.Data.Multiset.Powerset
Multiset.revzip_powersetAux_lemma : ∀ {α : Type u_2} [inst : DecidableEq α] (l : List α) {l' : List (Multiset α)},
  (∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l) → l'.revzip = List.map (fun x => (x, ↑l - x)) l'
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.instMonoidalCategoryStruct : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategoryStruct (AlgCat R)
-- Init.Data.Int.DivMod.Lemmas
Int.emod_neg : ∀ (a b : ℤ), a % -b = a % b
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encode_lt_prec : ∀ (cf cg : Nat.Partrec.Code),
  Encodable.encode cf < Encodable.encode (cf.prec cg) ∧ Encodable.encode cg < Encodable.encode (cf.prec cg)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk'_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  (s : X.Splitting), (CategoryTheory.SimplicialObject.Split.mk' s).X = X
-- Init.Data.String.OrderInstances
String.Slice.Pos.instAntisymmLe : ∀ {s : String.Slice}, Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.SuccPred.Basic
Order.pred_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a b : α),
  Order.pred (min a b) = min (Order.pred a) (Order.pred b)
-- Batteries.Tactic.GeneralizeProofs
/-- Loop for `generalizeProofsCore`.  -/
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.generalizeProofsCore.go : Array Lean.FVarId →
  Array Lean.FVarId →
    Bool → Lean.MVarId → ℕ → Array Lean.Expr → Batteries.Tactic.GeneralizeProofs.MGen (Array Lean.Expr × Lean.MVarId)
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkDiscrs : Lean.Elab.Deriving.Header → Lean.InductiveVal → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchDiscr))
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.norm_pos : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂]
  [Nontrivial E] (e : E ≃SL[σ₁₂] F), 0 < ‖↑e‖
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.vcomp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) (X : C),
  (α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
-- Batteries.Data.AssocList
/-- Split the list into head and tail, if possible.  -/
Batteries.AssocList.pop? : {α : Type u_1} → {β : Type u_2} → Batteries.AssocList α β → Option ((α × β) × Batteries.AssocList α β)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- Let `v` be an `(n + 1)`-tuple with two equal elements `v i = v j`, `i ≠ j`.
Let `w i` (resp., `w j`) be the vector `v` with `i`th (resp., `j`th) element removed.
Then `(-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0`.
This follows from the fact that these two vectors differ by a permutation of sign `(-1) ^ (i + j)`.

These are the only two nonzero terms in the proof of `map_eq_zero_of_eq`
in the definition of `alternatizeUncurryFin` below.  -/
AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n]→ₗ[R] N) {v : Fin (n + 1) → M}
  {i j : Fin (n + 1)}, v i = v j → i ≠ j → (-1) ^ ↑i • f (i.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0
-- Mathlib.Algebra.GroupWithZero.Basic
GroupWithZero.mul_left_injective : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {x : G₀}, x ≠ 0 → Function.Injective fun y => y * x
-- Mathlib.Topology.Compactness.Lindelof
Topology.IsClosedEmbedding.nonLindelofSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NonLindelofSpace X] {f : X → Y},
  Topology.IsClosedEmbedding f → NonLindelofSpace Y
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_eq_of_injOn_lift : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α),
  Set.InjOn f s → Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) = Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_range_comp : ∀ {ι : Type u} {f : ι → Ordinal.{v}},
  BddAbove (Set.range f) → ∀ (g : Ordinal.{v} → Ordinal.{max v w}), BddAbove (Set.range (g ∘ f))
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult : Type
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] (f : α → β) (s : Set α) (a : α),
  IsLocalMinOn f s a = IsMinFilter f (nhdsWithin a s) a
-- Std.Http.Server.Config
/-- Timeout for keep-alive connections
 -/
Std.Http.Config.keepAliveTimeout : Std.Http.Config → { x // x > 0 }
-- Init.WFExtrinsicFix
/-- A fixpoint combinator that can be used to construct recursive functions with an
**extrinsic, partial** proof of termination.

Given a relation `R` and a fixpoint functional `F` which must be decreasing with respect
to `R`, `partialExtrinsicFix R F` is the recursive function obtained by having `F` call
itself recursively.

For each input `a`, `partialExtrinsicFix R F a` can be verified given a **partial** termination
proof. The precise semantics are as follows.

If `Acc R a` does not hold, `partialExtrinsicFix R F a` might run forever. In this case,
nothing interesting can be proved about the recursive function; it is opaque and behaves like a
recursive function with the `partial` modifier.

If `Acc R a` *does* hold, `partialExtrinsicFix R F a` is equivalent to
`F a (fun a' _ => partialExtrinsicFix R F a')`, both logically and regarding its termination behavior.

In particular, if `R` is well-founded, `partialExtrinsicFix R F a` is equivalent to
`WellFounded.fix _ F`.
 -/
WellFounded.partialExtrinsicFix : {α : Sort u_1} →
  {C : α → Sort u_2} →
    [∀ (a : α), Nonempty (C a)] → (R : α → α → Prop) → ((a : α) → ((a' : α) → R a' a → C a') → C a) → (a : α) → C a
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_exp : ∀ (z : ℂ), ‖Complex.exp z‖ = Real.exp z.re
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.iff_of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (e : C ≌ D), CategoryTheory.IsFiltered C ↔ CategoryTheory.IsFiltered D
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsBigO` over an `OpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.isBigO_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : OpenPartialHomeomorph α β) {b : β},
  b ∈ e.target → ∀ {f : β → E} {g : β → F}, f =O[nhds b] g ↔ (f ∘ ↑e) =O[nhds (↑e.symm b)] (g ∘ ↑e)
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimit_iff : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Order.IsPredLimit a ↔ ¬IsMax a ∧ Order.IsPredPrelimit a