mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.Channel
/-- The slot in `buf` that the next send will happen to.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.sendIdx : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → ℕ
-- Mathlib.Data.Int.ModEq
Int.modulus_modEq_zero : ∀ {n : ℤ}, n ≡ 0 [ZMOD n]
-- Mathlib.Order.TypeTags
/-- Recursor for `WithBot` using the preferred forms `⊥` and `↑a`.  -/
WithBot.recBotCoe : {α : Type u_1} → {C : WithBot α → Sort u_2} → C ⊥ → ((a : α) → C ↑a) → (n : WithBot α) → C n
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C],
  CategoryTheory.HasExactLimitsOfShape J D
-- Mathlib.Order.Bounds.Basic
le_of_isLUB_Iio : ∀ {α : Type u_1} [inst : Preorder α] {b : α} (a : α), IsLUB (Set.Iio a) b → b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.lift.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.Limits.equalizer.lift k h = CategoryTheory.Limits.equalizer.lift k_1 ⋯
-- Lean.Level
Lean.Level.PP.Result.maxNode.sizeOf_spec : ∀ (a : List Lean.Level.PP.Result), sizeOf (Lean.Level.PP.Result.maxNode a) = 1 + sizeOf a
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instEpiToRange : ∀ {X Y : SSet} (f : X ⟶ Y), CategoryTheory.Epi (SSet.Subcomplex.toRange f)
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_Ioc : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α),
  Bornology.IsBounded (Set.Ioc a b)
-- Mathlib.Algebra.Group.Int.Units
Int.eq_one_or_neg_one_of_mul_eq_neg_one' : ∀ {u v : ℤ}, u * v = -1 → u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
-- Mathlib.Topology.Category.Stonean.Basic
Profinite.lift.eq_1 : ∀ {X Y : Profinite} {Z : Stonean} (e : Stonean.toProfinite.obj Z ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f],
  Profinite.lift e f = CategoryTheory.Projective.factorThru e f
-- Lean.Meta.Closure
Lean.Meta.Closure.Context.zetaDelta : Lean.Meta.Closure.Context → Bool
-- Mathlib.Topology.Category.Compactum
Compactum.instT2SpaceA : ∀ {X : Compactum}, T2Space X.A
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.mk.inj : ∀ {name : List Lean.Name} {stx selection : Lean.Syntax} {prevSiblings : Array Lean.Lsp.DocumentSymbol}
  {name_1 : List Lean.Name} {stx_1 selection_1 : Lean.Syntax} {prevSiblings_1 : Array Lean.Lsp.DocumentSymbol},
  { name := name, stx := stx, selection := selection, prevSiblings := prevSiblings } =
      { name := name_1, stx := stx_1, selection := selection_1, prevSiblings := prevSiblings_1 } →
    name = name_1 ∧ stx = stx_1 ∧ selection = selection_1 ∧ prevSiblings = prevSiblings_1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isCompact_isOpen_iff_ideal : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (PrimeSpectrum.zeroLocus ↑I)ᶜ = s
-- Mathlib.Analysis.Normed.Group.Real
enorm_norm' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (x : E), ‖‖x‖‖ₑ = ‖x‖ₑ
-- Lean.Elab.Do.ForwardSyntax
/-- A body that effect-forwards into the enclosing `do` block via a `do←` marker, captured from
syntax of the form `do← body` or `fun b₁ … bₖ => do← body`. `binders` is empty in the bare
form.
 -/
Lean.Elab.Do.ForwardArg : Type
-- Std.Sync.Notify
/-- Notify all currently waiting consumers.
 -/
Std.Notify.notify : Std.Notify → BaseIO Unit
-- Mathlib.Computability.StateTransition
StateTransition.mem_eval : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, b ∈ StateTransition.eval f a ↔ StateTransition.Reaches f a b ∧ f b = none
-- Mathlib.Data.Set.Image
Set.insert_none_range_some : ∀ (α : Type u_5), insert none (Set.range some) = Set.univ
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_1.eq_1 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_1 ()
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_2 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (el : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.error el s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_2 el s'
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `comp p q` is the composition of `p : R[X]` and `q : M[X]` as `q(p(x))`.  -/
PolynomialModule.comp : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Polynomial R → PolynomialModule R M →ₗ[R] PolynomialModule R M
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertMany : {α : Type u} →
  {β : α → Type v} →
    {ρ : Type w} →
      [ForIn Id ρ ((a : α) × β a)] →
        [inst : BEq α] →
          [inst_1 : Hashable α] →
            (m : Std.DHashMap.Internal.Raw₀ α β) →
              ρ →
                { m' //
                  ∀ (P : Std.DHashMap.Internal.Raw₀ α β → Prop),
                    (∀ {m'' : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) →
                      P m → P m' }
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.instMonoid : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → Monoid (P →ᵃⁱ[𝕜] P)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A version of `cellFrontier_subset_finite_closedCell` using open cells: The boundary of a cell is
contained in a finite union of open cells of a lower dimension.  -/
Topology.CWComplex.cellFrontier_subset_finite_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.openCell m j
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesRightHomologyOf S₁] [inst_10 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso' F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv
      (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_zero_iff_of_orderTop : ∀ {α : Type u_3} [inst : PartialOrder α] [OrderTop α], Order.krullDim α = 0 ↔ Subsingleton α
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationHSMul : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup V]
  {μ : MeasureTheory.VectorMeasure X V} {𝕜 : Type u_3} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 V] {c : 𝕜}
  [MeasureTheory.IsFiniteMeasure μ.variation], MeasureTheory.IsFiniteMeasure (c • μ).variation
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Sort u_3) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size)
  (h_1 :
    (size : ℕ) →
      (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) →
        (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
          motive ⟨{ size := size, buckets := buckets }, hm⟩),
  (match ⟨{ size := size, buckets := buckets }, hm⟩ with
    | ⟨{ size := size, buckets := buckets }, hm⟩ => h_1 size buckets hm) =
    h_1 size buckets hm
-- Mathlib.Data.SetLike.Basic
SetLike.coe_sort_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] (p : A), ↑↑p = ↥p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` and `j : K →+* M` are ring homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical (in fact only the `IsPRadical.pow_mem` is required) and `M` is a perfect ring,
then one can define a map `L → M` which maps an element `x` of `L` to `y ^ (p ^ -n)` if
`x ^ (p ^ n)` is equal to some element `y` of `K`.  -/
PerfectRing.liftAux : {K : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring K] →
        [inst_1 : CommSemiring L] →
          [inst_2 : CommSemiring M] →
            (i : K →+* L) → (K →+* M) → (p : ℕ) → [ExpChar M p] → [PerfectRing M p] → [IsPRadical i p] → L → M
-- Std.Internal.UV.System
/-- Changes the current working directory.
 -/
Std.Internal.UV.System.chdir : String → IO Unit
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange_prodMap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ N) (g : M' →+ N'),
  AddMonoidHom.mrange (f.prodMap g) = (AddMonoidHom.mrange f).prod (AddMonoidHom.mrange g)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instTopElemOpensOpenNhds : {α : Type u_1} → [inst : TopologicalSpace α] → (K : TopologicalSpace.Compacts α) → Top ↑K.openNhds
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.norm_sub_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal} {s : Set E} {a b : E} {r : ℝ}, LipschitzOnWith C f s → a ∈ s → b ∈ s → ‖a - b‖ ≤ r → ‖f a - f b‖ ≤ ↑C * r
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.toRuleTerm : Aesop.ElabRuleTerm → Aesop.RuleTerm
-- Mathlib.Order.Interval.Finset.Basic
Finset.sup_Iic : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : OrderBot α] (a : α),
  (Finset.Iic a).sup id = a
-- Mathlib.Algebra.Category.ModuleCat.Tannaka
/-- An ingredient of Tannaka duality for rings:
A ring `R` is equivalent to
the endomorphisms of the additive forgetful functor `Module R ⥤ AddCommGroup`.
 -/
ringEquivEndForget₂ : (R : Type u) →
  [inst : Ring R] →
    R ≃+* CategoryTheory.End (CategoryTheory.AdditiveFunctor.of (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))
-- Mathlib.CategoryTheory.Action
/-- A multiplicative action M ↻ X viewed as a functor mapping the single object of M to X
and an element `m : M` to the map `X → X` given by multiplication by `m`.  -/
CategoryTheory.actionAsFunctor : (M : Type u_1) →
  [inst : Monoid M] → (X : Type u) → [MulAction M X] → CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.isField_of_isAlgClosed_of_isLocalRing : ∀ (K : Type u_1) (A : Type u_2) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A]
  [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A], IsField A
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_ofReal : ∀ (g : GL (Fin 2) ℝ) (y : ℝ), (UpperHalfPlane.σ g) ↑y = ↑y
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- The colimit cocone for `F : J ⥤ C` lifts to a cocone in `Over (colimit F)` with cone point
`𝟙 (colimit F)`. This is automatically also a colimit cocone.  -/
CategoryTheory.Limits.colimit.toOver : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.Limits.Cocone
              ((CategoryTheory.Limits.colimit.toCostructuredArrow F).comp
                (CategoryTheory.CostructuredArrow.toOver F (CategoryTheory.Limits.colimit F)))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_const_of_allZero : ∀ {coef : ℝ} {exps : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  exps.AllZero →
    have t := { coef := coef, unit := exps };
    Filter.Tendsto (t.toFun basis) Filter.atTop (nhds coef)
-- Mathlib.RingTheory.LinearDisjoint
/-- The image of `R` in `S` is linearly disjoint with any other subalgebras.  -/
Subalgebra.LinearDisjoint.bot_left : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (B : Subalgebra R S),
  ⊥.LinearDisjoint B
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.pos : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E]
  (self : Bundle.ContMDiffRiemannianMetric IB n F E) (b : B) (v : E b), v ≠ 0 → 0 < ((self.inner b) v) v
-- Aesop.RulePattern
Aesop.instInhabitedRulePattern.default : Aesop.RulePattern
-- Lean.LocalContext
Lean.LocalContext.isEmpty : Lean.LocalContext → Bool
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Key technical lemma: the twisted inclusion `selfProdPermIncl h b` maps `a` to `F.map u b`.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProdTermIncl_fib_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A : C}
  {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} {a : (F.obj A).obj}
  (h : (CategoryTheory.ConcreteCategory.hom (F.map u)) a = CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsConnected A] (b : (F.obj A).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map u)) b =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl✝ h b))) a
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Function.IsPartialInv.eq`. -/
Function.isPartialInv_left : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α}, Function.IsPartialInv f g → ∀ (x : α), g (f x) = some x
-- Init.Data.UInt.Lemmas
UInt8.toNat_toUInt64 : ∀ (x : UInt8), x.toUInt64.toNat = x.toNat
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₂_comp_i : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₂ f φ)
      (groupCohomology.shortComplexH2 B).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i
      (groupCohomology.cochainsMap₂ f φ)
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.map.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra P Q] (f : R →+* P) (r : R)
  [inst_6 : IsLocalization.Away r S] [inst_7 : IsLocalization.Away (f r) Q],
  IsLocalization.Away.map S Q f r = IsLocalization.map Q f ⋯
-- Aesop.Forward.PremiseIndex
Aesop.instBEqPremiseIndex : BEq Aesop.PremiseIndex
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_filterMap_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  (Std.DHashMap.filterMap f m).size = m.size ↔
    ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) (Std.DHashMap.Const.get m k h)).isSome = true
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps : {α : Type u_1} →
  Lean.Language.SnapshotTree →
    α →
      (Lean.Language.SnapshotTask Lean.Language.SnapshotTree →
          α → Lean.Server.ServerTask (α × Lean.Language.SnapshotTree.foldSnaps.Control)) →
        Lean.Server.ServerTask α
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.smul : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : Monoid S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂},
  IsCompactOperator f → ∀ (c : S), IsCompactOperator (c • f)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.orbitRel_addSubgroupOf : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (H K : AddSubgroup G),
  AddAction.orbitRel (↥(H.addSubgroupOf K)) α = AddAction.orbitRel (↥(H ⊓ K)) α
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The extension of a compatible family to the generated sieve is compatible.  -/
CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
  x.Compatible → x.sieveExtend.Compatible
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ι_functorMapTgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b) (b' : B i ⟶ T)
  (hb' : CategoryTheory.CategoryStruct.comp b (CategoryTheory.Arrow.Hom.right τ) = b') (t' : A i ⟶ Y)
  (ht' : CategoryTheory.CategoryStruct.comp t (CategoryTheory.Arrow.Hom.left τ) = t'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX)
        { i := i, t := t, b := b, w := w })
      (CategoryTheory.SmallObject.functorMapTgt f τ) =
    CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πY)
      { i := i, t := t', b := b', w := ⋯ }
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instMulAction.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  UpperSet.instMulAction = Function.Injective.mulAction SetLike.coe ⋯ ⋯
-- Mathlib.Order.Filter.Prod
Filter.prod_eq_bot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- Pointwise, the indicators of δ-thickenings of a set eventually coincide
with the indicator of the set as δ>0 tends to zero.  -/
indicator_thickening_eventually_eq_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] (f : α → β) (E : Set α) (x : α),
  ∀ᶠ (δ : ℝ) in nhdsWithin 0 (Set.Ioi 0), (Metric.thickening δ E).indicator f x = (closure E).indicator f x
-- Mathlib.Topology.EMetricSpace.Weak
instWeakEMetricSpaceWithBot.eq_1 : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α] [m : WeakEMetricSpace α],
  instWeakEMetricSpaceWithBot =
    { toWeakPseudoEMetricSpace := instWeakPseudoEMetricSpaceWithBot, eq_of_edist_eq_zero := ⋯ }
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFields : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- `tensorUnit i` is an initial object when `i ≠ 0`.  -/
CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApply : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : DecidableEq I] →
            [inst_4 : CategoryTheory.Limits.HasInitial C] →
              (i : I) → i ≠ 0 → CategoryTheory.Limits.IsInitial (CategoryTheory.GradedObject.Monoidal.tensorUnit i)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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} (φ : X ⟶ Y), ((t.triangleLEGT n).map φ).hom₂ = φ
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.GrothendieckTopology.CoversTop.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {I : Type u_1} {Y : I → C},
  J.CoversTop Y →
    ∀ (F : CategoryTheory.Sheaf J A) {c : CategoryTheory.Limits.Cone F.obj} (hc : CategoryTheory.Limits.IsLimit c)
      {X : A} {f g : X ⟶ c.pt},
      (∀ (i : I),
          CategoryTheory.CategoryStruct.comp f (c.π.app (Opposite.op (Y i))) =
            CategoryTheory.CategoryStruct.comp g (c.π.app (Opposite.op (Y i)))) →
        f = g
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.map : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {H : Subgroup G} (f : G →* G')
  [Group.IsPerfect ↥H], Group.IsPerfect ↥(Subgroup.map f H)
-- Mathlib.Order.Bounds.Defs
/-- The set of lower bounds of a set.  -/
lowerBounds : {α : Type u_1} → [LE α] → Set α → Set α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above: the measure of the intersection of a decreasing sequence of measurable
sets is the limit of the measures.  -/
MeasureTheory.tendsto_measure_iInter_atTop : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Antitone s → (∃ i, μ (s i) ≠ ⊤) → Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋂ n, s n)))