mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- Matrix version of `isSemilinearSet_setOfPred_eq`.  -/
Nat.isSemilinearSet_setOfPred_mulVec_eq : ∀ {ι : Type u_3} {κ : Type u_4} [inst : Fintype κ] (u v : ι → ℕ) (A B : Matrix ι κ ℕ),
  IsSemilinearSet {x | u + A.mulVec x = v + B.mulVec x}
-- Mathlib.Computability.DFA
DFA.union_accept : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2),
  (M1.union M2).accept = {s | s.1 ∈ M1.accept ∨ s.2 ∈ M2.accept}
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Given `ι : C ⥤ A`, this is the extension of `Λ : LeftResolution ι` to
`LeftResolution ((functorExtension₂ C A).obj ι)`, where
`(functorExtension₂ C A).obj ι : Karoubi C ⥤ Karoubi A` is the extension of `ι`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            [inst_2 : CategoryTheory.Preadditive C] →
              [inst_3 : CategoryTheory.Preadditive A] →
                [ι.Additive] →
                  CategoryTheory.Abelian.LeftResolution ((CategoryTheory.Idempotents.functorExtension₂ C A).obj ι)
-- Mathlib.Data.Holor
Holor.instInhabited : {α : Type} → {ds : List ℕ} → [Inhabited α] → Inhabited (Holor α ds)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For a nonzero `k = r/s ∈ K`, the fractional ideal `(k)` is equal to the product
`∏_v v^(val_v(r) - val_v(s))`.  -/
FractionalIdeal.finprod_heightOneSpectrum_factorization_principal : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ (k : K),
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) k →
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R),
            ↑v.asIdeal ^
              (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors) -
                ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(Classical.choose ⋯)})).factors)) =
          I
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (range : Lean.Lsp.Range) (uri_1 : Lean.Lsp.DocumentUri) (range_1 : Lean.Lsp.Range),
  ({ uri := uri, range := range } = { uri := uri_1, range := range_1 }) = (uri = uri_1 ∧ range = range_1)
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.lift.congr_simp : ∀ {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → CommRing (G i)]
  (f : (i j : ι) → i ≤ j → G i → G j) (P : Type u_3) [inst_2 : CommRing P] (g g_1 : (i : ι) → G i →+* P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x),
  Ring.DirectLimit.lift G f P g Hg = Ring.DirectLimit.lift G f P g_1 ⋯
-- Mathlib.Data.Multiset.FinsetOps
Multiset.le_ndunion_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (t : Multiset α), s.Nodup → s ≤ s.ndunion t
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_lt_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α]
  [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α},
  (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → (Multiset.map f s).sum < (Multiset.map g s).sum
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableWithinAt.fst : ∀ {𝕜 : 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] {x : E} {s : Set E} {f₂ : E → F × G},
  DifferentiableWithinAt 𝕜 f₂ s x → DifferentiableWithinAt 𝕜 (fun x => (f₂ x).1) s x
-- Mathlib.Algebra.Group.TransferInstance
Equiv.Neg.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Neg β], e.Neg = { neg := fun x => e.invFun (-e.toFun x) }
-- Mathlib.Control.Monad.Cont
OptionT.callCC.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadCont m] {α β : Type u}
  (f : MonadCont.Label α (OptionT m) β → OptionT m α),
  OptionT.callCC f = OptionT.mk (MonadCont.callCC fun x => (f (OptionT.mkLabel x)).run)
-- Mathlib.Algebra.Group.End
Equiv.Perm.iterate_eq_pow : ∀ {α : Type u_4} (f : Equiv.Perm α) (n : ℕ), (⇑f)^[n] = ⇑(f ^ n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k}, (compare t.maxKey! (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey!).isLE = true
-- Init.GrindInstances.Ring.UInt
USize.intCast : IntCast USize
-- Init.Data.List.ToArrayImpl
/-- Converts a `List α` into an `Array α` by repeatedly pushing elements from the list onto an empty
array. `O(|xs|)`.

Use `List.toArray` instead of calling this function directly. At runtime, this operation implements
both `List.toArray` and `Array.mk`.
 -/
List.toArrayImpl : {α : Type u_1} → List α → Array α
-- Mathlib.Algebra.Colimit.DirectLimit
/-- `map₀` as a `RingHom`.  -/
DirectLimit.map₀RingHom : {ι : 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 ι] →
                [inst_4 : Nonempty ι] →
                  [inst_5 : (i : ι) → NonAssocSemiring (G i)] →
                    [inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] →
                      ((i : ι) → G i) →+* DirectLimit G f
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.ErrorFormat.noConfusionType : Sort v✝ → Mathlib.Linter.TextBased.ErrorFormat → Mathlib.Linter.TextBased.ErrorFormat → Sort v✝
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.continuous_setToFun_of_dominated : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {X : Type u_7} [inst_4 : TopologicalSpace X] [FirstCountableTopology X]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : X → α → E} {bound : α → ℝ},
  (∀ (x : X), MeasureTheory.AEStronglyMeasurable (fs x) μ) →
    (∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, Continuous fun x => fs x a) → Continuous fun x => MeasureTheory.setToFun μ T hT (fs x)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The centralizer of a set as subsemiring.  -/
Subsemiring.centralizer : {R : Type u_1} → [inst : Semiring R] → Set R → Subsemiring R
-- Std.Time.Format.Modifier
/-- `b`: Day period with noon/midnight distinction (e.g., AM, noon, midnight).
 -/
Std.Time.Modifier.b : Std.Time.Text → Std.Time.Modifier
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_self' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ j) =
      CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_4 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match Nat.Partrec.Code.right with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_4 ()
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the reverse direction of `Asymptotics.isLittleOTVS_iff_isLittleO`. -/
Asymptotics.IsLittleO.isLittleOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =o[l] g → f =o[𝕜; l] g
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.zero_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (x : M), 0 x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isColimit : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C),
  (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isColimit =
    (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.exactAt_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact → ∀ (i : ι), S.X₁.ExactAt i → S.X₃.ExactAt i → S.X₂.ExactAt i
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.liftEquiv_apply : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A]
  (fg :
    { fg //
      (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧
        (∀ (r : R) (x : M), fg.2 (r • x) = fg.1 r * fg.2 x) ∧
          ∀ (r : R) (x : M), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }),
  TrivSqZeroExt.liftEquiv fg = TrivSqZeroExt.lift (↑fg).1 (↑fg).2 ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_nsmul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : ContinuousAdd M] (x : M) (n : ℕ),
  SeparationQuotient.mk (n • x) = n • SeparationQuotient.mk x
-- Mathlib.Data.Fintype.Prod
/-- See `Pi.infinite_of_exists_right` for the case that only one `π i` is infinite.  -/
Pi.infinite_of_right : ∀ {ι : Sort u_4} {π : ι → Type u_5} [∀ (i : ι), Infinite (π i)] [Nonempty ι], Infinite ((i : ι) → π i)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A category `HasWideEqualizers` if it has all limits of shape `WalkingParallelFamily J`, i.e.
if it has a wide equalizer for every family of parallel morphisms.  -/
CategoryTheory.Limits.HasWideEqualizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.MeasureTheory.Measure.Prod
/-- Marginal measure on `β` obtained from a measure on `ρ` `α × β`, defined by `ρ.map Prod.snd`.  -/
MeasureTheory.Measure.snd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → MeasureTheory.Measure (α × β) → MeasureTheory.Measure β
-- Mathlib.Data.Quot
Quotient.sound' : ∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, s₁ a b → Quotient.mk'' a = Quotient.mk'' b
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → aig.RefVec w → ℕ → aig.ShiftTarget w
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coeFn_smul : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {R : Type u_2} [inst_1 : SMul R NNReal] [inst_2 : SMul R ENNReal]
  [inst_3 : IsScalarTower R NNReal ENNReal] [inst_4 : IsScalarTower R ENNReal ENNReal] [IsScalarTower R NNReal NNReal]
  (c : R) (μ : MeasureTheory.FiniteMeasure Ω), ⇑(c • μ) = c • ⇑μ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- Constructor for additive morphisms from `CohomologyClass K L n`.  -/
CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          {G : Type u_2} →
            [inst_2 : AddCommGroup G] →
              (f : CochainComplex.HomComplex.Cocycle K L n →+ G) →
                CochainComplex.HomComplex.coboundaries K L n ≤ f.ker →
                  CochainComplex.HomComplex.CohomologyClass K L n →+ G
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : Colex α), ofColex (b • a) = b • ofColex a
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousAt.norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {a : α},
  ContinuousAt f a → ContinuousAt (fun x => ‖f x‖) a
-- Lean.Parser.Syntax
Lean.Parser.optPrecedence.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config.mk.sizeOf_spec : ∀ (useDecide emptyType : Bool) (searchFuel : ℕ) (genDiseq : Bool),
  sizeOf { useDecide := useDecide, emptyType := emptyType, searchFuel := searchFuel, genDiseq := genDiseq } =
    1 + sizeOf useDecide + sizeOf emptyType + sizeOf searchFuel + sizeOf genDiseq
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0),
  CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom S.rightHomologyι =
    CategoryTheory.CategoryStruct.id S.opcycles
-- Mathlib.Data.Fintype.Perm
permsOfList.eq_2 : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α),
  permsOfList (a :: l) =
    permsOfList l ++ List.flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f g : Module.End R N),
  LinearMap.rTensor M (f * g) = LinearMap.rTensor M f * LinearMap.rTensor M g
-- Init.Data.Option.Lemmas
Option.left_le_of_merge_le : ∀ {α : Type u_1} [inst : LE α] {f : α → α → α},
  (∀ (a b c : α), f a b ≤ c → a ≤ c) → ∀ {o₁ o₂ o₃ : Option α}, Option.merge f o₁ o₂ ≤ o₃ → o₁ ≤ o₃
-- Mathlib.Algebra.LinearRecurrence
instInhabitedLinearRecurrence : (R : Type u_1) → [inst : CommSemiring R] → Inhabited (LinearRecurrence R)
-- Init.Data.String.Termination
String.Slice.Pos.Down.mk.sizeOf_spec : ∀ {s : String.Slice} (inner : s.Pos), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.norm_mk_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
  (S : Submodule R M) (m : M), ‖Submodule.Quotient.mk m‖ ≤ ‖m‖
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isMatch_ofSliceTo_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {pos : (s.sliceTo p).Pos},
  String.Slice.Pattern.Model.IsMatch pat (String.Slice.Pos.ofSliceTo pos) ↔ String.Slice.Pattern.Model.IsMatch pat pos
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The "reduction" relation  -/
Quiver.FreeGroupoid.redStep : {V : Type u} → [inst : Quiver V] → HomRel (CategoryTheory.Paths (Quiver.Symmetrify V))
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Auxiliary definition for `mk`.  -/
CochainComplex.mkAux : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₀ ⟶ X₁) →
          (d₁ : X₁ ⟶ X₂) →
            CategoryTheory.CategoryStruct.comp d₀ d₁ = 0 →
              ((S : CategoryTheory.ShortComplex V) →
                  (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) →
                ℕ → CategoryTheory.ShortComplex V
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxoIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxo.IsAlwaysFinite (BitVec n)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.IsUniversal.existsUnique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.CostructuredArrow S T), ∃! η, CategoryTheory.CategoryStruct.comp (S.map η) f.hom = g.hom
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_toList_insert_self : ∀ {α : Type u_1} {cmp : α → α → Ordering} (v : α) (t : RBTree.RBSet α cmp), v ∈ (t.insert v).toList
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.mk : {r : UInt8 → Bool} →
  (toByteArray : ByteArray) → Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray → Std.Http.URI.EncodedQueryString r
-- Std.Net.Addr
Std.Net.instInhabitedSocketAddressV4.default : Std.Net.SocketAddressV4
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffWithinAt_finsetProd`. -/
contMDiffWithinAt_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x
-- Mathlib.Algebra.Group.Basic
sub_ne_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b ≠ 0 ↔ a ≠ b
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.tsum_eval : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] {α : Type u_5}
  {p : α → ContinuousMultilinearMap 𝕜 E F},
  Summable p → ∀ (m : (i : ι) → E i), (∑' (a : α), p a) m = ∑' (a : α), (p a) m
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.Raw.unitOfList l).getKey! k' = k
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instCommRing : {σ : Type u_1} → {R : Type u_2} → [CommRing R] → CommRing (MvPowerSeries σ R)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.op.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.op = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.op c.π }
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `fderiv 𝕜 f` is smooth at `x₀`.  -/
ContDiffAt.fderiv_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x₀ : E}
  {m n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x₀ → m + 1 ≤ n → ContDiffAt 𝕜 m (fderiv 𝕜 f) x₀
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).getKey? k = (t₂.getKey? k).or (t₁.getKey? k)
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.mk : {α : Type u} →
  [toPreorderPackage : Std.PreorderPackage α] →
    [toOrd : Ord α] →
      [toLawfulOrderOrd : Std.LawfulOrderOrd α] → (∀ (a b : α), a ≤ b ∨ b ≤ a) → Std.LinearPreorderPackage α
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_nat_eq : ∀ {a : Cardinal.{u_1}} (n : ℕ), Cardinal.aleph0 ≤ a → a + ↑n = a
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F),
  ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).pt = c.left
-- Mathlib.Order.KrullDimension
/-- For elements of finite height, `coheight` is strictly antitone.  -/
Order.coheight_strictAnti : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, y < x → Order.coheight x < ⊤ → Order.coheight x < Order.coheight y
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- If `f` is a normal epi, then every morphism `k : X ⟶ W` satisfying `NormalEpi.g ≫ k = 0`
induces `l : Y ⟶ W` such that `f ≫ l = k`.  -/
CategoryTheory.NormalEpi.desc' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {W : C} →
          (f : X ⟶ Y) →
            [nef : CategoryTheory.NormalEpi f] →
              (k : X ⟶ W) →
                CategoryTheory.CategoryStruct.comp CategoryTheory.NormalEpi.g k = 0 →
                  { l // CategoryTheory.CategoryStruct.comp f l = k }
-- Lean.Parser.Syntax
Lean.Parser.Command.macroTail : Lean.Parser.Parser
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_sub_self : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  autoParam (IsSelfAdjoint a) CFC.abs_sub_self._auto_1 → CFC.abs a - a = 2 • a⁻
-- Mathlib.SetTheory.ZFC.PSet
PSet.nonempty_of_nonempty_type : ∀ (x : PSet.{u_1}) [h : Nonempty x.Type], x.Nonempty
-- Init.Data.Repr
/-- Auxiliary class for marking types that should be considered atomic by `Repr` methods.
We use it at `Repr (List α)` to decide whether `bracketFill` should be used or not.  -/
ReprAtom : Type u → Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_true_iff_forall_contains_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool},
  m.WF → (m.all p = true ↔ ∀ (a : α) (h : m.contains a = true), p a (Std.DHashMap.Raw.Const.get m a h) = true)
-- Init.Prelude
/-- `a ++ b` is the result of concatenation of `a` and `b`. See `HAppend`.  -/
Append.append : {α : Type u} → [self : Append α] → α → α → α