mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedMap_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : HasFibers.Fib p R} (f : R ⟶ S)
  (ψ : (HasFibers.ι R).obj b' ⟶ a) [inst_3 : p.IsCartesian f ψ] (φ : (HasFibers.ι R).obj b ⟶ a)
  [inst_4 : p.IsHomLift f φ],
  CategoryTheory.CategoryStruct.comp ((HasFibers.ι R).map (HasFibers.inducedMap f ψ φ)) ψ = φ
-- Mathlib.CategoryTheory.Types.Basic
/-- A morphism in `Type` is an epimorphism if and only if it is surjective.  -/
CategoryTheory.epi_iff_surjective : ∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.self_apply_inverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → ∀ (y : M₂), f (f.inverse y) = y
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.finsetSum' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) → MeasureTheory.IsStronglyProgressive f (∑ c ∈ s, U c)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
/-- For a spectral object indexed by a preorder, this is the map
`E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₃) ⟶ E^{n₁}(i₀ ≤ i₁ ≤ i₂ ≤ i₄)`.  -/
CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃' : {C : Type u_1} →
  {ι' : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : Preorder ι'] →
          (X' : CategoryTheory.Abelian.SpectralObject C ι') →
            (i₀ i₁ i₂ i₃ i₄ : ι') →
              (hi₀₁ : i₀ ≤ i₁) →
                (hi₁₂ : i₁ ≤ i₂) →
                  (hi₂₃ : i₂ ≤ i₃) →
                    (hi₃₄ : i₃ ≤ i₄) →
                      (n₀ n₁ n₂ : ℤ) →
                        (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'._auto_1) →
                          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'._auto_3) →
                            X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                                (CategoryTheory.homOfLE hi₂₃) n₀ n₁ n₂ hn₁ hn₂ ⟶
                              X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂)
                                (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- Given an embedding `e : Embedding c c'` of complex shapes which satisfy `e.IsTruncLE`,
this is the (canonical) truncation functor
`HomologicalComplex C c' ⥤ HomologicalComplex C c'`.  -/
ComplexShape.Embedding.truncLEFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [e.IsTruncLE] →
            (C : Type u_4) →
              [inst : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [CategoryTheory.Limits.HasZeroObject C] →
                    [CategoryTheory.CategoryWithHomology C] →
                      CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c')
-- Mathlib.Topology.ContinuousMap.Basic
/-- The restriction of a continuous map to the preimage of a set.  -/
ContinuousMap.restrictPreimage : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (f : C(α, β)) → (s : Set β) → C(↑(⇑f ⁻¹' s), ↑s)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_const_bot : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} [inst_1 : Bot ι],
  (MeasureTheory.stoppedValue u fun x => ⊥) = u ⊥
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instOrderTop : {X : AlgebraicGeometry.Scheme} → OrderTop X.IdealSheafData
-- Mathlib.Analysis.Distribution.Support
/-- **Alias** of `Distribution.TemperedDistribution.IsVanishingOn.smulLeftCLM`. -/
Distribution.IsVanishingOn.smulLeftCLM : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E},
  Distribution.IsVanishingOn (⇑f) s →
    ∀ {g : E → ℂ},
      Function.HasTemperateGrowth g → Distribution.IsVanishingOn (⇑((TemperedDistribution.smulLeftCLM F g) f)) s
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- Postcompose a simplicial homotopy with a morphism of simplicial objects.  -/
CategoryTheory.SimplicialObject.Homotopy.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      {f g : X ⟶ Y} →
        CategoryTheory.SimplicialObject.Homotopy f g →
          {Y' : CategoryTheory.SimplicialObject C} →
            (p : Y ⟶ Y') →
              CategoryTheory.SimplicialObject.Homotopy (CategoryTheory.CategoryStruct.comp f p)
                (CategoryTheory.CategoryStruct.comp g p)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (c :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C)))
  {X Y : CategoryTheory.WithInitial SimplexCategory} (f : X ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.inverse.obj c).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f =>
      c.right.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => c.hom.app a
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id c.left
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map_id : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C],
  CategoryTheory.Limits.chosenEnd.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.chosenEnd F)
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : D ⥤ C ⥤ D`, `Y : C` and `X : GradedObject J D`,
`((mapBifunctor F J I).obj X).obj ((single₀ I).obj X) a` is an initial when `a : J × I`
is such that `a.2 ≠ 0`.  -/
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀IsInitial : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) →
                    (Y : C) →
                      [∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)] →
                        (X : CategoryTheory.GradedObject J D) →
                          (a : J × I) →
                            a.2 ≠ 0 →
                              CategoryTheory.Limits.IsInitial
                                (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
                                  ((CategoryTheory.GradedObject.single₀ I).obj Y) a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true →
        Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter m₂ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} (φ : R ⟶ R')
  {X : Cᵒᵖ} (r' : R'.obj X), ((CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r').map φ).IsAmalgamation r'
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.Ring.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  P.Ring = (Polynomial (Polynomial R) ⧸ Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.associator_inv_hom : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c)
  (h : CategoryTheory.FreeBicategory.Hom c d), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Init.PropLemmas
and_congr_right_eq : ∀ {a b c : Prop}, (a → b = c) → (a ∧ b) = (a ∧ c)
-- Mathlib.CategoryTheory.Category.Preorder
/-- The equivalence of categories from the order dual of a preordered type `X`
to the opposite category of the preorder `X`.  -/
CategoryTheory.orderDualEquivalence : (X : Type u) → [inst : Preorder X] → Xᵒᵈ ≌ Xᵒᵖ
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The `n`-skeleton of a CW complex, for `n ∈ ℕ ∪ {∞}`. For statements use `skeletonLT` instead
and then derive the statement about `skeleton`.  -/
Topology.RelCWComplex.skeleton : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) → {D : Set X} → [inst : Topology.RelCWComplex C D] → ℕ∞ → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Data.Finset.Sum
Finset.toLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (u : Finset (α ⊕ β)), u.toLeft = Finset.filterMap (Sum.elim some fun x => none) u ⋯
-- Std.Time.Internal.Bounded
/-- Expand the bottom of the bounded to a number `nlo` if `lo` is greater or equal to the previous lower bound.
 -/
Std.Time.Internal.Bounded.LE.expandBottom : {lo hi nlo : ℤ} → Std.Time.Internal.Bounded.LE lo hi → nlo ≤ lo → Std.Time.Internal.Bounded.LE nlo hi
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_bot : ∀ {G : Type u_1} [inst : AddGroup G], ↑⊥ = {0}
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.div_slash_SL2 : ∀ (k1 k2 : ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f g : UpperHalfPlane → ℂ),
  SlashAction.map (k1 - k2) A (f / g) = SlashAction.map k1 A f / SlashAction.map k2 A g
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_6 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f g : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.case g, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_6 (f.case g) f g ⋯ k
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instStarRing : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalSemiring β] →
        [inst_2 : StarRing β] →
          [inst_3 : TopologicalSpace β] →
            [ContinuousStar β] → [inst_5 : IsTopologicalSemiring β] → StarRing (CompactlySupportedContinuousMap α β)
-- Mathlib.Data.FunLike.Group
FunLike.commGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : CommGroup β]
  [inst_8 : IsOneApply F α β] [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β]
  [inst_12 : IsPowApply ℕ F α β] [inst_13 : IsPowApply ℤ F α β],
  FunLike.commGroup = Function.Injective.commGroup (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Qq.MetaM
/-- If `e` is a `ty`, then view it as a term of `Q($ty)`.  -/
Qq.checkTypeQ : {u : Lean.Level} →
  Lean.Expr →
    (ty :
        have u := u;
        Q(Sort u)) →
      Lean.MetaM (Option Q(«$ty»))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- For `x` within a ball of Archimedean class `c`, `f.val x`'coefficient at `d` vanishes
for `d ≤ c`.  -/
HahnEmbedding.Partial.coeff_eq_zero_of_mem : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] {c : FiniteArchimedeanClass M} {x : ↥(↑f).domain},
  ↑x ∈ FiniteArchimedeanClass.ball K c → ∀ {d : FiniteArchimedeanClass M}, ↑d ≤ ↑c → (ofLex (↑↑f x)).coeff d = 0
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedUserInfo : Inhabited Std.Http.URI.UserInfo
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp_zero : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp Turing.ToPartrec.Code.zero' k =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.zero' k) ∪
      Turing.PartrecToTM2.contSupp k
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.addSubgroupOf_isOpen : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (U K : AddSubgroup G),
  IsOpen ↑K → IsOpen ↑(K.addSubgroupOf U)
-- Init.Omega.Constraint
Lean.Omega.Constraint.combine_sat : ∀ (c c' : Lean.Omega.Constraint) (t : ℤ), ((c.combine c').sat t = true) = (c.sat t = true ∧ c'.sat t = true)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.leadingCoeff_neg_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : LinearOrder R]
  {x : Lex (HahnSeries Γ R)}, (ofLex x).leadingCoeff < 0 ↔ x < 0
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.add : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : AddZeroClass β] [ContinuousAdd β] {l : Filter α}
  {f g : α → β}, l.ZeroAtFilter f → l.ZeroAtFilter g → l.ZeroAtFilter (f + g)
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.sub_top : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a : WithTop α}, a - ⊤ = ↑⊥
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded  -/
UniformCauchySeqOnFilter : {α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → Filter ι → Filter α → Prop
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → v.intValuation = v_1.intValuation
-- Mathlib.Order.GaloisConnection.Basic
sSup_image2_eq_sSup_sSup : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) → sSup (Set.image2 l s t) = l (sSup s) (sSup t)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_union : ∀ {K : Type u} [inst : DivisionRing K] (s t : Set K), Subfield.closure (s ∪ t) = Subfield.closure s ⊔ Subfield.closure t
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  {a : X} [inst_5 : LinearOrder X] [CompactIccSpace X],
  MeasureTheory.IntegrableOn f (Set.Ici a) μ ↔
    MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_zero : ∀ {α : Type u_1} {β : Type v} (f : α → Option β), Multiset.filterMap f 0 = 0
-- Mathlib.RingTheory.RingHom.Integral
RingHom.isIntegral_stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
-- Init.Data.Fin.Lemmas
Fin.mk_succ_pos : ∀ {n : ℕ} (i : ℕ) (h : i < n), 0 < ⟨i.succ, ⋯⟩
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_top : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  FirstOrder.Language.Substructure.comap f ⊤ = ⊤
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk.injEq : ∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (toEquiv : R ≃ S)
  (map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) (toEquiv_1 : R ≃ S)
  (map_mul'_1 : ∀ (x y : R), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
  (map_add'_1 : ∀ (x y : R), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y),
  ({ toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' } =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_smul : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_3} [inst_1 : Semiring S] [inst_2 : Module R S] (r : R)
  (x : PowerSeries S), (HahnSeries.ofPowerSeries ℤ S) (r • x) = r • (HahnSeries.ofPowerSeries ℤ S) x
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- Any discrete subgroup of `SL(2, ℝ)` acts properly discontinuously on `ℍ`.  -/
UpperHalfPlane.instProperlyDiscontinuousSL2RSubgroup : ∀ (𝒢 : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)) [DiscreteTopology ↥𝒢],
  ProperlyDiscontinuousSMul (↥𝒢) UpperHalfPlane
-- Mathlib.Logic.Function.Defs
/-- For a two-argument function `f`, `swap f` is the same function but taking the arguments
in the reverse order. `swap f y x = f x y`.  -/
Function.swap : {α : Sort u₁} → {β : Sort u₂} → {φ : α → β → Sort u₃} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p]
  (x : L) (n : ℕ) (y : K), i y = x ^ p ^ n → (IsPerfectClosure.equiv i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mk.injEq : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {S : C} (toPreOneHypercoverDenseData : F.PreOneHypercoverDenseData S)
  (mem₀ : toPreOneHypercoverDenseData.toPreOneHypercover.sieve₀ ∈ J S)
  (mem₁₀ :
    ∀ (i₁ i₂ : toPreOneHypercoverDenseData.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData.X i₁)
      (p₂ : W₀ ⟶ toPreOneHypercoverDenseData.X i₂),
      CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData.f i₁) =
          CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData.f i₂) →
        toPreOneHypercoverDenseData.sieve₁₀ p₁ p₂ ∈ J₀ W₀)
  (toPreOneHypercoverDenseData_1 : F.PreOneHypercoverDenseData S)
  (mem₀_1 : toPreOneHypercoverDenseData_1.toPreOneHypercover.sieve₀ ∈ J S)
  (mem₁₀_1 :
    ∀ (i₁ i₂ : toPreOneHypercoverDenseData_1.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData_1.X i₁)
      (p₂ : W₀ ⟶ toPreOneHypercoverDenseData_1.X i₂),
      CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData_1.f i₁) =
          CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData_1.f i₂) →
        toPreOneHypercoverDenseData_1.sieve₁₀ p₁ p₂ ∈ J₀ W₀),
  ({ toPreOneHypercoverDenseData := toPreOneHypercoverDenseData, mem₀ := mem₀, mem₁₀ := mem₁₀ } =
      { toPreOneHypercoverDenseData := toPreOneHypercoverDenseData_1, mem₀ := mem₀_1, mem₁₀ := mem₁₀_1 }) =
    (toPreOneHypercoverDenseData = toPreOneHypercoverDenseData_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.inv.app CategoryTheory.Limits.WalkingParallelPair.zero =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingParallelPair.zero
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (name : Lean.Name) (val : Lean.Elab.Term.Arg) (numImplicitParams : ℕ),
  sizeOf { ref := ref, name := name, val := val, numImplicitParams := numImplicitParams } =
    1 + sizeOf ref + sizeOf name + sizeOf val + sizeOf numImplicitParams
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.IsCofiltered D], CategoryTheory.IsCofiltered (C × D)