mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Finiteness.Nakayama
/-- **Nakayama's Lemma**. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2.  -/
Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M), N.FG → N ≤ I • N → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The subspaces of a projective space form a complete lattice.  -/
Projectivization.Subspace.instCompleteLattice : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → CompleteLattice (Projectivization.Subspace K V)
-- Mathlib.CategoryTheory.Action.Basic
Action.instIsIsoHomInv : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N), CategoryTheory.IsIso f.inv.hom
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.induction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    AlgebraicTopology.DoldKan.HigherFacesVanish (q + 1)
      (CategoryTheory.CategoryStruct.comp φ
        ((CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X) +
              AlgebraicTopology.DoldKan.Hσ q).f
          (n + 1)))
-- Lean.Parser.Command
Lean.Parser.Term.open.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V],
  SpecialLinearGroup.centerEquivRootsOfUnity =
    {
      toFun := fun g =>
        ⋯.by_cases (fun x => 1) fun hR =>
          ⋯.by_cases (fun x => 1) fun hV =>
            have hV := ⋯;
            have hr := ⋯;
            let r := ⋯.choose;
            have this := ⋯;
            ⟨this.unit, ⋯⟩,
      invFun := SpecialLinearGroup.centerEquivRootsOfUnity_invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.mkContinuous_coe : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ↑(f.mkContinuous C h) = f
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClass_closedBall_circle : SMulCommClass Complex.UnitClosedDisc Circle Complex.UnitDisc
-- Mathlib.Order.Heyting.Basic
hnot_sup_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ￢a ⊔ a = ⊤
-- Mathlib.Control.Traversable.Equiv
Equiv.traverse.eq_1 : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] {m : Type u → Type u}
  [inst_1 : Applicative m] {α β : Type u} (f : α → m β) (x : t' α),
  Equiv.traverse eqv f x = ⇑(eqv β) <$> traverse f ((eqv α).symm x)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_X_of_ne : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i j : σ}, j ≠ i → (MvPolynomial.pderiv i) (MvPolynomial.X j) = 0
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ⟶ G.obj X)
  (naturality :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f))
      CategoryTheory.NatTrans.naturality._autoParam)
  (app_1 : (X : C) → F.obj X ⟶ G.obj X)
  (naturality_1 :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app_1 Y) = CategoryTheory.CategoryStruct.comp (app_1 X) (G.map f))
      CategoryTheory.NatTrans.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_const : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (g : G),
  (fwdDiff h fun x => g) = fun x => 0
-- Mathlib.Order.Lattice.Nat
Nat.sSup_mem : ∀ {s : Set ℕ}, s.Nonempty → BddAbove s → sSup s ∈ s
-- Mathlib.Order.RelSeries
RelSeries.head_append : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r),
  (p.append q connect).head = p.head
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.attachJPs : Array Lean.Elab.Term.Do.JPDecl → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Subsingleton.measurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [Subsingleton α],
  Measurable f
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Ideal.isPrime_map_of_isLocalizationAtPrime : ∀ {R : Type u_1} [inst : CommSemiring R] (q : Ideal R) [inst_1 : q.IsPrime] {S : Type u_4} [inst_2 : CommSemiring S]
  [inst_3 : Algebra R S] [IsLocalization.AtPrime S q] {p : Ideal R} [p.IsPrime],
  p ≤ q → (Ideal.map (algebraMap R S) p).IsPrime
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.ext' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂},
  (∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) → g = h
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- If `C` has finite limits then it has finite products.  -/
CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instInhabited.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M], SubAddAction.instInhabited = { default := ⊥ }
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.const_apply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetOne] (x : ℂ) (τ : UpperHalfPlane), (ModularForm.const x) τ = x
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_sup_ker_eq_map' : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  LieIdeal.map f I ⊔ LieIdeal.map f f.ker = LieIdeal.map f I
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α}, s +ᵥ ∅ = ∅
-- Mathlib.Algebra.CharP.Frobenius
RingHom.map_iterate_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (g : R →+* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R) (n : ℕ),
  g ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (g x)
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- `Idx` identifies a location inside the application of a polynomial functor. For `F : PFunctor`,
`x : F α` and `i : F.Idx`, `i` can designate one part of `x` or is invalid, if `i.1 ≠ x.1`.  -/
PFunctor.Idx : PFunctor.{uA, uB} → Type (max uA uB)
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  {homRel : HomRel C} [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel]
  [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] [W.HasQuotient homRel] {X Y : C} {f g : X ⟶ Y},
  Relation.EqvGen homRel f g → (W f ↔ W g)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.insert : {α : Type} → {x : Hashable α} → {x_1 : BEq α} → Lean.Meta.Try.Collector.OrdSet α → α → Lean.Meta.Try.Collector.OrdSet α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.max? = some km → t.contains km = true
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
-- Init.Data.SInt.Lemmas
Int16.toInt_div_of_ne_left : ∀ (a b : Int16), a ≠ Int16.minValue → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mk : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Filter.Tendsto f Filter.cofinite Filter.cofinite → Filter.TendstoCofinite f
-- Mathlib.Topology.Order.DenselyOrdered
/-- `Set.Ioo a b` is only closed if it is empty.  -/
isClosed_Ioo_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsClosed (Set.Ioo a b) ↔ b ≤ a
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smulDistribClass : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_4} {S : Type u_5} [inst : SMul M' α] [inst_1 : SMul M' β]
  [inst_2 : SMul α β] [inst_3 : SetLike S M'] [h : SMulDistribClass M' α β] (N' : S), SMulDistribClass (↥N') α β
-- Init.Data.UInt.Lemmas
UInt8.mod_eq_of_lt : ∀ {a b : UInt8}, a < b → a % b = a
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.replace.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (b : β a) (a_1 : α) (b_1 : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.replace a b (Std.DHashMap.Internal.AssocList.cons a_1 b_1 es) =
    bif a_1 == a then Std.DHashMap.Internal.AssocList.cons a b es
    else Std.DHashMap.Internal.AssocList.cons a_1 b_1 (Std.DHashMap.Internal.AssocList.replace a b es)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- The "μₗ" morphism.  -/
CategoryTheory.Functor.LaxLeftLinear.μₗ : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        (F : CategoryTheory.Functor D D') →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} →
                    [self : F.LaxLeftLinear C] →
                      (c : C) →
                        (d : D) →
                          CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶
                            F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instLeftCancelSemigroup : {α : Type u_1} → [LeftCancelSemigroup α] → LeftCancelSemigroup (Colex α)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {B : ℝ},
  B ≤ 0 → MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = 0
-- Mathlib.Topology.Order.OrderClosed
iUnion_Iic_eq_Iio_of_lt_of_tendsto : ∀ {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α},
  (∀ (i : ι), f i < a) → Filter.Tendsto f F (nhds a) → ⋃ i, Set.Iic (f i) = Set.Iio a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproductsOfShape J C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C),
  CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.inv.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π fun j => X.obj { as := j }))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι fun j => X.obj { as := j }))
          (CategoryTheory.Limits.Sigma.isoColimit X).hom))
-- Init.Control.Basic
/-- A way to lift a computation from one monad to another while providing the lifted computation with a
means of interpreting computations from the outer monad. This provides a means of lifting
higher-order operations automatically.

Clients should typically use `control` or `controlAt`, which request an instance of `MonadControlT`:
the reflexive, transitive closure of `MonadControl`. New instances should be defined for
`MonadControl` itself.
 -/
MonadControlT : (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `GroupWithZero` along an injective function.
See note [reducible non-instances].  -/
Function.Injective.groupWithZero : {G₀ : Type u_2} →
  {G₀' : Type u_4} →
    [inst : GroupWithZero G₀] →
      [inst_1 : Zero G₀'] →
        [inst_2 : Mul G₀'] →
          [inst_3 : One G₀'] →
            [inst_4 : Inv G₀'] →
              [inst_5 : Div G₀'] →
                [inst_6 : Pow G₀' ℕ] →
                  [inst_7 : Pow G₀' ℤ] →
                    (f : G₀' → G₀) →
                      Function.Injective f →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : G₀'), f (x * y) = f x * f y) →
                              (∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) →
                                (∀ (x y : G₀'), f (x / y) = f x / f y) →
                                  (∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) →
                                    (∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) → GroupWithZero G₀'
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_reindex : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Star α] (eₘ : m ≃ l) (eₙ : n ≃ o)
  (M : Matrix m n α), ((Matrix.reindex eₘ eₙ) M).conjTranspose = (Matrix.reindex eₙ eₘ) M.conjTranspose
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_alt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_le_self : ∀ {r : ENNReal}, ↑⌊r⌋ₑ ≤ r
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.Turan.0.SimpleGraph.sum_ne_add_mod_eq_sub_one : ∀ {n r c : ℕ}, (∑ w ∈ Finset.range r, if c % r ≠ (n + w) % r then 1 else 0) = r - 1
-- Mathlib.Data.Sum.Basic
Sum.map_surjective : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ},
  Function.Surjective (Sum.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
-- Mathlib.Order.Minimal
/-- If two sets are order isomorphic, their minimals are also order isomorphic.  -/
OrderIso.mapSetOfPredMinimal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} → {t : Set β} → ↑s ≃o ↑t → ↑{x | Minimal (fun x => x ∈ s) x} ≃o ↑{x | Minimal (fun x => x ∈ t) x}
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.Equivalent.symm : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂}, B₁.Equivalent B₂ → B₂.Equivalent B₁
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_forall_le_4 : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ : Type v} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → l},
  Lean.Order.PartialOrder.rel P Q ↔
    ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), Lean.Order.PartialOrder.rel (P s₁ s₂ s₃ s₄) (Q s₁ s₂ s₃ s₄)
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_apply_inl_fst : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι), ((b.prod b') (Sum.inl i)).1 = b i
-- Batteries.Data.MLList.Basic
/-- Filter and transform a `MLList` using an `Option` valued function.  -/
MLList.filterMap : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [Monad m] → (α → Option β) → MLList m α → MLList m β
-- Std.Http.Data.Method
Std.Http.Method.uncheckout.sizeOf_spec : sizeOf Std.Http.Method.uncheckout = 1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_one : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint], CFC.log 1 = 0
-- Std.Internal.Do.PredTrans
/-- Unfolding lemma for `pushArg`: applies the state-threaded transformer at state `s`.  -/
Std.Internal.Do.PredTrans.apply_pushArg : ∀ {σ : Type u} {Pred : Type v} {EPred : Type w} {α : Type z} (x : σ → Std.Internal.Do.PredTrans Pred EPred (α × σ))
  (post : α → σ → Pred) (epost : EPred) (s : σ),
  (Std.Internal.Do.pushArg x).apply post epost s =
    (x s).apply
      (fun x =>
        match x with
        | (a, s) => post a s)
      epost
-- Std.Time.Format.DateFormat
/-- AM string (e.g., "AM").  -/
Std.Time.DayPeriodSymbols.am : Std.Time.DayPeriodSymbols → String
-- Init.Data.SInt.Lemmas
UInt8.toInt8_ofNat' : ∀ {n : ℕ}, (UInt8.ofNat n).toInt8 = Int8.ofNat n
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.tendsto_at : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s → ∀ {a : α}, a ∈ s → Filter.Tendsto (fun i => F i a) p (nhds (f a))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toLaxFunctor : CategoryTheory.LaxFunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam)
  (mapId_eq_eqToHom :
    autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam)
  (toLaxFunctor_1 : CategoryTheory.LaxFunctor B C)
  (map_id_1 :
    autoParam
      (∀ (X : B),
        toLaxFunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toLaxFunctor_1.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam)
  (mapId_eq_eqToHom_1 :
    autoParam (∀ (X : B), toLaxFunctor_1.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam),
  ({ toLaxFunctor := toLaxFunctor, map_id := map_id, mapId_eq_eqToHom := mapId_eq_eqToHom } =
      { toLaxFunctor := toLaxFunctor_1, map_id := map_id_1, mapId_eq_eqToHom := mapId_eq_eqToHom_1 }) =
    (toLaxFunctor = toLaxFunctor_1)
-- Mathlib.Order.Grade
GradeOrder.wellFoundedGT : ∀ {α : Type u_3} [inst : Preorder α] (𝕆 : Type u_5) [inst_1 : Preorder 𝕆] [GradeOrder 𝕆 α] [WellFoundedGT 𝕆],
  WellFoundedGT α
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- For `p ≠ 1`, the `p`-adic valuation of an integer `z ≠ 0` is the largest natural number `k` such
that `p^k` divides `z`. If `x = 0` or `p = 1`, then `padicValInt p q` defaults to `0`.  -/
padicValInt : ℕ → ℤ → ℕ
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.preimageDiagram.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C]
  {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
  (hF : ∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) (X : C)
  (y : (F.obj (Opposite.op 0)).obj.obj (Opposite.op X)),
  CategoryTheory.coherentTopology.preimageDiagram✝ hF X y =
    CategoryTheory.Functor.ofOpSequence
      (CategoryTheory.coherentTopology.struct.map✝ (CategoryTheory.coherentTopology.preimageStruct✝ hF X y))
-- Mathlib.RingTheory.SimpleRing.Congr
IsSimpleRing.of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] [Nontrivial S] (f : R →+* S),
  IsSimpleRing R → Function.Surjective ⇑f → IsSimpleRing S
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Lean.Parser.Command
Lean.Parser.Term.set_option.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Circular
CircularPartialOrder.toCircularPreorder : {α : Type u_1} → [self : CircularPartialOrder α] → CircularPreorder α
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
MonoidHom.compLeftContinuousBounded_apply : ∀ {β : Type v} {γ : Type w} (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : Monoid β] [inst_3 : BoundedMul β] [inst_4 : ContinuousMul β] [inst_5 : PseudoMetricSpace γ]
  [inst_6 : Monoid γ] [inst_7 : BoundedMul γ] [inst_8 : ContinuousMul γ] (g : β →* γ) {C : NNReal}
  (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β),
  (MonoidHom.compLeftContinuousBounded α g hg) f = BoundedContinuousFunction.comp (⇑g) hg f
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid : ∀ {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α], IsOrderedAddMonoid α
-- Mathlib.Combinatorics.SetFamily.LYM
/-- **Sperner's theorem**. The size of an antichain in `Finset α` is bounded by the size of the
maximal layer in `Finset α`. This precisely means that `Finset α` is a Sperner order.  -/
IsAntichain.sperner : ∀ {α : Type u_2} [inst : Fintype α] {𝒜 : Finset (Finset α)},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 → 𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)
-- Mathlib.Order.Partition.Basic
Partition.mem_removeBot : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] (P : Set α) (indep : sSupIndep P) (hsSup : sSup P = s),
  x ∈ Partition.removeBot P indep hsSup ↔ x ∈ P ∧ x ≠ ⊥
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  {fallback : β k}, (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).getD k fallback = fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : (t.getKey? a).isSome = true}, (t.getKey? a).get h = t.getKey a ⋯
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  μ.singularPart ν = 0 ↔ μ.AbsolutelyContinuous ν