mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.MulAction
smul_set_closure_subset : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] (K : Set M) (L : Set X), closure K • closure L ⊆ closure (K • L)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.zero_smul : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N), 0 • f = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_coe_coe : ∀ (a b : ℝ), ContinuousAt (fun p => p.1 * p.2) (↑a, ↑b)
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.map_id : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (k : ℕ)
  (A : CommAlgCat R) (N : Module.Grassmannian (↑A) (TensorProduct R (↑A) M) k),
  Module.Grassmannian.map (AlgHom.id R ↑A) N = N
-- Mathlib.Analysis.Calculus.FDeriv.Prod
Differentiable.finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  Differentiable 𝕜 φ → Differentiable 𝕜 φs → Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- An alternative definition of the sheaf condition in terms of equalizers. This is shown to be
equivalent in `CategoryTheory.Presheaf.isSheaf_iff_isSheaf'`.
 -/
CategoryTheory.Presheaf.IsSheaf' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        CategoryTheory.GrothendieckTopology C →
          [CategoryTheory.Limits.HasProducts A] →
            [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Functor Cᵒᵖ A → Prop
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive cancel commutative monoid if it
admits an injective map that preserves `0` and `+` to an additive cancel commutative monoid.  -/
Function.Injective.addCancelCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddCancelCommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) →
                    (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddCancelCommMonoid M₁
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) h))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Lax.OplaxTrans.vCompNaturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          (η : CategoryTheory.Lax.OplaxTrans F G) →
            (θ : CategoryTheory.Lax.OplaxTrans G H) →
              {a b : B} →
                (f : a ⟶ b) →
                  CategoryTheory.CategoryStruct.comp (F.map f)
                      (CategoryTheory.CategoryStruct.comp (η.app b) (θ.app b)) ⟶
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a))
                      (H.map f)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.congr_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D},
  f = g → ∀ (i : ι), f.f i = g.f i
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.whenPPOption : (Lean.Options → Bool) → Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is `eq`.
 -/
Ordering.isEq : Ordering → Bool
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.dpow_span_isSubideal : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A},
  S ⊆ ↑I → Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable δ] {R : γ → δ → Prop} {f : α → β → γ} {g : α → β → δ},
  PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun a b => R (f a b) (g a b)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_pow_eq_natCast_mul : ∀ {R : Type u} [inst : CommSemiring R] (n k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
-- Mathlib.Data.List.OfFn
List.ofFn_congr : ∀ {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α), List.ofFn f = List.ofFn fun i => f (Fin.cast ⋯ i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.leadingCoeff_cons_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R},
  P.nextCoeff ≠ 0 → P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOptionValue : Inhabited Lean.LeanOptionValue
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y), (CategoryTheory.Subobject.functor C).map f = TypeCat.ofHom (CategoryTheory.Subobject.pullback f.unop).obj
-- Lean.Data.NameMap.Basic
Lean.NameHashSet.insert : Lean.NameHashSet → Lean.Name → Std.HashSet Lean.Name
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (E.p₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) =
    CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.eqToHom ⋯)
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a Boolean algebra is a set containing the bottom and top elements, and
closed under suprema, infima and complements.  -/
BooleanSubalgebra : (α : Type u_2) → [BooleanAlgebra α] → Type u_2
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNonUnitalCommSemiring : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [NonUnitalCommSemiring Y] → NonUnitalCommSemiring (LocallyConstant X Y)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given a walk, produces a walk from it by bypassing subwalks between repeated vertices.
The result is a path, as shown in `SimpleGraph.Walk.bypass_isPath`.
This is packaged up in `SimpleGraph.Walk.toPath`.  -/
SimpleGraph.Walk.bypass : {V : Type u} → {G : SimpleGraph V} → [DecidableEq V] → {u v : V} → G.Walk u v → G.Walk u v
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `b.reindex (e : ι ≃ ι')` is a basis indexed by `ι'`  -/
Module.Basis.reindex : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      {M : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → ι ≃ ι' → Module.Basis ι' R M
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.checkTerminalAsSorry : Lean.MVarId → Lean.Elab.Tactic.TacticM Bool
-- Lean.Elab.Tactic.Monotonicity
Lean.Meta.Monotonicity.defaultFailK : {α : Type} → Lean.Expr → Array Lean.Name → Lean.MetaM α
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.sUnion_countablePartition : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ),
  ⋃₀ MeasurableSpace.countablePartition α n = Set.univ
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_symm_apply_packingRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet Y),
  ((Delone.DeloneSet.mapIsometry f).symm D).packingRadius = D.packingRadius
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.map_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β},
  RightOrdContinuous f → ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of June.
 -/
Std.Time.Month.Ordinal.june : Std.Time.Month.Ordinal
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne'.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (N : Submodule R S),
  N.lTensorOne' =
    ↑(LinearEquiv.ofEq ((Subalgebra.toSubmodule ⊥).mulMap N).range N ⋯) ∘ₗ
      ((Subalgebra.toSubmodule ⊥).mulMap N).rangeRestrict
-- Std.Http.Data.Headers
Std.Http.Headers.mk.injEq : ∀ (map map_1 : Std.Internal.IndexMultiMap Std.Http.Header.Name Std.Http.Header.Value),
  ({ map := map } = { map := map_1 }) = (map = map_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.keysArray.toList = m.keys
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.mk.sizeOf_spec : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} [inst_1 : SizeOf ι]
  [inst_2 : SizeOf X] [inst_3 : (a : X) → SizeOf (s a)] (toFun : ι → C(X, ℝ))
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : 0 ≤ toFun) (le_one' : toFun ≤ 1)
  (eventuallyEq_one' : ∀ x ∈ s, ∃ i, ⇑(toFun i) =ᶠ[nhds x] 1),
  sizeOf
      { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', le_one' := le_one',
        eventuallyEq_one' := eventuallyEq_one' } =
    1
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mem_sInf : ∀ {M : Type u_1} [inst : MulOneClass M] {f : Set (SaturatedSubmonoid M)} {x : M}, x ∈ sInf f ↔ ∀ s ∈ f, x ∈ s
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.zero_mem_iff : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  0 ∈ spectrum R a ↔ ¬IsUnit a
-- Init.Data.Slice.Operations
/-- Folds an operation from left to right over the elements in a slice.
An accumulator of type `β` is constructed by starting with `init` and combining each
element of the slice with the current accumulator value in turn.
Examples for the special case of subarrays:
 * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
 * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
 -/
Std.Slice.foldl : {α : Type v} →
  {γ : Type u} →
    {β : Type v} →
      {δ : Type w} →
        (δ → β → δ) →
          δ →
            [Std.ToIterator (Std.Slice γ) Id α β] →
              [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Slice γ → δ
-- Init.Data.UInt.Lemmas
UInt64.mul_assoc : ∀ (a b c : UInt64), a * b * c = a * (b * c)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_inv_apply : ∀ {X Y : BddOrd} (e : X ≅ Y) (s : ↑Y.toPartOrd),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filter f m) k =
        (Option.filter (fun x => f k' x) (Std.DHashMap.Raw.Const.get? m k)).get!
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mk.injEq : ∀ {R : Type u_7} {S : Type u_8} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (gen : S) (dim : ℕ)
  (basis : Module.Basis (Fin dim) R S) (basis_eq_pow : ∀ (i : Fin dim), basis i = gen ^ ↑i) (gen_1 : S) (dim_1 : ℕ)
  (basis_1 : Module.Basis (Fin dim_1) R S) (basis_eq_pow_1 : ∀ (i : Fin dim_1), basis_1 i = gen_1 ^ ↑i),
  ({ gen := gen, dim := dim, basis := basis, basis_eq_pow := basis_eq_pow } =
      { gen := gen_1, dim := dim_1, basis := basis_1, basis_eq_pow := basis_eq_pow_1 }) =
    (gen = gen_1 ∧ dim = dim_1 ∧ basis ≍ basis_1)
-- Mathlib.NumberTheory.Padics.Complex
/-- The underlying metric space of `PadicAlgCl p` is ultrametric.  -/
PadicAlgCl.isUltrametricDist : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsUltrametricDist (PadicAlgCl p)
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff_le : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b \ (b \ a) ≤ a
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.categoryFormatter : Lean.Name → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac._auto_1)
  [inst_3 : CategoryTheory.Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
  [inst_4 : CategoryTheory.Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer k ⋯).hom
        (CategoryTheory.Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯))) =
    S.map' (k + 1) (k + 2) ⋯ ⋯
-- Init.Data.UInt.Lemmas
USize.ofNatLT.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n < USize.size), USize.ofNatLT n h = USize.ofNatLT n_1 ⋯
-- Init.Control.Lawful.MonadLift.Instances
instLawfulMonadLiftTOfLawfulMonadLift : ∀ (m : Type u → Type v) (n : Type u → Type w) (o : Type u → Type x) [inst : Monad m] [inst_1 : Monad n]
  [inst_2 : Monad o] [inst_3 : MonadLift n o] [inst_4 : MonadLiftT m n] [LawfulMonadLift n o] [LawfulMonadLiftT m n],
  LawfulMonadLiftT m o
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryRightEquiv_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G)
  (v : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)),
  (((continuousMultilinearCurryRightEquiv 𝕜 Ei G) f) v) x = f (Fin.snoc v x)
-- Std.Time.Format.Modifier
/-- `F`: Day-of-week-in-month / occurrence of the weekday within the month (e.g., 2nd Sunday -> 2).
 -/
Std.Time.Modifier.F : Std.Time.Number → Std.Time.Modifier
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.adj_comm : ∀ {α : Type u_1} {H : Hypergraph α} (x y : α), H.Adj x y ↔ H.Adj y x
-- Init.Control.StateRef
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value paired with the final state.

The monad `m` must support `ST` effects in order to create and mutate reference cells.
 -/
StateRefT'.run : {ω σ : Type} → {m : Type → Type} → [Monad m] → [MonadLiftT (ST ω) m] → {α : Type} → StateRefT' ω σ m α → σ → m (α × σ)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The ring of integers of `adicCompletion`.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                ValuationSubring (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.PulledChunk.mk.sizeOf_spec : ∀ (final incomplete : Bool) (chunk : Std.Http.Chunk),
  sizeOf { final := final, incomplete := incomplete, chunk := chunk } =
    1 + sizeOf final + sizeOf incomplete + sizeOf chunk
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian
are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : Type u_4} {X : S → Ω → ℝ}
  {Y : T → Ω → ℝ},
  ProbabilityTheory.IsGaussianProcess (Sum.elim X Y) P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (t : T), AEMeasurable (Y t) P) →
        (∀ (s : S) (t : T), ProbabilityTheory.covariance (X s) (Y t) P = 0) →
          ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedAddCommGroup.negGen_eq_of_top : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : Nontrivial G] [inst_4 : IsAddCyclic G],
  LinearOrderedAddCommGroup.negGen G = LinearOrderedAddCommGroup.Subgroup.negGen ⊤
-- Init.Control.Lawful.Instances
ExceptT.run_adapt : ∀ {m : Type u_1 → Type u_2} {ε ε' α : Type u_1} [inst : Monad m] (f : ε → ε') (x : ExceptT ε m α),
  (ExceptT.adapt f x).run = Except.mapError f <$> x.run
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedErrorCode.default : Lean.JsonRpc.ErrorCode
-- Mathlib.Order.Disjoint
IsCompl.sup_eq_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → x ⊔ y = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.mem_finsetWalkLength_iff : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v},
  p ∈ G.finsetWalkLength n u v ↔ p.length = n
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.homologyπ_restrictionHomologyIso_hom_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j] {Z : C}
  (h : K.homology j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyπ j)
      (CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom h) =
    CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom
      (CategoryTheory.CategoryStruct.comp (K.homologyπ j') h)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.crossing_eq_crossing_of_lowerCrossingTime_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω} {M : ℕ},
  N ≤ M →
    MeasureTheory.lowerCrossingTime a b f N n ω < N →
      MeasureTheory.upperCrossingTime a b f M n ω = MeasureTheory.upperCrossingTime a b f N n ω ∧
        MeasureTheory.lowerCrossingTime a b f M n ω = MeasureTheory.lowerCrossingTime a b f N n ω
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.vadd_of_tower_def : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S)
  (r : M) (x : ↥s), r +ᵥ x = ⟨r +ᵥ ↑x, ⋯⟩
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_41 : HSub Std.Time.Week.Offset Std.Time.Day.Offset Std.Time.Day.Offset
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Variant of `AlgebraicGeometry.localRingHom_comp_stalkIso` for `Spec.map`.  -/
AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S)
  (x : ↑((AlgebraicGeometry.Spec R).presheaf.stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Spec.stalkIso S p).inv)
      ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯)
        ((CategoryTheory.ConcreteCategory.hom
            (AlgebraicGeometry.Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom)
          x)) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p)) x
-- Mathlib.Algebra.Group.Action.Pi
Set.piecewise_smul : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (s : Set ι)
  [inst_1 : (i : ι) → Decidable (i ∈ s)] (c : M) (f₁ g₁ : (i : ι) → α i),
  s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `A` is flat, then for any family of
`R`-linearly independent elements `{ a_i }` of `A`, and any family of
`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is
also `R`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥A] {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B},
      LinearIndependent R a → LinearIndependent R b → LinearIndependent R fun i => ↑(a i.1) * ↑(b i.2)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.forall_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s →
    ∀ {P : Set α → Prop}, (∀ ⦃s t : Set α⦄, s ⊆ t → P s → P t) → ((∀ s ∈ l, P s) ↔ ∀ (i : ι), p i → P (s i))