mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.isKernelPair : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} {p₁ p₂ : R ⟶ A}
  (self : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂), CategoryTheory.IsKernelPair self.π p₁ p₂
-- Mathlib.CategoryTheory.Sums.Basic
/-- Any functor out of a sum is the sum of its precomposition with the inclusions.  -/
CategoryTheory.Functor.isoSum : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor (A ⊕ B) C) →
              F ≅ ((CategoryTheory.Sum.inl_ A B).comp F).sum' ((CategoryTheory.Sum.inr_ A B).comp F)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C}
  (z w : (CategoryTheory.FunctorToTypes.prod F G).obj a), z.1 = w.1 → z.2 = w.2 → z = w
-- Mathlib.Topology.Algebra.Support
subset_tsupport : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
  Function.support f ⊆ tsupport f
-- Mathlib.Algebra.Order.Disjointed
/-- A recursion principle for `disjointed`. To construct / define something for `disjointed f i`,
it's enough to construct / define it for `f n` and to able to extend through diffs.

Note that this version allows an arbitrary `Sort*`, but requires the domain to be `Nat`, while
the root-level `disjointedRec` allows more general domains but requires `p` to be `Prop`-valued.  -/
Nat.disjointedRec : {α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] →
    {f : ℕ → α} → {p : α → Sort u_3} → (⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)) → ⦃n : ℕ⦄ → p (f n) → p (disjointed f n)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], Std.ExtDHashMap.Const.insertMany m [] = m
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.Atom₁ → m Lean.Expr) →
    (Mathlib.Tactic.BicategoryLike.Atom₁ →
        Mathlib.Tactic.BicategoryLike.WhiskerRight →
          Mathlib.Tactic.BicategoryLike.HorizontalComp →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
      (Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Mor₁ → m Lean.Expr) →
        (Mathlib.Tactic.BicategoryLike.Atom₁ →
            Mathlib.Tactic.BicategoryLike.Structural →
              Mathlib.Tactic.BicategoryLike.HorizontalComp →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
          (Mathlib.Tactic.BicategoryLike.Atom₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Structural →
                  Mathlib.Tactic.BicategoryLike.WhiskerLeft →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Mathlib.Tactic.BicategoryLike.NormalExpr →
                              Mathlib.Tactic.BicategoryLike.NormalExpr →
                                Mathlib.Tactic.BicategoryLike.NormalExpr →
                                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                                    Lean.Expr →
                                      Lean.Expr →
                                        Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
            (Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
              (Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m
-- Init.Data.String.Lemmas.FindPos
String.posGT_eq_next : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos} (h' : String.Pos.Raw.IsValid s p),
  s.posGT p h = (s.pos p h').next ⋯
-- Mathlib.Order.Interval.Set.Disjoint
IsLUB.iUnion_Iio_eq : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {a : α} {f : ι → α},
  IsLUB (Set.range f) a → ⋃ x, Set.Iio (f x) = Set.Iio a
-- Init.Data.Vector.Lemmas
Vector.findSomeM?_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Array α} (h : xs.size = n)
  (f : α → m (Option β)), Vector.findSomeM? f (Vector.mk xs h) = Array.findSomeM? f xs
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t.contains k = true → (cmp k t.max!).isLE = true
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzero_coe : ∀ {α : Type u} {x : α} (hx : ↑x ≠ 0), WithZero.unzero hx = x
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.List.takeWhile_eq_filter_of_pairwise : ∀ {α : Type u} {p : α → Bool} {l : List α},
  List.Pairwise (fun a b => p a = false → p b = false) l → List.takeWhile p l = List.filter p l
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Nat.toUInt32 5 = 5`
* `Nat.toUInt32 65_539 = 65_539`
* `Nat.toUInt32 4_294_967_299 = 3`
 -/
Nat.toUInt32 : ℕ → UInt32
-- Mathlib.Topology.Algebra.Monoid
ContinuousAdd.to_continuousVAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousVAdd M M
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.toArray_eq_toArray_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toArray = (Std.Slice.Internal.iter s).toArray
-- Mathlib.Data.DFinsupp.BigOperators
/-- `sum f g` is the sum of `g i (f i)` over the support of `f`.  -/
DFinsupp.sum : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → Zero (β i)] →
          [(i : ι) → (x : β i) → Decidable (x ≠ 0)] → [AddCommMonoid γ] → (Π₀ (i : ι), β i) → ((i : ι) → β i → γ) → γ
-- Lean.Elab.MutualDef
Lean.Elab.Term.warn.redundantExpose : Lean.Option Bool
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- If `s` and `t` are `μ`-a.e. disjoint, then `s \ u` and `t` are disjoint for some measurable null
set `u`.  -/
MeasureTheory.AEDisjoint.exists_disjoint_diff : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → ∃ u, MeasurableSet u ∧ μ u = 0 ∧ Disjoint (s \ u) t
-- Mathlib.Order.Atoms
Set.OrdConnected.isStronglyCoatomic : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyCoatomic α] {s : Set α}, s.OrdConnected → IsStronglyCoatomic ↑s
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_mul : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] (x y : R),
  ArchimedeanClass.mk (x * y) = ArchimedeanClass.mk x + ArchimedeanClass.mk y
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- `f : X ⟶ Y` is left homotopic to itself relative to any precylinder.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.refl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → (P : HomotopicalAlgebra.Precylinder X) → {Y : C} → (f : X ⟶ Y) → P.LeftHomotopy f f
-- Mathlib.Topology.EMetricSpace.Basic
/-- ε-δ characterization of uniform embeddings on pseudoemetric spaces  -/
EMetric.isUniformEmbedding_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveCoyonedaObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C) {X_1 Y : C}
  (f : X_1 ⟶ Y),
  (CategoryTheory.preadditiveCoyonedaObj X).map f =
    ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp g f, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.mk.sizeOf_spec : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} [inst_1 : SizeOf H] [inst_2 : SizeOf M]
  (atlas : Set (PartialEquiv M H)) (chartAt : M → PartialEquiv M H)
  (mem_chart_source : ∀ (x : M), x ∈ (chartAt x).source) (chart_mem_atlas : ∀ (x : M), chartAt x ∈ atlas)
  (open_source : ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source)
  (continuousOn_toFun :
    ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source),
  sizeOf
      { atlas := atlas, chartAt := chartAt, mem_chart_source := mem_chart_source, chart_mem_atlas := chart_mem_atlas,
        open_source := open_source, continuousOn_toFun := continuousOn_toFun } =
    1
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instSMul : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieRingModule L N] →
                        [inst_8 : LieAlgebra R L] → [LieModule R L N] → SMul R (M →ₗ⁅R,L⁆ N)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring is closed under addition.  -/
Subring.add_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s
-- Batteries.Control.AlternativeMonad
AlternativeMonad.toBind : {m : Type u_1 → Type u_2} → [self : AlternativeMonad m] → Bind m
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.natDegree 0 = 0
-- Mathlib.Order.Filter.Pi
/-- The indexed product of finitely many principal filters
is the principal filter corresponding to the cylinder `Set.univ.pi s`.

If the index type is infinite, then `mem_pi_principal` and `hasBasis_pi_principal` may be useful.  -/
Filter.pi_principal : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] (s : (i : ι) → Set (α i)),
  (Filter.pi fun i => Filter.principal (s i)) = Filter.principal (Set.univ.pi s)
-- Init.Data.Order.Lemmas
Std.max_eq_or : ∀ {α : Type u} [inst : Max α] [Std.MaxEqOr α] {a b : α}, a ⊔ b = a ∨ a ⊔ b = b
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLiftUnit_desc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] (s : CategoryTheory.Bicategory.LeftLift f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g)
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanLiftDesc s) f) =
    s.unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_alter!_eq_isEmpty_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty =
        ((Std.DTreeMap.Internal.Impl.erase! k t).isEmpty && (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.aestronglyMeasurable_on_iff : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G]
  {β : Type u_6} [inst_6 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ {f : α → β},
        (∀ (g : G) (x : α), f (g +ᵥ x) = f x) →
          (MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict t))
-- Mathlib.Tactic.ClickSuggestions.Util
_private.Mathlib.Tactic.ClickSuggestions.Util.0.Mathlib.Tactic.ClickSuggestions.kabstractFindsPositions.visit : Lean.Expr → Lean.SubExpr.Pos → Lean.HeadIndex → ℕ → IO.Ref Bool → Lean.Expr → Lean.SubExpr.Pos → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Prod
AddUnits.embedProduct_injective : ∀ (α : Type u_6) [inst : AddMonoid α], Function.Injective ⇑(AddUnits.embedProduct α)
-- Init.Data.Range.Polymorphic.Iterators
Std.Rio.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.Least? α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] {r : Std.Rio α} {a : α},
  (Std.Rio.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- Given a class of morphisms `P`, this is the class of pushouts
of morphisms in `P`.  -/
CategoryTheory.MorphismProperty.pushouts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.Red.reduce_right : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₁ (FreeGroup.reduce L₂)
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent.map_apply_coe : ∀ {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module A M₁] [inst_4 : Module A M₂] (φ : M₁ →ₗ[A] M₂)
  (c : ↥(Ideal.primaryComponent M₁ I)), ↑((Ideal.primaryComponent.map I φ) c) = φ ↑c
-- Mathlib.Control.Traversable.Instances
List.traverse_eq_map_id : ∀ {α β : Type u_1} (f : α → β) (x : List α), List.traverse (pure ∘ f) x = pure (f <$> x)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.of_map : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {c : NNReal} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {κ : ProbabilityTheory.Kernel Ω' Ω''} {Y : Ω'' → Ω}
  {X : Ω → ℝ},
  Measurable Y →
    ProbabilityTheory.Kernel.HasSubgaussianMGF X c (κ.map Y) ν →
      ProbabilityTheory.Kernel.HasSubgaussianMGF (X ∘ Y) c κ ν
-- Init.Data.String.Bootstrap
String.Internal.length : String → ℕ
-- Mathlib.Order.KrullDimension
Order.length_le_height : ∀ {α : Type u_1} [inst : Preorder α] {p : LTSeries α} {x : α}, RelSeries.last p ≤ x → ↑p.length ≤ Order.height x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_erase_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl k fallback = fallback
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a right lift is a Kan lift across an isomorphism of lifts.  -/
CategoryTheory.Bicategory.RightLift.IsAbsKan.ofIsoAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.RightLift f g} → s.IsAbsKan → (s ≅ t) → t.IsAbsKan
-- Mathlib.Order.Category.BoolAlg
BoolAlg.of.injEq : ∀ (carrier : Type u_1) [str : BooleanAlgebra carrier] (carrier_1 : Type u_1) (str_1 : BooleanAlgebra carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.forget_obj : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (X : F.CoGrothendieck),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).obj X = X.base
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Mon D)),
  (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).X = F.comp (CategoryTheory.Mon.forget D)
-- Mathlib.Algebra.Order.Quantale
IsQuantale.mk : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α],
  (∀ (x : α) (s : Set α), x * sSup s = ⨆ y ∈ s, x * y) →
    (∀ (s : Set α) (y : α), sSup s * y = ⨆ x ∈ s, x * y) → IsQuantale α
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
completedRiemannZeta₀_zero : completedRiemannZeta₀ 0 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2 + 1
-- Mathlib.Algebra.Group.Conj
AddConjClasses.forall_isAddConj : ∀ {α : Type u} [inst : AddMonoid α] {p : AddConjClasses α → Prop},
  (∀ (a : AddConjClasses α), p a) ↔ ∀ (a : α), p (AddConjClasses.mk a)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_mul_sqrt_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_mul_sqrt_self._auto_1 → CFC.sqrt a * CFC.sqrt a = a
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.refl_homotopyHomInvId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c), (HomotopyEquiv.refl C).homotopyHomInvId = Homotopy.ofEq ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C)
  [inst_5 : CategoryTheory.Limits.HasBiproduct f] [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F] {W : C}
  (g : (j : J) → f j ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.mapBiproduct f).hom
      (CategoryTheory.Limits.biproduct.desc fun j => F.map (g j)) =
    F.map (CategoryTheory.Limits.biproduct.desc g)
-- Batteries.Classes.Order
Std.LawfulCmp.toTransCmp : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {cmp : α → α → Ordering} [self : Std.LawfulCmp cmp], Std.TransCmp cmp
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
_private.Mathlib.Combinatorics.Enumerative.Partition.Glaisher.0.Nat.Partition.aux_mul_one_sub_X_pow : ∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommRing R] [NoZeroDivisors R] [IsTopologicalRing R]
  {m : ℕ},
  0 < m →
    (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1) *
        ∏' (i : ℕ), (1 - PowerSeries.X ^ (i + 1)) =
      ∏' (i : ℕ), (1 - PowerSeries.X ^ ((i + 1) * m))
-- Mathlib.Topology.NhdsWithin
eventually_nhds_subtype_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop),
  (∀ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∀ᶠ (x : α) in nhdsWithin (↑a) s, P x
-- Mathlib.Algebra.Ring.Center
Set.ofNat_mem_center : ∀ (M : Type u_1) [inst : NonAssocSemiring M] (n : ℕ) [inst_1 : n.AtLeastTwo], OfNat.ofNat n ∈ Set.center M
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.mem_map_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  {f : α →o β} {b : β}, b ∈ c.map f ↔ ∃ a ∈ c, f a = b
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depthLB.match_1.eq_2 : ∀ (motive : RBTree.RBColor → ℕ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive RBTree.RBColor.red n)
  (h_2 : (n : ℕ) → motive RBTree.RBColor.black n),
  (match RBTree.RBColor.black, n with
    | RBTree.RBColor.red, n => h_1 n
    | RBTree.RBColor.black, n => h_2 n) =
    h_2 n
-- Mathlib.Order.Hom.Lattice
InfHom.symm_dual_id : ∀ {α : Type u_2} [inst : Min α], InfHom.dual.symm (SupHom.id αᵒᵈ) = InfHom.id α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.legend : Lean.Lsp.SemanticTokensOptions → Lean.Lsp.SemanticTokensLegend
-- Mathlib.Topology.Algebra.UniformMulAction
/-- If a scalar action is central, then its right action is uniform continuous when its left action
is.  -/
UniformContinuousConstSMul.op : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : SMul M X] [inst_2 : SMul Mᵐᵒᵖ X] [IsCentralScalar M X]
  [UniformContinuousConstSMul M X], UniformContinuousConstSMul Mᵐᵒᵖ X
-- Mathlib.Analysis.Calculus.FDeriv.Star
HasFDerivAt.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E}
  [inst_9 : TrivialStar 𝕜], HasFDerivAt f f' x → HasFDerivAt (fun x => star (f x)) (↑(starL' 𝕜) ∘SL f') x
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [inst_1 : SizeOf C]
  (fiber : CategoryTheory.Functor C (Type w))
  (isCofiltered :
    autoParam (CategoryTheory.IsCofiltered fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam)
  (initiallySmall :
    autoParam (CategoryTheory.InitiallySmall fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam)
  (jointly_surjective :
    ∀ {X : C},
      ∀ R ∈ J X,
        ∀ (x : fiber.obj X), ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber.map f)) y = x),
  sizeOf
      { fiber := fiber, isCofiltered := isCofiltered, initiallySmall := initiallySmall,
        jointly_surjective := jointly_surjective } =
    1 + sizeOf fiber + sizeOf isCofiltered + sizeOf initiallySmall
-- Mathlib.Logic.Equiv.Basic
/-- If `α` is equivalent to `β`, then `IsEmpty α` is equivalent to `IsEmpty β`.  -/
Equiv.isEmpty_congr : ∀ {α : Sort u_1} {β : Sort u_4} (e : α ≃ β), IsEmpty α ↔ IsEmpty β