mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.AbsConvex
exists_nhds_hasAntitoneBasis_absConvex_open_add_closure_subset : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup E] [ZeroLEOneClass 𝕜] [FirstCountableTopology E],
  ∃ x,
    (nhds 0).HasAntitoneBasis x ∧
      ∀ (n : ℕ), IsOpen (x n) ∧ AbsConvex 𝕜 (x n) ∧ x (n + 1) + x (n + 1) ⊆ x n ∧ closure (x (n + 1)) ⊆ x n
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Balanced.dual : ∀ {α : Type u_1} {t : Ordnode α}, t.Balanced → t.dual.Balanced
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit.congr_simp : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ hc₁_1 : CategoryTheory.Limits.IsColimit c₁),
  hc₁ = hc₁_1 →
    ∀ {c₂ : CategoryTheory.Limits.Cocone K₂} (hc₂ hc₂_1 : CategoryTheory.Limits.IsColimit c₂),
      hc₂ = hc₂_1 →
        ∀
          {c₃ :
            CategoryTheory.Limits.Cocone
              (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
          (hc₃ hc₃_1 : CategoryTheory.Limits.IsColimit c₃),
          hc₃ = hc₃_1 →
            CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃ =
              CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁_1 hc₂_1 hc₃_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] (a : α), MulLECancellable a = ∀ ⦃b c : α⦄, a * b ≤ a * c → b ≤ c
-- Mathlib.Computability.TuringDegree
TuringDegree.instPartialOrder : PartialOrder TuringDegree
-- Mathlib.Order.SuccPred.Limit
PredOrder.colimitRecOn_of_isPredLimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (isMax : (a : α) → IsMax a → motive a)
  (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) (hb : Order.IsPredLimit b),
  PredOrder.colimitRecOn b isMax pred isPredLimit =
    isPredLimit b hb fun x x_1 => PredOrder.colimitRecOn x isMax pred isPredLimit
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget₂Mon_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommMon.forget₂Mon C).comp (CategoryTheory.Mon.forget C) = CategoryTheory.CommMon.forget C
-- Mathlib.RingTheory.Coalgebra.MulOpposite
MulOpposite.instCoalgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → Coalgebra R Aᵐᵒᵖ
-- Init.Data.SInt.Lemmas
Int16.toInt_toInt32 : ∀ (x : Int16), x.toInt32.toInt = x.toInt
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_X_pow_self_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (p : PowerSeries R), (PowerSeries.trunc n) (PowerSeries.X ^ n * p) = 0
-- Lean.Elab.Term.TermElabM
/-- Nested `let rec` expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
 -/
Lean.Elab.Term.LetRecToLift : Type
-- Mathlib.Logic.Equiv.Defs
Equiv.existsUnique_congr : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (a : α), p a ↔ q (e a)) → ((∃! a, p a) ↔ ∃! b, q b)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.subtractionCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : SubtractionCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.subtractionCommMonoid f hf one mul inv div npow zpow =
    { toSubtractionMonoid := Function.Injective.subtractionMonoid f hf one mul inv div npow zpow, add_comm := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_if : ∀ {m n : ℕ}, (m...n).toList = if m < n then m :: ((m + 1)...n).toList else []
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_Ici : ∀ {n : ℕ} (i : Fin n), Fin.rev ⁻¹' Set.Ici i = Set.Iic i.rev
-- Mathlib.LinearAlgebra.Span.Defs
/-- A version of `Submodule.span_eq` for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects.  -/
Submodule.coe_span_eq_self : ∀ {R : Type u_1} {M : Type u_4} {S : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S), ↑(Submodule.span R ↑s) = ↑s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).get? k = none
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.neg_op_vadd_set_distrib : ∀ {α : Type u_2} [inst : AddGroup α] (a : α) (s : Set α), -(AddOpposite.op a +ᵥ s) = -a +ᵥ -s
-- Mathlib.Analysis.Analytic.ConvergenceRadius
constFormalMultilinearSeries.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : ContinuousConstSMul 𝕜 E] [inst_4 : IsTopologicalAddGroup E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : ContinuousConstSMul 𝕜 F] (c : F),
  constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 𝕜 E c
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable, and `f =O[atBot] g`, `f =O[atTop] g'` for some
`g`, `g'` integrable at `atBot` and `atTop` respectively, then `f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot_atTop : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] {g' : α → F}
  [Filter.atBot.IsMeasurablyGenerated] [Filter.atTop.IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrable f μ →
    f =O[Filter.atBot] g →
      MeasureTheory.IntegrableAtFilter g Filter.atBot μ →
        f =O[Filter.atTop] g' → MeasureTheory.IntegrableAtFilter g' Filter.atTop μ → MeasureTheory.Integrable f μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_isBasis'_eq : ∀ {α : Type u_1} {M : Matroid α}, M.removeLoops.IsBasis' = M.IsBasis'
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.comap_lt_comap`. -/
Ideal.IntegralClosure.comap_lt_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] {I J : Ideal A} [I.IsPrime],
  I < J → Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
-- Mathlib.Computability.Encoding
Computability.Encoding.card_le_aleph0 : ∀ {α : Type u_1} {Γ : Type u_2} (e : Computability.Encoding α Γ) [Countable Γ], Cardinal.mk α ≤ Cardinal.aleph0
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ.eq_1 : ∀ (s : ℂ), s.Gammaℝ = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is weakly between the other two, the oriented angle at the
first point (reversed) is zero.  -/
Wbtw.oangle₃₁₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₁ p₂ = 0
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_eq_ofNat : ∀ {m : ℕ∞} {n : ℕ} [inst : n.AtLeastTwo], ↑m = OfNat.ofNat n ↔ m = OfNat.ofNat n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.WF.getThenInsertIfNew?! : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [Std.LawfulEqOrd α] {k : α} {v : β}
  {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v).2.WF
-- Mathlib.Analysis.Convex.Independent
/-- If a family is convex independent, a point in the family is not in the convex hull of the other
points. See `convexIndependent_set_iff_notMem_convexHull_sdiff` for the `Set` version.  -/
convexIndependent_iff_notMem_convexHull_sdiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {p : ι → E},
  ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- `preVariationFun` of the empty set is equal to zero.  -/
MeasureTheory.preVariation.empty : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal), MeasureTheory.preVariationFun f ∅ = 0
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.foldlAux.eq_def : ∀ {α : Type u} (f : α → Char → α) (s : String) (stopPos i : String.Pos.Raw) (a : α),
  String.Legacy.foldlAux f s stopPos i a =
    if h : i < stopPos then
      have this := ⋯;
      String.Legacy.foldlAux f s stopPos (String.Pos.Raw.next s i) (f a (String.Pos.Raw.get s i))
    else a
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s` unifies with `t`, convert a result for `s` to a result for `t`.

If `s` does not unify with `t`, this results in a type-incorrect proof.
 -/
Mathlib.Meta.Finset.ProveEmptyOrConsResult.uncheckedCast : {u v : Lean.Level} →
  {α : Q(Type u)} →
    {β : Q(Type v)} →
      (s : Q(Finset «$α»)) →
        (t : Q(Finset «$β»)) →
          Mathlib.Meta.Finset.ProveEmptyOrConsResult s → Mathlib.Meta.Finset.ProveEmptyOrConsResult t
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.withAntiquotSuffixSpliceFn : Lean.SyntaxNodeKind → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Combinatorics.Additive.Corner.Defs
Set.Subsingleton.isCornerFree : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)}, A.Subsingleton → IsCornerFree A
-- Init.Data.UInt.Lemmas
UInt16.toUSize_div : ∀ (a b : UInt16), (a / b).toUSize = a.toUSize / b.toUSize
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C}
  (φ ψ : W.LeftFraction₂ X Y),
  φ.fst.map L ⋯ = ψ.fst.map L ⋯ ∧ φ.snd.map L ⋯ = ψ.snd.map L ⋯ ↔ CategoryTheory.MorphismProperty.LeftFraction₂Rel φ ψ
-- Mathlib.Algebra.Order.Group.MinMax
min_div_div_right' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b c : α),
  min (a / c) (b / c) = min a b / c
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange f).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.opensRange f).ι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_isometry_right_iff : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₂ → P₃},
  Isometry f → (Similar v₁ (f ∘ v₂) ↔ Similar v₁ v₂)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.boundedAtFilter_cuspFunction : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
      (nhdsWithin 0 {0}ᶜ).BoundedAtFilter (Function.Periodic.cuspFunction h f)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filterMapWithPostcondition : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β β₂ γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [inst_8 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_10 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_12 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.IterM.filterMapWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      match __do_lift with
        | some c => g c acc
        | none => pure (ForInStep.yield acc)
-- Mathlib.Probability.Martingale.BorelCantelli
/-- The stopped process of `f` above `r` is the process that is equal to `f` until `leastGE f r`
(the first time `f` passes above `r`), and then is constant afterwards.  -/
MeasureTheory.stoppedAbove : {ι : Type u_1} →
  {Ω : Type u_2} →
    {β : Type u_3} → [inst : LinearOrder ι] → [OrderBot ι] → [InfSet ι] → [Preorder β] → (ι → Ω → β) → β → ι → Ω → β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.entryAtIdx?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.Equiv t₂ → t₁.entryAtIdx? i = t₂.entryAtIdx? i
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- For `m ≤ n + 1`, the `m`-spine of `X` factors through the `n + 1`-truncation
of `X`.  -/
SSet.truncation_spine : ∀ (X : SSet) (n m : ℕ) (h : m ≤ n + 1), ((SSet.truncation (n + 1)).obj X).spine m h = X.spine m
-- Mathlib.Data.List.Map2
List.map₂Right_cons_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.map₂Right f (a :: as) (b :: bs) = f (some a) b :: List.map₂Right f as bs
-- Aesop.Forward.Match.Types
Aesop.instBEqCompleteMatch : BEq Aesop.CompleteMatch
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_lt_enum : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))},
  r ((Ordinal.enum r) o₁) ((Ordinal.enum r) o₂) ↔ o₁ < o₂
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.nilpotent_ad_of_nilpotent_algebra : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [LieRing.IsNilpotent L],
  ∃ k, ∀ (x : L), (LieAlgebra.ad R L) x ^ k = 0
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial_zero_eq_C_apply : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (PowerSeries.monomial 0) a = PowerSeries.C a
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.closure_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), closure {K | (↑K).Finite ∧ ↑K ⊆ s} = {K | ↑K ⊆ closure s}
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_sdiff_singleton : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ t → a ∉ s → s ⊆ t \ {a}
-- Lean.Parser.Tactic.Doc
/-- The mapping between tactics and their custom names.

The first projection in each pair is the tactic name, and the second is the custom name.
 -/
Lean.Parser.Tactic.Doc.tacticNameExt : Lean.PersistentEnvExtension (Lean.Name × String) (Lean.Name × String) (Lean.NameMap String)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pushforward along a morphism is the same as refining the singleton pre-`0`-hypercover.  -/
CategoryTheory.PreZeroHypercover.pushforwardIsoBind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        (E : CategoryTheory.PreZeroHypercover X) →
          CategoryTheory.PreZeroHypercover.pushforward f E ≅
            (CategoryTheory.PreZeroHypercover.singleton f).bind fun x => E
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIoo : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → (a b : α) → Fintype ↑(Set.Ioo a b)
-- Init.Data.Option.Lemmas
Option.isSome_iff_exists : ∀ {α : Type u_1} {x : Option α}, x.isSome = true ↔ ∃ a, x = some a
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
AntitoneOn.memLp_of_measure_ne_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {p : ENNReal} {f : X → E},
  AntitoneOn f s →
    ∀ {a b : X}, IsLeast s a → IsGreatest s b → μ s ≠ ⊤ → MeasurableSet s → MeasureTheory.MemLp f p (μ.restrict s)
-- Mathlib.Analysis.Hofer
hofer : ∀ {X : Type u_1} [inst : MetricSpace X] [CompleteSpace X] (x : X) (ε : ℝ),
  0 < ε →
    ∀ {ϕ : X → ℝ},
      Continuous ϕ →
        (∀ (y : X), 0 ≤ ϕ y) →
          ∃ ε' > 0, ∃ x', ε' ≤ ε ∧ dist x' x ≤ 2 * ε ∧ ε * ϕ x ≤ ε' * ϕ x' ∧ ∀ (y : X), dist x' y ≤ ε' → ϕ y ≤ 2 * ϕ x'
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.categoryOfGradedObjects : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    (β : Type w) → CategoryTheory.Category.{max w v, max u w} (CategoryTheory.GradedObject β C)
-- Mathlib.Topology.Maps.Basic
Topology.isQuotientMap_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsQuotientMap f ↔ Function.Surjective f ∧ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)
-- Init.Data.Int.Lemmas
Int.sub_eq_zero : ∀ {a b : ℤ}, a - b = 0 ↔ a = b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.isOpenMap : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), IsOpenMap ⇑e
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_of_fintype : ∀ (α β : Type u) [inst : Fintype α] [inst_1 : Zero β], Cardinal.mk (α →₀ β) = Cardinal.mk β ^ Fintype.card α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.cotrident_ι_app_one : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f],
  (CategoryTheory.Limits.wideCoequalizer.cotrident f).ι.app CategoryTheory.Limits.WalkingParallelFamily.one =
    CategoryTheory.Limits.wideCoequalizer.π f
-- Mathlib.FieldTheory.KrullTopology
/-- Given a field extension `L/K`, `finiteExts K L` is the set of
intermediate field extensions `L/E/K` such that `E/K` is finite.  -/
finiteExts : (K : Type u_1) →
  [inst : Field K] → (L : Type u_2) → [inst_1 : Field L] → [inst_2 : Algebra K L] → Set (IntermediateField K L)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_homogeneousCore_eq_self : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : HomogeneousIdeal 𝒜), Ideal.homogeneousCore 𝒜 I.toIdeal = I
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousFunctionalCalculus.spectrum_nonempty : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : TopologicalSpace A} {inst_8 : Algebra R A} [self : ContinuousFunctionalCalculus R A p]
  [Nontrivial A] (a : A), p a → (spectrum R a).Nonempty
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.instWhiskerVerticalOfIsIsoFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] {T : CategoryTheory.Functor C₁ D₁} {L : CategoryTheory.Functor C₁ C₂}
  {R : CategoryTheory.Functor D₁ D₂} {B : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T L R B)
  {L' : CategoryTheory.Functor C₁ C₂} {R' : CategoryTheory.Functor D₁ D₂} [w.GuitartExact] (α : L ⟶ L') (β : R' ⟶ R)
  [CategoryTheory.IsIso α] [CategoryTheory.IsIso β], (w.whiskerVertical α β).GuitartExact
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticWith : {α : Type} → [Lean.FromJson α] → Lean.FromJson (Lean.Lsp.DiagnosticWith α)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.generatorsOfIsCokernelFree_s : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)) (a : σ),
  (SheafOfModules.generatorsOfIsCokernelFree f g H H').s a = M.freeHomEquiv g a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ ProfiniteGrp.{u_1} Profinite)
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι}, (∀ i ∈ a, UpperSemicontinuous (f i)) → UpperSemicontinuous fun z => ∑ i ∈ a, f i z