mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.IOError
/-- A resource was exhausted.

This corresponds to the POSIX errors  `EMFILE`, `ENFILE`, `ENOSPC`, `E2BIG`, `EAGAIN`, `EMLINK`,
`EMSGSIZE`, `ENOBUFS`, `ENOLCK`, `ENOMEM`, and `ENOSR`.
 -/
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.le_inverseImage_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D), P ≤ (P.strictMap F).inverseImage F
-- Mathlib.Topology.CompactOpen
ContinuousMap.coe_const' : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ⇑ContinuousMap.const' = ContinuousMap.const X
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Given a cofiltered diagram of qcqs schemes `Dᵢ` over `S` with affine transition maps.
If `X` is locally of finite presentation over `S`, then any `S`-morphism `lim Dᵢ ⟶ X` factors
through some `lim Dᵢ ⟶ Dⱼ ⟶ X` for some `j`.
 -/
AlgebraicGeometry.Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [AlgebraicGeometry.LocallyOfFinitePresentation f] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] (a : c.pt ⟶ X),
  CategoryTheory.CategoryStruct.comp c.π t =
      (CategoryTheory.Functor.const I).map (CategoryTheory.CategoryStruct.comp a f) →
    ∃ i g, CategoryTheory.CategoryStruct.comp (c.π.app i) g = a ∧ CategoryTheory.CategoryStruct.comp g f = t.app i
-- Lean.Parser.Basic
/-- Auxiliary function used to execute parsers provided to `longestMatchFn`.
Push `left?` into the stack if it is not `none`, and execute `p`.

Remark: `p` must produce exactly one syntax node.
Remark: the `left?` is not none when we are processing trailing parsers.  -/
Lean.Parser.runLongestMatchParser : Option Lean.Syntax → ℕ → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey? k' = some k
-- Std.Net.Addr
Std.Net.instDecidableEqInterfaceAddress : DecidableEq Std.Net.InterfaceAddress
-- Mathlib.Data.Option.Basic
Option.casesOn'_eq_elim : ∀ {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) (a : Option α), a.casesOn' b f = a.elim b f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons : {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Adj u v → G.Walk v w → G.Walk u w
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The data of a functorial factorization of any morphism in `C` as a morphism in `W₁`
followed by a morphism in `W₂`.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Type (max u_1 v_1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The inverse Fourier transform of line derivative in direction `m` is given by multiplication of
`-(2 * π * Complex.I) • (inner ℝ · m)` with the inverse Fourier transform.  -/
SchwartzMap.fourierInv_lineDerivOp_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E) (m : V),
  FourierTransformInv.fourierInv (LineDeriv.lineDerivOp m f) =
    -(2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulLeftCLM E fun x => inner ℝ x m) (FourierTransformInv.fourierInv f)
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.currPos : {s : String.Slice} → s.RevPosIterator → s.Pos
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_continuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [inst_4 : CategoryTheory.GaloisCategory C]
  [CategoryTheory.PreGaloisCategory.FiberFunctor F] [inst_6 : TopologicalSpace G] [IsTopologicalGroup G]
  [∀ (X : C), ContinuousSMul G (F.obj X).obj], Continuous ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_le_pow_iff_norm_lt_pow_add_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ), ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- Simplicially homotopic maps of simplicial sets induce the same map on
homology of the singular chain complex (with coefficients in `R`).
The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.congr_homologyMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : CategoryTheory.SimplicialObject.Homotopy f g) (R : C) (n : ℕ),
  SSet.homologyMap f R n = SSet.homologyMap g R n
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.comp_apply : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (hnp : ℬ →+*ᵍ 𝒞) (hmn : 𝒜 →+*ᵍ ℬ) (x : A),
  (hnp.comp hmn) x = hnp (hmn x)
-- Mathlib.Data.Complex.Basic
Complex.eta : ∀ (z : ℂ), { re := z.re, im := z.im } = z
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div : ∀ (a : UnitAddCircle), DifferentiableAt ℂ (fun s => HurwitzZeta.hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function `f * g` at `⊤` is less than or equal to the sum of the proximity functions of
`f` and `g`, respectively.
 -/
ValueDistribution.proximity_mul_top_le : ∀ {f₁ f₂ : ℂ → ℂ},
  Meromorphic f₁ →
    Meromorphic f₂ →
      ValueDistribution.proximity (f₁ * f₂) ⊤ ≤ ValueDistribution.proximity f₁ ⊤ + ValueDistribution.proximity f₂ ⊤
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform isomorphism between `α` and `β`  -/
«term_≃ᵤ_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.DTreeMap.maxEntry : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → t.isEmpty = false → (a : α) × β a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mvar : Lean.Meta.SynthInstance.GeneratorNode → Lean.Expr
-- Mathlib.Order.Filter.CountableSeparatingOn
exists_nonempty_countable_separating : ∀ (α : Type u_1) {p : Set α → Prop} {s₀ : Set α},
  p s₀ →
    ∀ (t : Set α) [HasCountableSeparatingOn α p t],
      ∃ S, S.Nonempty ∧ S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_zero : ∀ {a : ℕ} (a1 : 1 < a), Pell.yn a1 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.subgraphInhabited : {V : Type u} → {G : SimpleGraph V} → Inhabited G.Subgraph
-- Mathlib.Data.Quot
piSetoid : {ι : Sort u_3} → {α : ι → Sort u_4} → [(i : ι) → Setoid (α i)] → Setoid ((i : ι) → α i)
-- Mathlib.Topology.Algebra.Monoid.FunOnFinite
FunOnFinite.continuous_linearMap : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [ContinuousAdd M] {X : Type u_3} {Y : Type u_4} [inst_5 : Finite X] [inst_6 : Finite Y]
  (f : X → Y), Continuous ⇑(FunOnFinite.linearMap R M f)
-- Init.Omega.LinearCombo
_private.Init.Omega.LinearCombo.0.Lean.Omega.LinearCombo.join : List String → String
-- Lean.Message
Lean.MessageLog.msgs : Lean.MessageLog → Lean.PersistentArray Lean.Message
-- Std.Http.Data.Chunk
Std.Http.instInhabitedTrailer : Inhabited Std.Http.Trailer
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a (m.get a h) = true)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.homogeneousCochains.d_eq : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (i : ℕ),
  X.homogeneousCochains.d i (i + 1) = (TopRep.invariantsFunctor k G).map (X.d (i + 1))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The obvious projection functor from structured arrows.  -/
CategoryTheory.StructuredArrow.proj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (S : D) → (T : CategoryTheory.Functor C D) → CategoryTheory.Functor (CategoryTheory.StructuredArrow S T) C
-- Mathlib.LinearAlgebra.Determinant
/-- Any alternating map to `R` where `ι` has the cardinality of a basis equals the determinant
map with respect to that basis, multiplied by the value of that alternating map on that basis.  -/
AlternatingMap.eq_smul_basis_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) (f : M [⋀^ι]→ₗ[R] R), f = f ⇑e • e.det
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- finite = integral + finite type  -/
Algebra.finite_iff_isIntegral_and_finiteType : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filterMap_eq_length_iff : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true),
        (f a (Std.Internal.List.getValueCast a l h)).isSome = true)
-- Mathlib.RingTheory.Unramified.Finite
/-- Proposition I.2.3 of [iversen]
If `S` is an unramified `R`-algebra, and `M` is an `S`-module, then the map
`S ⊗[R] M →ₗ[S] M` taking `(b, m) ↦ b • m` admits an `S`-linear section.  -/
Algebra.FormallyUnramified.sec : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [IsScalarTower R S M] →
                    [Algebra.FormallyUnramified R S] → [Algebra.EssFiniteType R S] → M →ₗ[S] TensorProduct R S M
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.center_ne_bot : ∀ (G : Type u_1) [inst : AddGroup G] [Nontrivial G] [AddGroup.IsNilpotent G], AddSubgroup.center G ≠ ⊥
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_cochain_from_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {K : CochainComplex C ℤ} {γ₁ γ₂ : CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K j},
  γ₁ = γ₂ ↔
    (CochainComplex.mappingCone.inl φ).comp γ₁ ⋯ = (CochainComplex.mappingCone.inl φ).comp γ₂ ⋯ ∧
      (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₁ ⋯ =
        (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₂ ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback v : β},
  Std.ExtDHashMap.Const.getD (m.insert k v) a fallback =
    if (k == a) = true then v else Std.ExtDHashMap.Const.getD m a fallback
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] [Nontrivial E],
  μ.toSphere ≠ 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (p : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to0.trAux M s (Turing.TM1.Stmt.branch p q₁ q₂) x =
    bif p s x then Turing.TM1to0.trAux M s q₁ x else Turing.TM1to0.trAux M s q₂ x
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mean.eq_1 : ∀ {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι)
  (F : ι → Set X) (s : Set X), IsAddFoelner.mean μ u F s = (↑u).limUnder fun i => μ (s ∩ F i) / μ (F i)
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of August.
 -/
Std.Time.Month.Ordinal.august : Std.Time.Month.Ordinal
-- Mathlib.Data.EReal.Operations
EReal.top_mul_bot : ⊤ * ⊥ = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `extremalNumber (card V) H` is at most `x` if and only if every `H`-free simple graph `G` has
at most `x` edges.  -/
SimpleGraph.extremalNumber_le_iff : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] (H : SimpleGraph W) (m : ℕ),
  SimpleGraph.extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → G.edgeFinset.card ≤ m
-- Mathlib.Algebra.Group.Prod
/-- Coproduct of two `MonoidHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 * g p.2`.
(Commutative case; for the general case, see `MonoidHom.noncommCoprod`.)  -/
MonoidHom.coprod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : CommMonoid P] → (M →* P) → (N →* P) → M × N →* P
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter! m₂) k = default
-- Lean.Setup
/-- Abstract structure of a module's header.  -/
Lean.ModuleHeader : Type
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.min? = some km → t.contains km = true
-- Mathlib.Analysis.Fourier.AddCircle
fourier_norm : ∀ {T : ℝ} [inst : Fact (0 < T)] (n : ℤ), ‖fourier n‖ = 1
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, whiskering `G` with the
natural transformation `F ⟶ H` yields the composition of the counit of the first adjunction with
the unit of the second adjunction.  -/
CategoryTheory.Adjunction.Triple.whiskerLeft_leftToRight : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful],
  G.whiskerLeft t.leftToRight = CategoryTheory.CategoryStruct.comp t.adj₁.counit t.adj₂.unit
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'.comm : ∀ {ι : 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.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionToTruncGE'.f K e i) ((K.truncGE' e).d i j) =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).d i j) (HomologicalComplex.restrictionToTruncGE'.f K e j)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : F.obj a × G.obj a),
  (CategoryTheory.FunctorToTypes.binaryProductEquiv F G a).symm z = CategoryTheory.FunctorToTypes.prodMk z.1 z.2
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight_obj_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)),
  ((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_algebraMap : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A)
  (x : R),
  (DoubleQuot.quotQuotEquivComm I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
    (algebraMap R ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_isReduced : ∀ (u : PNat.XgcdType), u.flip.IsReduced ↔ u.IsReduced
-- Init.Data.BitVec.Bitblast
BitVec.ssubOverflow_eq : ∀ {w : ℕ} (x y : BitVec w), x.ssubOverflow y = (!x.msb && y.msb && (x - y).msb || x.msb && !y.msb && !(x - y).msb)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.lift_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F] {X : C}
  (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.lift f hf) (CategoryTheory.Limits.end_.π F j) = f j
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_of_ne : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R}
  (hx : x ≠ 0), x.order = ⋯.min ⋯
-- Std.Http.Data.URI.Basic
/-- Hierarchical path component of a URI. Each segment is stored as an `EncodedSegment` to maintain
proper percent-encoding.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.3
 -/
Std.Http.URI.Path : Type
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The fully faithful embedding of `CompHausLike P` in `TopCat`.  -/
CompHausLike.compHausLikeToTop : (P : TopCat → Prop) → CategoryTheory.Functor (CompHausLike P) TopCat
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.mapMon.eq_1 : ∀ {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.Monoidal] (hF : F.FullyFaithful),
  hF.mapMon =
    { preimage := fun {X Y} f => CategoryTheory.Mon.Hom.mk' (hF.preimage f.hom) ⋯ ⋯, map_preimage := ⋯,
      preimage_map := ⋯ }
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_posPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)),
  ↑↑(MeasureTheory.Lp.posPart f) =ᵐ[μ] fun a => max (↑↑f a) 0
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallySeparated_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsTotallySeparated {x}
-- Init.Data.List.Lemmas
List.getLast?.eq_2 : ∀ {α : Type u} (a : α) (as : List α), (a :: as).getLast? = some ((a :: as).getLast ⋯)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isClopen_singleton_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α], IsClopen {∅}
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.constantCoeff_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  MvPowerSeries.constantCoeff ((MvPowerSeries.expand p hp) φ) = MvPowerSeries.constantCoeff φ
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.mk.sizeOf_spec : ∀ (sharedExprs : Lean.Meta.Sym.SharedExprs) (config : Lean.Meta.Sym.Config),
  sizeOf { sharedExprs := sharedExprs, config := config } = 1 + sizeOf sharedExprs + sizeOf config
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.diff m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Order.RelIso.Basic
RelIso.sumLexEmpty_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsEmpty β] (a : α ⊕ β),
  (RelIso.sumLexEmpty r s) a = Sum.elim id (fun a => isEmptyElim a) a
-- Mathlib.Data.Nat.Factors
Nat.eq_prime_pow_of_unique_prime_dvd : ∀ {n p : ℕ}, n ≠ 0 → (∀ {d : ℕ}, Nat.Prime d → d ∣ n → d = p) → n = p ^ n.primeFactorsList.length
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
AnalyticWithinAt.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  AnalyticWithinAt ℝ f s x → AnalyticWithinAt ℝ (Real.sigmoid ∘ f) s x
-- Mathlib.Topology.Sheaves.Skyscraper
/-- If `y ∉ closure {p₀}`, then the stalk of `skyscraperPresheaf p₀ A` at `y` is a terminal object
 -/
skyscraperPresheafStalkOfNotSpecializesIsTerminal : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {y : ↑X} → ¬p₀ ⤳ y → CategoryTheory.Limits.IsTerminal ((skyscraperPresheaf p₀ A).stalk y)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_X : ∀ {A : Type u_2} [inst : CommRing A] (a : A), (PowerSeries.rescale a) PowerSeries.X = PowerSeries.C a * PowerSeries.X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.map_id : ∀ {R : Type r} {F : Type u} [inst : CommRing R] [inst_1 : Field F] {W' : WeierstrassCurve.Affine R}
  [inst_2 : DecidableEq F] [inst_3 : Algebra R F] (P : (W'.baseChange F).Point),
  (WeierstrassCurve.Affine.Point.map (Algebra.ofId F F)) P = P