mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesHasSum.sum : ∀ {ι : Type u_1} {f : ι → ℕ → ℂ} {S : Finset ι} {s : ℂ} {a : ι → ℂ},
  (∀ i ∈ S, LSeriesHasSum (f i) s (a i)) → LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHomEquiv_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : G →* H), MonoidAlgebra.mapDomainBialgHomEquiv f = MonoidAlgebra.mapDomainBialgHom R f
-- Mathlib.Order.Heyting.Basic
sdiff_self : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ a = ⊥
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubmonoid_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α], Antitone fun s => fixingAddSubmonoid M s
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C]
  (x : X.obj (Opposite.op { len := 0 })),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0) (X.homology₀Iso R).hom) =
    CategoryTheory.Limits.Sigma.ι (fun x => R) (SSet.π₀.mk x)
-- Mathlib.Data.Set.Defs
/-- Elaborate set builder notation for `Set`.

* `{x | p x}` is elaborated as `Set.ofPred fun x ↦ p x`
* `{x : α | p x}` is elaborated as `Set.ofPred fun x : α ↦ p x`
* `{binder x | p x}`, where `x` is bound by the `binder` binder, is elaborated as
  `{x | binder x ∧ p x}`. The typical example is `{x ∈ s | p x}`, which is elaborated as
  `{x | x ∈ s ∧ p x}`. The possible binders are
  * `· ∈ s`, `· ∉ s`
  * `· ⊆ s`, `· ⊂ s`, `· ⊇ s`, `· ⊃ s`
  * `· ≤ a`, `· ≥ a`, `· < a`, `· > a`, `· ≠ a`

  More binders can be declared using the `binder_predicate` command, see `Init.BinderPredicates` for
  more info.

See also
* `Data.Finset.Basic` for the `Finset` builder notation elaborator partly overriding this one for
  syntax of the form `{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator partly overriding this one for
  syntax of the form `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
* `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator partly overriding this
  one for syntax of the form `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.
 -/
Mathlib.Meta.elabSetBuilder : Lean.Elab.Term.TermElab
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Iic : ∀ {n m : ℕ} (a : Fin n) (h : n ≤ m), Finset.map (Fin.castLEEmb h) (Finset.Iic a) = Finset.Iic (Fin.castLE h a)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_add_right : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (s + t).Nonempty → t.Nonempty
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π)
      (CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π)
      (CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  {Z_1 : CategoryTheory.Functor (CategoryTheory.Over Z) (CategoryTheory.Over Z)}
  (h : CategoryTheory.Functor.id (CategoryTheory.Over Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ChosenPullbacksAlong.pullbackComp f g).hom
        (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).counit h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).counit h
-- Mathlib.Topology.Covering.Basic
/-- A constructor for `IsCoveringMapOn` when there are both empty and nonempty fibers.  -/
IsCoveringMapOn.mk' : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (s : Set X)
  (F : ↑s → Type u_3) [inst_2 : (x : ↑s) → TopologicalSpace (F x)] [hF : ∀ (x : ↑s), DiscreteTopology (F x)]
  (t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }),
  (∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ nhds ↑x, f ⁻¹' U = ∅) → IsCoveringMapOn f s
-- Mathlib.Analysis.Calculus.Taylor
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.

Version for arbitrary sets  -/
hasDerivWithinAt_taylorWithinEval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x y : ℝ} {n : ℕ} {s s' : Set ℝ},
  UniqueDiffOn ℝ s →
    s' ∈ nhdsWithin y s →
      y ∈ s' →
        s' ⊆ s →
          ContDiffOn ℝ (↑n) f s →
            DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y →
              HasDerivWithinAt (fun t => taylorWithinEval f n s t x)
                (((↑n.factorial)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.termσ_2 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  {X Y : CategoryTheory.Over A} (ε : X ⟶ Y),
  (CategoryTheory.OverPresheafAux.restrictedYoneda A).map ε =
    CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ (CategoryTheory.Over.Hom.left ε) ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∈ t ↔ t[a]?.isSome = true
-- Mathlib.Algebra.Lie.Subalgebra
/-- An injective Lie algebra morphism is an equivalence onto its range.  -/
LieEquiv.ofInjective : {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₂) → Function.Injective ⇑f → L₁ ≃ₗ⁅R⁆ ↥f.range
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.ofAIGAux.go : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      (decls : Array (Std.Sat.AIG.Decl α)) →
        (idx : ℕ) → Std.Sat.AIG.RelabelNat.State α decls idx → Std.Sat.AIG.RelabelNat.State α decls decls.size
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Given a closed embedding into a completely pseudometrizable space,
the source space is also completely pseudometrizable.  -/
Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → TopologicalSpace.IsCompletelyPseudoMetrizableSpace X
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.norm_toAbs_eq : ∀ {R : Type u_1} [inst : Ring R] (v : AbsoluteValue R ℝ) (x : R), ‖WithAbs.toAbs v x‖ = v x
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDHashMap.getD : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.ExtDHashMap α β → (a : α) → β a → β a
-- Mathlib.Data.Rel
/-- Preimage of a set `t` under a relation `R`. Same as the image of `t` under `R.inv`.  -/
SetRel.preimage : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set β → Set α
-- Init.Data.Int.DivMod.Lemmas
Int.sub_emod_bmod : ∀ {y : ℤ} (x : ℤ) (n : ℕ), (x - y % ↑n).bmod n = (x - y).bmod n
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given `Uᵢ ×[Z] Y`, this is the glued fibred product `X ×[Z] Y`.  -/
AlgebraicGeometry.Scheme.Pullback.gluing : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          AlgebraicGeometry.Scheme.GlueData
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₂_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ) {Z : C}
  (h_1 : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))
      (CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] {r : R},
  Ideal.span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_ofNatLT : ∀ (n : ℕ) (hn : n < 2 ^ 32), Int32.ofBitVec n#'hn = Int32.ofNat n
-- Mathlib.Topology.MetricSpace.Congruence
/-- Two sets of vertices remain congruent under a dilation if the dilations have equal ratios.  -/
Congruent.comp_dilation : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {P₄ : Type u_6} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃]
  [inst_3 : PseudoEMetricSpace P₄] {F₁ : Type u_7} {F₂ : Type u_8} [inst_4 : FunLike F₁ P₁ P₃]
  [inst_5 : DilationClass F₁ P₁ P₃] [inst_6 : FunLike F₂ P₂ P₄] [inst_7 : DilationClass F₂ P₂ P₄] {f₁ : F₁} {f₂ : F₂},
  Congruent v₁ v₂ → Dilation.ratio f₁ = Dilation.ratio f₂ → Congruent (⇑f₁ ∘ v₁) (⇑f₂ ∘ v₂)
-- Mathlib.Data.List.Permutation
List.mem_permutationsAux2' : ∀ {α : Type u_1} {t : α} {ts ys l : List α},
  l ∈ (List.permutationsAux2 t ts [] ys id).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.toBasisAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s : ι → (x : M) → V x}
  {u : Set M} {x : M} {n : WithTop ℕ∞} (hs : IsLocalFrameOn I F n s u) (hx : x ∈ u),
  hs.toBasisAt hx = Module.Basis.mk ⋯ ⋯
-- Lean.Language.Basic
/-- Yields the default reporting range of a `Syntax`, which is just the `canonicalOnly` range
of the syntax if any, or `inherit` otherwise.
 -/
Lean.Language.SnapshotTask.defaultReportingRange : Option Lean.Syntax → Lean.Language.SnapshotTask.ReportingRange
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.nil : {α : Type u} → {β : α → Type v} → Std.DHashMap.Internal.AssocList α β
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
CuspForm.toModularFormₗ_injective : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne], Function.Injective ⇑CuspForm.toModularFormₗ
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalNonAssocRingOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalNonAssocRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalNonAssocRing (DirectLimit G f)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (S T : Set G),
  AddSubgroup.IsComplement S T = Function.Bijective fun x => ↑x.1 + ↑x.2
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.isRegularMonoCategory`.

---

The following diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
being a pullback for any monic `m` means that every monomorphism
in `C` is the pullback of a regular monomorphism; since regularity
is stable under base change, every monomorphism is regular.
Hence, `C` is a regular mono category.
It also follows that `C` is a balanced category.
 -/
CategoryTheory.HasClassifier.isRegularMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.HasSubobjectClassifier C],
  CategoryTheory.IsRegularMonoCategory C
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.addRight_apply : ∀ {α : Type u_2} [inst : Add α] [inst_1 : LinearOrder α] [inst_2 : AddRightStrictMono α] (m n : α),
  (OrderEmbedding.addRight m) n = n + m
-- Init.Data.Ord.Vector
Vector.compare_eq_compare_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : Ord α] {a b : Vector α n}, compare a b = compare a.toArray b.toArray
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.instIsTopologicalDivisionRing : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [inst_2 : IsTopologicalDivisionRing K]
  [inst_3 : CompletableTopField K] [inst_4 : IsUniformAddGroup K], IsTopologicalDivisionRing (UniformSpace.Completion K)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_singleton : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (x : X), Metric.coveringNumber ε {x} = 1
-- Mathlib.Algebra.Group.Units.Hom
/-- The additive homomorphism on `AddUnit`s induced by an `AddMonoidHom`.  -/
AddUnits.map : {M : Type u} → {N : Type v} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → (M →+ N) → AddUnits M →+ AddUnits N
-- Mathlib.Order.Bounds.Image
MonotoneOn.image_upperBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  MonotoneOn f t → s ⊆ t → f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.differentiableAt_binEntropy : ∀ {p : ℝ}, p ≠ 0 → p ≠ 1 → DifferentiableAt ℝ Real.binEntropy p
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → Array β → Sort u_3) (a : α) (as : List α) (acc : Array β)
  (h_1 : (acc : Array β) → motive [] acc) (h_2 : (a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc),
  (match a :: as, acc with
    | [], acc => h_1 acc
    | a :: as, acc => h_2 a as acc) =
    h_2 a as acc
-- Mathlib.Data.Fin.SuccPred
Fin.succ_injective : ∀ (n : ℕ), Function.Injective Fin.succ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_left_unitality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₁ X₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).hom
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂).hom))
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.primrec₂_curry : Primrec₂ Nat.Partrec.Code.curry
-- Lean.SubExpr
Lean.SubExpr.instToJsonFVarId : Lean.ToJson Lean.FVarId
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerLeft_id : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C),
  CategoryTheory.eHomWhiskerLeft V X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.Algebra.Divisibility.Basic
dvd_pow_self : ∀ {α : Type u_1} [inst : Monoid α] (a : α) {n : ℕ}, n ≠ 0 → a ∣ a ^ n
-- Mathlib.ModelTheory.Definability
Set.TermDefinable.eq_1 : ∀ {M : Type w} (A : Set M) (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u₁} (f : (α → M) → M),
  A.TermDefinable L f = ∃ φ, f = fun v => FirstOrder.Language.Term.realize v φ
-- Mathlib.Data.Quot
Quotient.out_equiv_out : ∀ {α : Sort u_1} {s : Setoid α} {x y : Quotient s}, x.out ≈ y.out ↔ x = y
-- Init.Data.String.Lemmas.FindPos
String.posGT_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : p < s.toSlice.rawEndPos), s.toSlice.posGT p h = (s.posGT p h).toSlice
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_self : ∀ {α : Type u_1} {s t : Set α}, s ∪ t \ s = s ∪ t
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- Ternary version of `fderivWithin_comp`, with equality assumptions of basepoints added, in
order to apply more easily as a rewrite from right-to-left.  -/
fderivWithin_comp₃ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {f : E → F} (x : E) {s : Set E} {g' : G → G'} {g : F → G} {t : Set F} {u : Set G} {y : F}
  {y' : G},
  DifferentiableWithinAt 𝕜 g' u y' →
    DifferentiableWithinAt 𝕜 g t y →
      DifferentiableWithinAt 𝕜 f s x →
        Set.MapsTo g t u →
          Set.MapsTo f s t →
            g y = y' →
              f x = y →
                UniqueDiffWithinAt 𝕜 s x →
                  fderivWithin 𝕜 (g' ∘ g ∘ f) s x =
                    fderivWithin 𝕜 g' u y' ∘SL fderivWithin 𝕜 g t y ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ → i₂ ≠ i₃ → line[ℝ, t.points i₂, t.points i₃].SSameSide (Affine.Simplex.excenter t {i₂}) (t.points i₁)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.ΓIsEquiv : AlgebraicGeometry.AffineScheme.Γ.IsEquivalence
-- Init.Data.List.BasicAux
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
over a nested inductive like `inductive T | mk : List T → T`.  -/
List.tacticSizeOf_list_dec : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The functor from augmented objects to arrows.  -/
CategoryTheory.SimplicialObject.Augmented.toArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.Arrow C)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.isSome_get?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (Std.ExtDHashMap.Const.get? m a).isSome = m.contains a
-- Mathlib.Algebra.Group.Submonoid.Defs
ZeroMemClass.coe_eq_zero : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : ↥S'},
  ↑x = 0 ↔ x = 0
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- See `Edge.comp`
 -/
SSet.Truncated.Edge.compStruct : {A : SSet.Truncated 2} →
  [inst : A.Quasicategory₂] →
    {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
      (f : SSet.Truncated.Edge x y) → (g : SSet.Truncated.Edge y z) → f.CompStruct g (f.comp g)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_preimage_fst_singleton_eq_tsum : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β] [Countable β] (μ : MeasureTheory.Measure (α × β)) (x : α),
  μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_eq_zero_iff : ∀ {a b : Ordinal.{u_4}}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.End : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : CoalgebraStruct R A] → Monoid (A →ₐc[R] A)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, a ∈ m.erase k → a ∈ m
-- Mathlib.Topology.QuasiSeparated
IsQuasiSeparated.image_of_isEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  IsQuasiSeparated s → Topology.IsEmbedding f → IsQuasiSeparated (f '' s)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.mem_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {y : N},
  y ∈ f.range ↔ ∃ x, f x = y
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
_private.Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : SizeOf C] (X : C) [grp : CategoryTheory.GrpObj X], sizeOf { X := X, grp := grp } = 1 + sizeOf X + sizeOf grp
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The functor `Γ₀` sends a chain complex `K` to the simplicial object which
sends `Δ` to the direct sum of the objects `summand K Δ A` for all `A : Splitting.IndexSet Δ`  -/
AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ChainComplex C ℕ → SimplexCategoryᵒᵖ → [CategoryTheory.Limits.HasFiniteCoproducts C] → C