mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.not_isBase_of_ssubset : ∀ {α : Type u_1} {M : Matroid α} {B X : Set α}, M.IsBase B → X ⊂ B → ¬M.IsBase X
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if the product of `X` and `Y` exists, then the
binary biproduct of `X` and `Y` exists.  -/
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
  [CategoryTheory.Limits.HasBinaryProduct X Y], CategoryTheory.Limits.HasBinaryBiproduct X Y
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_iff_exists_monotone_subseq : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsPreorder α r],
  s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
-- Mathlib.ModelTheory.Order
/-- This is not an instance because it would form a loop with
`FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass`.
As both types are `Prop`s, it would only cause a slowdown.  -/
FirstOrder.Language.StrongHomClass.toOrderIsoClass : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered] (M : Type u_1) [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] (N : Type u_2) [inst_4 : L.Structure N] [inst_5 : LE N] [L.OrderedStructure N] (F : Type u_3)
  [inst : EquivLike F M N] [L.StrongHomClass F M N], OrderIsoClass F M N
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Odd Hurwitz zeta kernel (function whose Mellin transform will be the odd part of the completed
Hurwitz zeta function). See `oddKernel_def` for the defining formula, and `hasSum_int_oddKernel`
for an expression as a sum over `ℤ`.
 -/
HurwitzZeta.oddKernel : UnitAddCircle → ℝ → ℝ
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `HasMFDerivWithinAt` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabHasMFDerivWithinAt : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- The characteristic `p` version of `peval_polyOfInterest`  -/
WittVector.peval_polyOfInterest' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] (n : ℕ) (x y : WittVector p k),
  WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- A submonoid `H` of `M` determines a submonoid `H.op` of the opposite monoid `Mᵐᵒᵖ`.  -/
Submonoid.opEquiv : {M : Type u_2} → [inst : MulOneClass M] → Submonoid M ≃o Submonoid Mᵐᵒᵖ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.instBoundedContinuousMapClass : ∀ (B : Type u_6) {E : outParam (Type u_7)} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (Ω : outParam (TopologicalSpace.Opens E)) (F : outParam (Type u_8)) [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (n : outParam ℕ∞) [inst_4 : TestFunctionClass B Ω F n], BoundedContinuousMapClass B E F
-- Mathlib.FieldTheory.IsSepClosed
/-- If `k` is perfect, `K` is a separable closure of `k`,
then it is also an algebraic closure of `k`.  -/
IsSepClosure.isAlgClosure_of_perfectField : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra k K] [IsSepClosure k K]
  [PerfectField k], IsAlgClosure k K
-- Lean.Parser.Extension
Lean.Parser.declareTrailingBuiltinParser : Lean.Name → Lean.Name → ℕ → Lean.CoreM Unit
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.Functor.hasLiftingProperty_iff_of_isEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (G : CategoryTheory.Functor C D) [G.IsEquivalence] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y),
  CategoryTheory.HasLiftingProperty (G.map i) (G.map p) ↔ CategoryTheory.HasLiftingProperty i p
-- Mathlib.CategoryTheory.Action.Basic
/-- A fully faithful functor between categories induces a fully faithful functor between
the categories of `G`-actions within those categories.  -/
CategoryTheory.Functor.FullyFaithful.mapAction : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} W] →
        {F : CategoryTheory.Functor V W} →
          F.FullyFaithful → (G : Type u_3) → [inst_2 : Monoid G] → (F.mapAction G).FullyFaithful
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V} [inst_5 : SizeOf C]
  [inst_6 : SizeOf V] (π : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))
  (hπ :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))))
  (isLimitWedge : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π c) ⋯))
  (map_comp_π :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π c' j) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))),
  sizeOf { π := π, hπ := hπ, isLimitWedge := isLimitWedge, map_comp_π := map_comp_π } = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The identity `image f ⟶ image f` fits into the commutative square represented by the identity
morphism `𝟙 f` in the arrow category.  -/
CategoryTheory.Limits.imageMapId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (f : CategoryTheory.Arrow C) →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.id f)
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.instAppendTreeMap_mathlib : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → [Append β] → Append (Std.TreeMap α β cmp)
-- Mathlib.Control.Fold
Monoid.foldrM.mk.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α : Type u} (f : α → m α), Monoid.foldrM.mk f = f
-- Lean.Server.GoTo
Lean.Server.GoToKind.determineTargetExprs : Lean.Server.GoToKind → Lean.Elab.TermInfo → Lean.MetaM (Array Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
      (CategoryTheory.Limits.pullback.snd f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- If `F` preserves a binary biproduct, we get a definitionally nice isomorphism
`F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y`.  -/
CategoryTheory.Functor.mapBiprod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              (X Y : C) →
                [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
                  [inst_5 : F.PreservesZeroMorphisms] →
                    [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] → F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.nhds_zero_eq_map_structureMap : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Zero (R i)]
  [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (R i)],
  (∀ (i : ι), IsOpen ↑(B i)) →
    nhds (RestrictedProduct.structureMap R (fun i => ↑(B i)) Filter.cofinite 0) =
      Filter.map (RestrictedProduct.structureMap R (fun i => ↑(B i)) Filter.cofinite) (nhds 0)
-- Mathlib.Control.Applicative
Functor.Comp.pure_seq_eq_map : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α β : Type v} (f : α → β) (x : Functor.Comp F G α), pure f <*> x = f <$> x
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.interior.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], ModelWithCorners.interior M = {x | I.IsInteriorPoint x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.ext_iff : ∀ {R : Type u} {x y : WeierstrassCurve R}, x = y ↔ x.a₁ = y.a₁ ∧ x.a₂ = y.a₂ ∧ x.a₃ = y.a₃ ∧ x.a₄ = y.a₄ ∧ x.a₆ = y.a₆
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_zero_apply : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (m : ↑M₁.toModuleCat),
  (TopModuleCat.Hom.hom 0) m = 0
-- Mathlib.Algebra.Group.ULift
/-- The multiplicative equivalence between `ULift α` and `α`.
 -/
MulEquiv.ulift : {α : Type u} → [inst : Mul α] → ULift.{u_1, u} α ≃* α
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The set of points in a simplex constructed with `mkOfPoint`.  -/
Affine.Simplex.range_mkOfPoint_points : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), Set.range (Affine.Simplex.mkOfPoint k p).points = {p}
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.eq_bot_iff : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [NeZero 2] [inst_4 : Module K M] [inst_5 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  (q : ↥P.invtRootSubmodule), q = ⊥ ↔ ∀ (i : ι), P.root i ∉ ↑q
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that checks if the attribute was already applied  -/
Mathlib.Tactic.Translate.linter.translateOverwrite : Lean.Option Bool
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.mk.sizeOf_spec : ∀ {P : TopCat → Prop} [inst : (a : TopCat) → SizeOf (P a)] (toTop : TopCat) [is_compact : CompactSpace ↑toTop]
  [is_hausdorff : T2Space ↑toTop] (prop : P toTop),
  sizeOf { toTop := toTop, is_compact := is_compact, is_hausdorff := is_hausdorff, prop := prop } =
    1 + sizeOf toTop + sizeOf is_compact + sizeOf is_hausdorff + sizeOf prop
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.coeff_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T) {n : ℕ},
  ↑((p.toSubring T hp).coeff n) = p.coeff n
-- Mathlib.NumberTheory.LucasPrimality
/-- If `a^(p-1) = 1 mod p`, but `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`, then `p`
is prime. This is true because `a` has order `p-1` in the multiplicative group mod `p`, so this
group must itself have order `p-1`, which only happens when `p` is prime.
 -/
lucas_primality : ∀ (p : ℕ) (a : ZMod p), a ^ (p - 1) = 1 → (∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1) → Nat.Prime p
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
/-- Given `P : ObjectProperty C` and a family of categories `J : α → Type _`,
this property of objects contains `P` and all objects that are equal to `lim F`
for some functor `F : J a ⥤ C` such that `F.obj j` satisfies `P` for any `j`.  -/
CategoryTheory.ObjectProperty.strictLimitsClosureStep : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      {α : Type t} →
        (J : α → Type u') → [(a : α) → CategoryTheory.Category.{v', u'} (J a)] → CategoryTheory.ObjectProperty C
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_right : ∀ {aig : Std.Sat.AIG ℕ} {new1 : ℕ} {hnew1 : new1 < aig.decls.size} {new2 : ℕ} {hnew2 : new2 < aig.decls.size}
  (state1 state2 state3 : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1 state2 new1 hnew1 →
    Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state2 state3 new2 hnew2 →
      Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state1 state3 new2 hnew2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' fallback : α}
  {f : Option β → Option β},
  (t.alter k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.baseChange_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {S S' : C} (f : S' ⟶ S)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] (X : CategoryTheory.Over S),
  P X.hom → P ((CategoryTheory.Over.pullback f).obj X).hom
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul_inv_cancel : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M}, x.fst ≠ 0 → x * x⁻¹ = 1
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqExpect : BEq Std.Http.Header.Expect
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.linearMapPi_apply : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)] (S : Type u_1)
  [inst_5 : Semiring S] [inst_6 : (i : ι) → Module S (φ i)] [inst_7 : ∀ (i : ι), SMulCommClass R S (φ i)]
  (f : (i : ι) → M₂ →ₗ[R] φ i), (LinearEquiv.linearMapPi S) f = LinearMap.pi f
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂.eq_1 : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (p : MvPolynomial σ R), MvPolynomial.eval₂ f g p = p.coeff.sum fun s a => f a * s.prod fun n e => g n ^ e
-- Mathlib.FieldTheory.Finite.Basic
ZMod.pow_card_sub_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (a : ZMod p), a ^ (p - 1) = if a ≠ 0 then 1 else 0
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.memLp_dual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (L : StrongDual ℝ E) (p : ENNReal),
  p ≠ ⊤ → MeasureTheory.MemLp (⇑L) p μ
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.module : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : ContinuousAdd M] → [inst_5 : Module R M] → [ContinuousConstSMul R M] → Module R C(α, M)
-- Mathlib.Topology.Order.LocalExtr
isLocalMaxOn_univ_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalMaxOn f Set.univ a ↔ IsLocalMax f a
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.cons_of_le : ∀ {n m : ℕ} (a : ℕ) {b : ℕ} {l : List ℕ},
  Mathlib.Meta.NormNum.IsNat (b * m) n →
    a ≤ b → b.minFac = b → Mathlib.Meta.Simproc.FactorsHelper m b l → Mathlib.Meta.Simproc.FactorsHelper n a (b :: l)
-- Mathlib.Order.Filter.IsBounded
isCoboundedUnder_le_finset_sup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
  (hs : s.Nonempty),
  (∃ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
-- Batteries.Recycling.RBTree.Lemmas
/-- If `cut = x`, then `cut` and `x` have compare the same with respect to other elements.  -/
RBTree.RBNode.IsStrictCut.exact : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [self : RBTree.RBNode.IsStrictCut cmp cut] {x y : α}
  [Std.TransCmp cmp], cut x = Ordering.eq → cmp x y = cut y
-- Mathlib.Data.Num.Bitwise
/-- The `head` of a `SNum` is the Boolean value of its LSB.  -/
SNum.head : SNum → Bool
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.stabilizer_quotient : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), AddAction.stabilizer G ↑0 = H
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofSupport.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} (l : List V) (hne : l ≠ []) (hchain : List.IsChain G.Adj l),
  SimpleGraph.Walk.ofSupport l hne hchain = SimpleGraph.Walk.ofSupport l hne hchain
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C),
  (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `LinearEquiv.symm` defines an equivalence between `α ≃ₛₗ[σ] β` and `β ≃ₛₗ[σ] α`.  -/
LinearEquiv.symmEquiv : {R : Type u_1} →
  {S : Type u_6} →
    {M : Type u_7} →
      {M₂ : Type u_9} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_S_M₂ : Module S M₂} →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        {re₁ : RingHomInvPair σ σ'} → {re₂ : RingHomInvPair σ' σ} → (M ≃ₛₗ[σ] M₂) ≃ M₂ ≃ₛₗ[σ'] M
-- Mathlib.Tactic.Have
Mathlib.Tactic.optBinderIdent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Computability.EpsilonNFA
/-- The `εClosure` of a set is the set of states which can be reached by taking a finite string of
ε-transitions from an element of the set.  -/
εNFA.εClosure : {α : Type u} → {σ : Type v} → εNFA α σ → Set σ → Set σ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.Topology.Category.TopCommRingCat
/-- A bundled topological commutative ring.  -/
TopCommRingCat : Type (u + 1)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.bot_prod_bot : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N], ⊥.prod ⊥ = ⊥
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.single_target : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b : β), (PartialEquiv.single a b).target = {b}
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_of_le_mul' : ∀ {a b c : ENNReal}, a ≤ b * c → a / b ≤ c
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.isOpen_cylinder : ∀ (E : ℕ → Type u_1) [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] (x : (n : ℕ) → E n)
  (n : ℕ), IsOpen (PiNat.cylinder x n)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Translate a normal instruction. For the `write` command, we use a `goto` indirection so that
we can access the current value of the tape.  -/
Turing.TM1to1.trNormal : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      {n : ℕ} → (List.Vector Bool n → Γ) → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.Context : Type
-- Mathlib.Order.Interval.Finset.Basic
Finset.notMem_Ioi_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] {b : α}, b ∉ Finset.Ioi b
-- Mathlib.Order.Minimal
maximal_mem_image_antitone : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) → Maximal (fun x => x ∈ s) x → Minimal (fun x => x ∈ f '' s) (f x)
-- Init.Data.UInt.Lemmas
UInt16.neg_eq_neg_one_mul : ∀ (a : UInt16), -a = -1 * a
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_hasFDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : F →L[𝕜] G},
  HasFDerivAt (f ∘ ⇑iso) (f' ∘SL ↑iso) x ↔ HasFDerivAt f f' (iso x)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Auxiliary construction for `desc`.  -/
CategoryTheory.InjectiveResolution.descFOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (Z ⟶ Y) →
          (I : CategoryTheory.InjectiveResolution Y) →
            (J : CategoryTheory.InjectiveResolution Z) → J.cocomplex.X 1 ⟶ I.cocomplex.X 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_diff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, (m₁.diff m₂ ⋯).get? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else m₁.get? k
-- Std.Http.Internal.String
/-- Core character quoting used by `quoteHttpString`.

Emits `qdtext` characters directly and `"` / `\\` as `quoted-pair`.
The proof `h₀ : quotedStringChar c` guarantees the impossible branch is unreachable.
 -/
Std.Http.Internal.quoteCore : (c : Char) → Std.Http.Internal.Char.quotedStringChar c = true → String
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.isAtom_findAtom_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] {r : α}, IsAtom (IsPredArchimedean.findAtom r) ↔ r ≠ ⊥
-- Mathlib.Topology.Inseparable
subtype_inseparable_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop} (x y : Subtype p), Inseparable x y ↔ Inseparable ↑x ↑y
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_subtype_coe : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, Measurable Subtype.val