mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.SymmDiff
Set.symmDiff_subset_union : ∀ {α : Type u} {s t : Set α}, symmDiff s t ⊆ s ∪ t
-- Lean.Message
Lean.MessageDataContext.mk.sizeOf_spec : ∀ (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options),
  sizeOf { env := env, mctx := mctx, lctx := lctx, opts := opts } =
    1 + sizeOf env + sizeOf mctx + sizeOf lctx + sizeOf opts
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_quotientOut : ∀ (α : Sort u_1) [inst : Setoid α], ⇑(Function.Embedding.quotientOut α) = Quotient.out
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- the objects of the localized category.  -/
CategoryTheory.MorphismProperty.HasLocalization.D : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    (W : CategoryTheory.MorphismProperty C) → [self : W.HasLocalization] → Type u
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYonedaHomEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X : C} {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A}
  (α : CategoryTheory.Presheaf.freeYoneda X M ⟶ F) (f : F ⟶ G),
  CategoryTheory.Presheaf.freeYonedaHomEquiv (CategoryTheory.CategoryStruct.comp α f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.freeYonedaHomEquiv α) (f.app (Opposite.op X))
-- Mathlib.Algebra.Order.Field.GeomSum
geom_sum_of_one_lt : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K]
  [inst_4 : Sub K] [OrderedSub K] {x : K}, 1 < x → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)
-- Mathlib.SetTheory.Cardinal.Subfield
_private.Mathlib.SetTheory.Cardinal.Subfield.0.Subfield.Operands : {α : Type u} → (s : Set α) → Fin 6 ⊕ ↑s → Type
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousWithinAt_iff_forall_isOpen`. -/
UpperHemicontinuousWithinAt.of_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α}
  [inst_1 : TopologicalSpace β],
  (∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u) → UpperHemicontinuousWithinAt f s x
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.coe_comp : ∀ {X Y Z : AddCommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Order.Disjoint
Disjoint.eq_bot : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ⊓ b = ⊥
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.some_minEntry_eq_minEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β} {he : l.isEmpty = false},
  some (Std.DTreeMap.Internal.Impl.Const.minEntry l he) = Std.DTreeMap.Internal.Impl.Const.minEntry? l
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv_left`. -/
MonovaryOn.of_inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f⁻¹ g s → AntivaryOn f g s
-- Mathlib.Computability.Partrec
Partrec.map : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α →. β} {g : α → β → σ}, Partrec f → Computable₂ g → Partrec fun a => Part.map (g a) (f a)
-- Mathlib.Algebra.Torsor.Basic
vadd_vsub_vadd_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (v₁ v₂ : G) (p₁ p₂ : P),
  (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = v₁ - v₂ + (p₁ -ᵥ p₂)
-- Std.Data.Iterators.Producers.Monadic.Array
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.ArrayIterator.pos : {α : Type w} → Std.Iterators.Types.ArrayIterator α → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_pos : ∀ {a b c d : ℤ}, b < 0 → 0 < d → b ∣ a → d ∣ c → (a / b < c / d ↔ c * b < d * a)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₁.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont'),
  sizeOf (Turing.PartrecToTM2.Cont'.cons₁ a a_1) = 1 + sizeOf a + sizeOf a_1
-- Lean.Server.FileWorker.InlayHints
_private.Lean.Server.FileWorker.InlayHints.0.Lean.Server.FileWorker.handleInlayHintsDidChange.updateOldInlayHints : Lean.Lsp.DidChangeTextDocumentParams →
  Array Lean.Elab.InlayHintInfo → Lean.Server.RequestM (Array Lean.Elab.InlayHintInfo)
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux.eq_def : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x)
  (x_3 : CategoryTheory.FreeBicategory.Hom x x_1),
  CategoryTheory.FreeBicategory.normalizeAux x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | x, x_4, p, CategoryTheory.FreeBicategory.Hom.of f => p.cons f
    | x, .(x), p, CategoryTheory.FreeBicategory.Hom.id .(x) => p
    | x, x_4, p, f.comp g =>
      CategoryTheory.FreeBicategory.normalizeAux (CategoryTheory.FreeBicategory.normalizeAux p f) g
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.coe_restrOpen_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s), ↑(e.restrOpen s hs).symm = ↑e.symm
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey? k = none
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.index.eq_def : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (x : Ordinal.{u}),
  p.index x =
    have i := x;
    have Z := ⋃ j, Metric.ball (p.c (p.index ↑j)) (p.r (p.index ↑j));
    have R := ⨆ b, p.r ↑b;
    Classical.epsilon fun b => p.c b ∉ Z ∧ R ≤ p.τ * p.r b
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.mk : ∀ {α : Type u_3} [t : TopologicalSpace α] [inst : Preorder α], t = Topology.lower α → Topology.IsLower α
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instCreatesLimitsOfSizeForget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.CreatesLimitsOfSize.{w, u_1, v, v, max u v, u} (CategoryTheory.Mon.forget C)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.coind₁ι_app : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type v} [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (rep : TopRep k G),
  TopRep.coind₁ι.app rep = TopRep.ofHom rep.ρ.coind₁ι
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.union_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ ∪ m₂).Equiv (m₁ ∪ m₃)
-- Mathlib.Algebra.Ring.Defs
IsDomain.toIsCancelMulZero : ∀ {α : Type u} {inst : Semiring α} [self : IsDomain α], IsCancelMulZero α
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- The mates equivalence commutes with horizontal composition of squares.  -/
CategoryTheory.mateEquiv_hcomp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] [inst_3 : CategoryTheory.Category.{v₄, u₄} D]
  [inst_4 : CategoryTheory.Category.{v₅, u₅} E] [inst_5 : CategoryTheory.Category.{v₆, u₆} F]
  {G : CategoryTheory.Functor A D} {H : CategoryTheory.Functor B E} {K : CategoryTheory.Functor C F}
  {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor D E}
  {R₂ : CategoryTheory.Functor E D} {L₃ : CategoryTheory.Functor B C} {R₃ : CategoryTheory.Functor C B}
  {L₄ : CategoryTheory.Functor E F} {R₄ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃)
  (adj₄ : L₄ ⊣ R₄) (α : CategoryTheory.TwoSquare G L₁ L₂ H) (β : CategoryTheory.TwoSquare H L₃ L₄ K),
  (CategoryTheory.mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α.vComp β) =
    ((CategoryTheory.mateEquiv adj₃ adj₄) β).hComp ((CategoryTheory.mateEquiv adj₁ adj₂) α)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_sInf : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)), (sInf S).unop = sInf (Submonoid.op ⁻¹' S)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (n : σ), (MvPolynomial.X n).degrees = {n}
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_add_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddLeftInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => g + x) μ μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, Std.DTreeMap.Internal.Impl.contains (t.minKeyD fallback) t = true
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.le_sum_card_subset_chunk_parts : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {𝒜 : Finset (Finset α)}
  {s : Finset α},
  𝒜 ⊆ (SzemerediRegularity.chunk hP G ε hU).parts →
    s ∈ 𝒜 →
      ↑𝒜.card * ↑s.card *
          (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) /
            (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)) ≤
        ↑(𝒜.sup id).card
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k fallback : α},
  m.WF → (Std.HashSet.Raw.filter f m).getD k fallback = (Option.filter f (m.get? k)).getD fallback
-- Mathlib.Data.Fin.Fin2
Fin2.last.eq_1 : Fin2.last = Fin2.fz
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.mk : Option Lean.Lsp.DocumentSelector → Lean.Lsp.TextDocumentSyncKind → Lean.Lsp.TextDocumentChangeRegistrationOptions
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.AddZeroClass.IsUnital : ∀ {X : Type u} [_G : AddZeroClass X], EckmannHilton.IsUnital (fun x1 x2 => x1 + x2) 0
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.mk.injEq : ∀ {R : Type u_2} [inst : NonAssocRing R] (toAddGroupSeminorm : AddGroupSeminorm R)
  (map_one' : toAddGroupSeminorm.toFun 1 = 1)
  (map_mul' : ∀ (x y : R), toAddGroupSeminorm.toFun (x * y) = toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y)
  (toAddGroupSeminorm_1 : AddGroupSeminorm R) (map_one'_1 : toAddGroupSeminorm_1.toFun 1 = 1)
  (map_mul'_1 :
    ∀ (x y : R), toAddGroupSeminorm_1.toFun (x * y) = toAddGroupSeminorm_1.toFun x * toAddGroupSeminorm_1.toFun y),
  ({ toAddGroupSeminorm := toAddGroupSeminorm, map_one' := map_one', map_mul' := map_mul' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toAddGroupSeminorm = toAddGroupSeminorm_1)
-- Mathlib.Algebra.GCDMonoid.Basic
exists_eq_pow_of_mul_eq_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] [Subsingleton αˣ] {a b c : α},
  IsUnit (gcd a b) → ∀ {k : ℕ}, a * b = c ^ k → ∃ d, a = d ^ k
-- Lean.Meta.Basic
Lean.Meta.withFreshCache : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_empty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal), Metric.coveringNumber ε ∅ = 0
-- Mathlib.Algebra.Order.Sub.Basic
tsub_le_self : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a - b ≤ a
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_iff_subseteq_ker_lsmul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Module.IsTorsionBySet R M s ↔ s ⊆ ↑(LinearMap.lsmul R M).ker
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smul_eq_C_mul : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : LaurentPolynomial R), r • f = LaurentPolynomial.C r * f
-- Mathlib.Algebra.DirectSum.Module
DirectSum.sigmaLcurry_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)]
  (f : DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd) (i : ι) (j : α i),
  (((DirectSum.sigmaLcurry R) f) i) j = f ⟨i, j⟩
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Ioo : ∀ {a b : ℝ}, MeasureTheory.volume (Set.Ioo a b) = ENNReal.ofReal (b - a)
-- Init.Data.UInt.Lemmas
UInt8.le_trans : ∀ {a b c : UInt8}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_one : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], LinearEquiv.baseChange R A M M 1 = 1
-- Mathlib.Analysis.Convex.Combination
/-- Center of mass of a finite collection of points with prescribed weights.
Note that we require neither `0 ≤ w i` nor `∑ w = 1`.  -/
Finset.centerMass : {R : Type u_1} →
  {E : Type u_3} →
    {ι : Type u_5} → [inst : Field R] → [inst_1 : AddCommGroup E] → [Module R E] → Finset ι → (ι → R) → (ι → E) → E
-- Init.Data.List.MapIdx
List.mapIdx_singleton : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {a : α}, List.mapIdx f [a] = [f 0 a]
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.id_tensor_id : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.Edge.id x).tensor (SSet.Truncated.Edge.id y) = SSet.Truncated.Edge.id (x, y)
-- Mathlib.Data.Sum.Order
Sum.Lex.denselyOrdered_of_noMinOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMinOrder β],
  DenselyOrdered (α ⊕ₗ β)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary_zero : SSet.boundary 0 = ⊥
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.not_irrelevant_le : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (self : ProjectiveSpectrum 𝒜), ¬HomogeneousIdeal.irrelevant 𝒜 ≤ self.asHomogeneousIdeal
-- Init.Data.Option.Basic
instLTOption : {α : Type u_1} → [LT α] → LT (Option α)
-- Mathlib.Analysis.Seminorm
/-- Closed seminorm-balls at the origin are absorbent.  -/
Seminorm.absorbent_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.closedBall 0 r)
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.null.sizeOf_spec : sizeOf Lean.JsonRpc.RequestID.null = 1
-- Init.Data.Iterators.PostconditionMonad
/-- Given a function `α → PostconditionT m β`, returns a function
`PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
Std.Iterators.PostconditionT.bind : {m : Type w → Type w'} →
  [Monad m] →
    {α β : Type w} →
      Std.Iterators.PostconditionT m α → (α → Std.Iterators.PostconditionT m β) → Std.Iterators.PostconditionT m β
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_degree_le_one : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, f.Splits → g.degree ≤ 1 → (f.comp g).Splits
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center.addCommMonoid : {M : Type u_1} → [inst : AddMonoid M] → AddCommMonoid ↥(AddSubmonoid.center M)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f}
  {cc' : CategoryTheory.Limits.CokernelCofork f'} (hf : CategoryTheory.Limits.IsColimit cc)
  (hf' : CategoryTheory.Limits.IsColimit cc') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).inv =
    CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf' cc φ.inv
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β} {f : β → m (Option β')}
  {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.Iter.filterMapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => p fx
          | none => pure { down := false })
      (Std.Iter.mapM pure it)
-- Mathlib.Data.List.Indexes
List.mapIdxMAux'_eq_mapIdxMGo : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit.{u + 1}) (as : List α)
  (arr : Array PUnit.{u + 1}), List.mapIdxMAux' f arr.size as = List.mapIdxM.go f as arr *> pure PUnit.unit
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.funUnique_apply : ∀ {R : Type u_3} {ι : Type u_4} [inst : CommSemiring R] (S : Type u_8) [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Unique ι] (x : ι → S), (AlgEquiv.funUnique R ι S) x = (Equiv.funUnique ι S) x
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_pow : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (f : (i : ι) → s i →ₗ[R] s i) (n : ℕ),
  PiTensorProduct.map (f ^ n) = PiTensorProduct.map f ^ n
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_inv : ∀ {M : Type u_1} (s : Set M) [inst : Group M], SimpleGraph.mulCayley s⁻¹ = SimpleGraph.mulCayley s
-- Init.Simproc
/-- Auxiliary command for associating a pattern with a builtin simplification procedure.
 -/
Lean.Parser.simprocPatternBuiltin : Lean.ParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i j : Set α},
  MeasurableSet i → v.restrict i ≤ w.restrict i → j ⊆ i → v.restrict j ≤ w.restrict j
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap.symm x w = ↑w.mult * Real.log (x w)
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.mkFiniteType_map : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (closed' :
    ∀ A ⊆ C,
      (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A)
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) (i : cell n),
  Topology.RelCWComplex.map n i = map n i
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  {X Y : CategoryTheory.CommMon (CategoryTheory.Functor C D)} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.map f).app X_1).hom.hom = f.hom.hom.app X_1
-- Mathlib.Data.Set.NAry
Function.uncurry.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α → β → φ) (a : α × β), Function.uncurry f a = f a.1 a.2
-- Std.Time.DateTime.PlainDateTime
Std.Time.instDecidableEqPlainDateTime.decEq : (x x_1 : Std.Time.PlainDateTime) → Decidable (x = x_1)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.sub_eq_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {s : ↥S},
  ↑s -ₒ s = 0
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Min M]
  [MeasurableInf₂ M], Measurable f → Measurable g → Measurable (f ⊓ g)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_eight : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 8 → M), ∑ i, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Each row sum of a row stochastic matrix is 1.  -/
Matrix.sum_row_of_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.rowStochastic R n → ∀ (i : n), ∑ j, M i j = 1
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.Away.integralClosure : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rf : Type u_5}
  {Sf : Type u_6} [inst_3 : CommRing Rf] [inst_4 : CommRing Sf] [inst_5 : Algebra R Rf] [inst_6 : Algebra S Sf]
  [inst_7 : Algebra Rf Sf] [inst_8 : Algebra R Sf] [IsScalarTower R S Sf] [inst_10 : IsScalarTower R Rf Sf] (f : R)
  [IsLocalization.Away f Rf] [IsLocalization.Away ((algebraMap R S) f) Sf]
  [inst_13 : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)]
  [IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf]
  [IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)],
  IsLocalization.Away ((algebraMap R ↥(integralClosure R S)) f) ↥(integralClosure Rf Sf)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.pos.sizeOf_spec : ∀ (a : ℕ), sizeOf (Sat.Literal.pos a) = 1 + sizeOf a
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local minimum equals zero.  -/
IsLocalMin.hasFDerivAt_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {a : E},
  IsLocalMin f a → HasFDerivAt f f' a → f' = 0