mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?ₘ'.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            Option ((a : α) × β a) →
              (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun k' => (compare k k').then Ordering.gt) → Sort u_3) →
          (x : Option ((a : α) × β a)) →
            (x_1 : Std.DTreeMap.Internal.Impl.ExplorationStep α β fun k' => (compare k k').then Ordering.gt) →
              ((x : Option ((a : α) × β a)) →
                  (k' : α) →
                    (a : (compare k k').then Ordering.gt = Ordering.lt) →
                      (v : β k') →
                        (a_1 : List ((a : α) × β a)) →
                          motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1)) →
                ((base : Option ((a : α) × β a)) →
                    (a : List ((a : α) × β a)) →
                      (a_1 : Std.DTreeMap.Internal.Cell α β fun k' => (compare k k').then Ordering.gt) →
                        (r : List ((a : α) × β a)) →
                          motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r)) →
                  ((base : Option ((a : α) × β a)) →
                      (a : List ((a : α) × β a)) →
                        (a_1 : α) →
                          (a_2 : (compare k a_1).then Ordering.gt = Ordering.gt) →
                            (a_3 : β a_1) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3)) →
                    motive x x_1
-- Mathlib.Algebra.Group.Nat.TypeTags
Nat.toAdd_pow : ∀ (a : Multiplicative ℕ) (b : ℕ), Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
/-- For `k` a field of (exponential) characteristic `p`,
the `p`-th root map `k → AdjoinPthRoots k`, as a `RingEquiv`.  -/
AdjoinPthRoots.root : (k : Type u_1) → [inst : Field k] → k ≃+* AdjoinPthRoots k
-- Init.Data.List.Lemmas
List.map_flatMap : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → List β} {l : List α},
  List.map f (List.flatMap g l) = List.flatMap (fun a => List.map f (g a)) l
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.pre.sizeOf_spec : sizeOf Mathlib.Tactic.Order.OrderType.pre = 1
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.shortComplexFunctor.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι),
  HomologicalComplex.shortComplexFunctor C c i = HomologicalComplex.shortComplexFunctor' C c (c.prev i) i (c.next i)
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.smul_mem_of_normal : ∀ (G : Type u_1) (B : Type u_3) [inst : Group G] [inst_1 : Semiring B] [inst_2 : MulSemiringAction G B] {C : Type u_4}
  [inst_3 : CommSemiring C] [inst_4 : Algebra C B] (N : Subgroup G) [hN : N.Normal] [hC : IsGaloisGroup (↥N) C B]
  (g : G) (x : C), g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)
-- Mathlib.Data.Matrix.Basic
Matrix.entryLinearMap_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_7) (α : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α] (i : m) (j : n) (M : Matrix m n α), (Matrix.entryLinearMap R α i j) M = M i j
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Zipper α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : Std.DTreeMap.Internal.Zipper α β) →
          ((it : Std.DTreeMap.Internal.Zipper α β) → motive Std.DTreeMap.Internal.Impl.leaf it) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l r : Std.DTreeMap.Internal.Impl α β) →
                      (it : Std.DTreeMap.Internal.Zipper α β) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l r) it) →
              motive x x_1
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α} {a : α},
  g.IsThreeCycle → (g.support = {a, g a, g (g a)} ↔ a ∈ g.support)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticCode.beq : Lean.Lsp.DiagnosticCode → Lean.Lsp.DiagnosticCode → Bool
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?ₘ'.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive :
    Option ((a : α) × β a) →
      (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun k' => (compare k k').then Ordering.gt) → Sort u_3)
  (x : Option ((a : α) × β a)) (k' : α) (a : (compare k k').then Ordering.gt = Ordering.lt) (v : β k')
  (a_1 : List ((a : α) × β a))
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : (compare k k').then Ordering.gt = Ordering.lt) →
          (v : β k') →
            (a_2 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_2 : Std.DTreeMap.Internal.Cell α β fun k' => (compare k k').then Ordering.gt) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_2 : α) →
          (a_3 : (compare k a_2).then Ordering.gt = Ordering.gt) →
            (a_4 : β a_2) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4)),
  (match x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_1 with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2 => h_1 x k' a v a_2
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r => h_2 base a a_2 r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4 => h_3 base a a_2 a_3 a_4) =
    h_1 x k' a v a_1
-- Init.Data.Format.Basic
Std.Format.brecOn.go : {motive : Std.Format → Sort u} →
  (t : Std.Format) → ((t : Std.Format) → Std.Format.below t → motive t) → motive t ×' Std.Format.below t
-- Init.Data.String.Slice
String.Slice.SplitIterator.instFiniteIdSubsliceOfSearchStep : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] {pat : ρ}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] {s : String.Slice} [Std.Iterators.Finite (σ s) Id],
  Std.Iterators.Finite (String.Slice.SplitIterator pat s) Id
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psum.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  MvPolynomial.psum σ R n = ∑ i, MvPolynomial.X i ^ n
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- Every standard smooth homomorphism `R → S` factors into `R -> R[X₁,...,Xₙ] → S`
where `n` is the relative dimension and `R[X₁,...,Xₙ] → S` is etale.  -/
RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {n : ℕ},
  RingHom.IsStandardSmoothOfRelativeDimension n f → ∃ g, g.comp MvPolynomial.C = f ∧ g.Etale
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.HasShift.mk : {C : Type u} →
  {A : Type u_2} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        (shift : CategoryTheory.Functor (CategoryTheory.Discrete A) (CategoryTheory.Functor C C)) →
          autoParam shift.Monoidal CategoryTheory.HasShift.shiftMonoidal._autoParam → CategoryTheory.HasShift C A
-- Mathlib.Data.List.Basic
List.eq_cons_of_mem_head? : ∀ {α : Type u} {x : α} {l : List α}, x ∈ l.head? → l = x :: l.tail
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.finYoneda_map : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) {X Y : FintypeCatᵒᵖ} (f : X ⟶ Y),
  (LightCondensed.finYoneda F).map f = TypeCat.ofHom fun g => g ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.unop)
-- Mathlib.Data.Part
Part.instNeg.eq_1 : ∀ {α : Type u_1} [inst : Neg α], Part.instNeg = { neg := Part.map Neg.neg }
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_5 : ∀ (ctx : Int.Internal.Linear.Context) (v : Int.Internal.Linear.Var),
  Int.Internal.Linear.Expr.denote ctx (Int.Internal.Linear.Expr.var v) = Int.Internal.Linear.Var.denote ctx v
-- Mathlib.Algebra.Group.UniqueProds.Basic
instTwoUniqueSumsFinsupp : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddZeroClass G] [TwoUniqueSums G], TwoUniqueSums (ι →₀ G)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- **Alias** of `MeasureTheory.measureReal_def`. -/
MeasureTheory.Measure.real_def : ∀ {α : Type u_6} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.real s = (μ s).toReal
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.mapAux_lemma : ∀ (s : String) (i : String.Pos.Raw) (c : Char),
  ¬String.Pos.Raw.atEnd s i = true →
    (String.Pos.Raw.set s i c).rawEndPos.byteIdx - (String.Pos.Raw.next (String.Pos.Raw.set s i c) i).byteIdx <
      s.rawEndPos.byteIdx - i.byteIdx
-- Mathlib.RingTheory.Ideal.Pure
/-- [Stacks Tag 04PS](https://stacks.math.columbia.edu/tag/04PS) ((1) => (2)) -/
Ideal.inf_eq_mul_of_pure : ∀ {R : Type u_1} [inst : CommRing R] (I J : Ideal R) [I.Pure], I ⊓ J = I * J
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq_append : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → s = t₁ ++ t₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [Std.TransCmp cmp] {k : α}, t.WF → t.keysArray.contains k = t.contains k
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- Decidability instance: useful when working with `Finset` sums / products.  -/
SummationFilter.instDecidablePredMemSetSupportOfLeAtTop : {β : Type u_2} → (L : SummationFilter β) → [L.LeAtTop] → DecidablePred fun x => x ∈ L.support
-- Mathlib.Topology.Algebra.Field
Subfield.isClosed_topologicalClosure : ∀ {α : Type u_2} [inst : Field α] [inst_1 : TopologicalSpace α] [inst_2 : IsTopologicalDivisionRing α] (s : Subfield α),
  IsClosed ↑s.topologicalClosure
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_succ_right_eq_cons_map : ∀ {m n : ℕ}, m < n → (m<...n + 1).toList = (m + 1) :: List.map (fun x => x + 1) (m<...n).toList
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_shape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ),
  ¬n + 1 = m → ∀ (z : CochainComplex.HomComplex.Cochain F G n), CochainComplex.HomComplex.δ n m z = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_nnreal_smul_apply : ∀ {α : Type u_1} {_m : MeasurableSpace α} (c : NNReal) (μ : MeasureTheory.Measure α) (s : Set α), (c • μ) s = ↑c * μ s
-- Mathlib.Algebra.RingQuot
RingQuot.sub_quot : ∀ {R : Type uR} [inst : Ring R] (r : R → R → Prop) {a b : R},
  { toQuot := Quot.mk (RingQuot.Rel r) a } - { toQuot := Quot.mk (RingQuot.Rel r) b } =
    { toQuot := Quot.mk (RingQuot.Rel r) (a - b) }
-- Mathlib.CategoryTheory.Core
/-- The functor `functorToCore (H ⋙ F)` factors through `functorToCore H`.  -/
CategoryTheory.Core.functorToCoreCompRightIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : Type u₂} →
      [inst_1 : CategoryTheory.Groupoid G] →
        {C' : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} C'] →
            (H : CategoryTheory.Functor G C) →
              (F : CategoryTheory.Functor C C') →
                CategoryTheory.Core.functorToCore (H.comp F) ≅ (CategoryTheory.Core.functorToCore H).comp F.core
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Set.Ioi ⊥ = Set.univ
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.pure_mul_pure : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a b : α),
  NonemptyInterval.pure a * NonemptyInterval.pure b = NonemptyInterval.pure (a * b)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.symm_apply_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B) (x : A), e.symm (e x) = x
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance between a set and its closure vanishes.  -/
Metric.hausdorffEDist_self_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Metric.hausdorffEDist s (closure s) = 0
-- Mathlib.Algebra.MvPolynomial.Eval
Algebra.adjoin_eq_range : ∀ (R : Type u) {S₁ : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁] (s : Set S₁),
  Algebra.adjoin R s = (MvPolynomial.aeval Subtype.val).range
-- Init.Data.Vector.MapIdx
Vector.mapIdx_push : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : ℕ → α → α_1} {xs : Vector α n} {a : α},
  Vector.mapIdx f (xs.push a) = (Vector.mapIdx f xs).push (f n a)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
CategoryTheory.Over.hasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasFiniteWidePullbacks C],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over B)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.natDegree_mul_comm : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → ∀ (q : Polynomial R), (p * q).natDegree = (q * p).natDegree
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.mkHCongrWithArity.withNewEqs : {α : Type} →
  Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starLift_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  [inst_10 : StarModule R C] (φ : A →⋆ₙₐ[R] C), Unitization.starLift φ = { toAlgHom := φ.toAlgHom, map_star' := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_strictMono_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 → StrictMono (AddSubmonoid.map f)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.ofComapInfPrincipal_eq_of_map : ∀ {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g),
  Ultrafilter.map m (Ultrafilter.ofComapInfPrincipal h) = g
-- Mathlib.Algebra.Group.Basic
neg_zsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), -n • a = -(n • a)
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedAddCommGroup : {E : Type u_2} → [SeminormedAddCommGroup E] → SeminormedAddCommGroup (ULift.{u_5, u_2} E)
-- Mathlib.Data.Quot
Quotient.forall : ∀ {α : Sort u_3} {s : Setoid α} {p : Quotient s → Prop}, (∀ (a : Quotient s), p a) ↔ ∀ (a : α), p ⟦a⟧
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.instMonoidalCategoryStruct : {R : Type u} → [inst : CommRing R] → [Invertible 2] → CategoryTheory.MonoidalCategoryStruct (QuadraticModuleCat R)
-- Lean.Elab.Command
Lean.Elab.Command.instMonadOptionsCommandElabM : Lean.MonadOptions Lean.Elab.Command.CommandElabM
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extend_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖)
  (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : E),
  (f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ h_norm₂) (e₁ x) = e₂ (f x)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldr.eq_1 : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : σ), RBTree.RBNode.Stream.foldr f RBTree.RBNode.Stream.nil x = x
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_tfae : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  IsOpen C →
    C.Nonempty →
      ConcaveOn ℝ C f →
        [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
            ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (nhds x₀) f,
            ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (nhds x₀) f,
            ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f|].TFAE
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (l l_1 : ρ), l = l_1 → m.insertMany l = m_1.insertMany l_1
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup E₂] [inst_5 : Module 𝕜₂ E₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_6 : RingHomIsometric σ₁₂] (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ),
  (p.comp f).closedBall x r = ⇑f ⁻¹' p.closedBall (f x) r
-- Batteries.Tactic.HelpCmd
/-- `#help note "foo"` searches for all library notes whose
label starts with "foo", then displays those library notes sorted alphabetically by label,
grouped by label.
The command only displays the library notes that are declared in
imported files or in the same file above the line containing the command.
 -/
Batteries.Tactic.«command#help_Note___» : Lean.ParserDescr
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_comm : ∀ {α : Type u} {β : Type v} {f g : α → β} {l : Filter α}, f =ᶠ[l] g ↔ g =ᶠ[l] f
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀), (CategoryTheory.PreZeroHypercover.map F E).f i = F.map (E.f i)
-- Mathlib.Topology.Separation.Basic
t1Space_antitone : ∀ {X : Type u_3}, Antitone (@T1Space X)
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The residue field of `FiniteElement`. This quotient inherits an order from `K`,
which makes it into a linearly ordered Archimedean field.  -/
ArchimedeanClass.FiniteResidueField : (K : Type u_1) → [inst : LinearOrder K] → [inst_1 : Field K] → [IsOrderedRing K] → Type u_1
-- Mathlib.Order.Types.Defs
/-- Equivalence relation on linear orders on arbitrary types in universe `u`, given by order
isomorphism.  -/
OrderType.instSetoid : Setoid LinOrd
-- Mathlib.Computability.DFA
/-- DFAs are closed under complement:
Given a DFA `M`, `Mᶜ` is also a DFA such that `L(Mᶜ) = {x ∣ x ∉ L(M)}`.  -/
DFA.instCompl : {α : Type u} → {σ : Type v} → Compl (DFA α σ)
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.span_le_supported_biUnion_support : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (α →₀ M)), Submodule.span R s ≤ Finsupp.supported M R (⋃ x ∈ s, ↑x.support)
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The sum of two independent Poisson random variables with rates `r₁, r₂` is a Poisson
random variable with rate `r₁ + r₂`.  -/
ProbabilityTheory.IndepFun.hasLaw_add_poissonMeasure : ∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {r₁ r₂ : NNReal} {X Y : Ω → ℕ},
  ProbabilityTheory.IndepFun X Y P →
    ProbabilityTheory.HasLaw X (ProbabilityTheory.poissonMeasure r₁) P →
      ProbabilityTheory.HasLaw Y (ProbabilityTheory.poissonMeasure r₂) P →
        ProbabilityTheory.HasLaw (X + Y) (ProbabilityTheory.poissonMeasure (r₁ + r₂)) P
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- `.expr` is an expression that will be indexed.  -/
Lean.Meta.RefinedDiscrTree.StackEntry.expr : Lean.Meta.RefinedDiscrTree.ExprInfo → Lean.Meta.RefinedDiscrTree.StackEntry
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_inj : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] {f g : α →ₙ+ β},
  WithZero.mapAddHom f = WithZero.mapAddHom g ↔ f = g
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.copy_sliceTo_eq : ∀ {t₁ t₂ s : String} {p : s.Pos}, p.Splits t₁ t₂ → (s.sliceTo p).copy = t₁
-- Init.Data.List.Sort.Lemmas
List.MergeSort.Internal.splitInTwo_fst : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitInTwo l).1 = ⟨List.take ((n + 1) / 2) ↑l, ⋯⟩
-- Mathlib.Algebra.Group.Graph
/-- **Goursat's lemma** for additive monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of additive monoids. Assume that the natural maps from
`G` to both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃+ I`.  -/
AddSubmonoid.exists_addEquiv_eq_mgraph : ∀ {H : Type u_2} {I : Type u_3} [inst : AddMonoid H] [inst_1 : AddMonoid I] {G : AddSubmonoid (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) →
    Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = e.toAddMonoidHom.mgraph
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.IsKProjective.nonempty_homotopy_zero : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {K : CochainComplex C ℤ} [self : K.IsKProjective] {L : CochainComplex C ℤ} (f : K ⟶ L),
  HomologicalComplex.Acyclic L → Nonempty (Homotopy f 0)
-- Plausible.Arbitrary
Plausible.Arbitrary.mk : {α : Type u} → Plausible.Gen α → Plausible.Arbitrary α
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.Set : ShareCommon.StateFactoryImpl → Type
-- Init.Prelude
/-- `ByteArray` is like `Array UInt8`, but with an efficient run-time representation as a packed
byte buffer.
 -/
ByteArray : Type
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t → (μ.restrict s).real t = μ.real (t ∩ s)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_nonneg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) (x : γ) (s : Set β), 0 ≤ κ.densityProcess ν n a x s
-- Mathlib.Order.SupIndep
/-- An independent indexed family of elements in a complete lattice is one in which every element
is disjoint from the `iSup` of the rest.

Example: an indexed family of non-zero elements in a
vector space is linearly independent iff the indexed family of subspaces they generate is
independent in this sense.

Example: an indexed family of submodules of a module is independent in this sense if
and only the natural map from the direct sum of the submodules to the module is injective.  -/
iSupIndep : {ι : Sort u_5} → {α : Type u_6} → [CompleteLattice α] → (ι → α) → Prop