mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The skyscraper presheaf supported at `p₀` with value `A` is the sheaf that assigns `A` to all opens
`U` that contain `p₀` and assigns `*` otherwise.
 -/
skyscraperSheaf : {X : TopCat} →
  (p₀ : ↑X) →
    [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst : CategoryTheory.Category.{u, v} C] → C → [CategoryTheory.Limits.HasTerminal C] → TopCat.Sheaf C X
-- Mathlib.Control.Applicative
Functor.Comp.map_pure : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G] {α β : Type v} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.coe_mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Continuous f), ⇑{ toFun := f, continuous_toFun := h } = f
-- Mathlib.Topology.Order.MonotoneConvergence
Antitone.ge_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atBot (nhds a) → ∀ (b : β), f b ≤ a
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.absNorm_ne_zero`.

---

The norm of a maximal ideal as an element of `ℝ≥0` is `≠ 0`  -/
NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], ↑(Ideal.absNorm v.asIdeal) ≠ 0
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy1.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.copy_sliceTo_startPos : ∀ {s : String.Slice}, (s.sliceTo s.startPos).copy = ""
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.mk.inj : ∀ {thmType : Lean.Expr} {us : List Lean.Level} {numIndices : ℕ} {thmType_1 : Lean.Expr} {us_1 : List Lean.Level}
  {numIndices_1 : ℕ},
  { thmType := thmType, us := us, numIndices := numIndices } =
      { thmType := thmType_1, us := us_1, numIndices := numIndices_1 } →
    thmType = thmType_1 ∧ us = us_1 ∧ numIndices = numIndices_1
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The centroid of some vertices of a simplex, in terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (fs : Finset (Fin (n + 1))),
  Finset.centroid ℝ fs s.points =
    (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
      (Affine.Simplex.centroidWeightsWithCircumcenter fs)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [h : ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsSFiniteKernel κ
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.comp_explicitCokernelπ : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (SemiNormedGrp.explicitCokernelπ f) = 0
-- Mathlib.Probability.Notation
/-- `X =ₐₛ Y` if `X = Y` almost surely.  -/
ProbabilityTheory.«term_=ₐₛ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Given an `R`-multilinear map `f` taking values in `R`, `f.smulRight z` is the map
sending `m` to `f m • z`.  -/
MultilinearMap.smulRight : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] → MultilinearMap R M₁ R → M₂ → MultilinearMap R M₁ M₂
-- Mathlib.AlgebraicTopology.SingularSet
/-- Geometric realization is left adjoint to the singular simplicial set construction.  -/
sSetTopAdj : SSet.toTop ⊣ TopCat.toSSet
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csInf_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddBelow s → s.Nonempty → (a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b)
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `min a b`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalMin : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mem_addSubgroup_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M}
  {s : UpperSet (FiniteArchimedeanClass M)},
  a ∈ FiniteArchimedeanClass.addSubgroup s ↔ ∀ (h : a ≠ 0), FiniteArchimedeanClass.mk a h ∈ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_lt_iff_lt_sin : ∀ {x y : ℝ}, x ∈ Set.Icc (-1) 1 → y ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → (Real.arcsin x < y ↔ x < Real.sin y)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.two_two : Real.HolderConjugate 2 2
-- Init.Data.Int.DivMod.Lemmas
Int.mul_bmod_left : ∀ (a : ℤ) (b : ℕ), (a * ↑b).bmod b = 0
-- Mathlib.LinearAlgebra.Dimension.Free
finrank_le_iff_exists_linearMap : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R]
  [Module.Finite R M] [Module.Finite R M'], Module.finrank R M ≤ Module.finrank R M' ↔ ∃ f, Function.Injective ⇑f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k = default
-- Mathlib.Order.Lattice
inf_left_comm : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)
-- Mathlib.Data.List.Rotate
List.isRotated_nil_iff' : ∀ {α : Type u} {l : List α}, [] ~r l ↔ [] = l
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.natDegree_denom_le_natDegree_minpolyX : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K),
  (¬∃ c, f = RatFunc.C c) → f.denom.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity_right₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {g : β → ENNReal},
  AEMeasurable g ν → μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun z => g z.2
-- Init.Data.SInt.Bitwise
Int64.shiftRight_and : ∀ {a b c : Int64}, (a &&& b) >>> c = a >>> c &&& b >>> c
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The `LinearIsometryEquiv` which maps an orthonormal basis to another. This is a convenience
wrapper around `Orthonormal.equiv`.  -/
OrthonormalBasis.equiv : {ι : Type u_1} →
  {ι' : Type u_2} →
    {𝕜 : Type u_3} →
      [inst : RCLike 𝕜] →
        {E : Type u_4} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : Fintype ι] →
                {E' : Type u_7} →
                  [inst_4 : Fintype ι'] →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : InnerProductSpace 𝕜 E'] →
                        OrthonormalBasis ι 𝕜 E → OrthonormalBasis ι' 𝕜 E' → ι ≃ ι' → E ≃ₗᵢ[𝕜] E'
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β) (f : β → α),
  ∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The n-skeleton as a functor `SSet.Truncated n ⥤ SSet`.  -/
SSet.Truncated.sk : (n : ℕ) → CategoryTheory.Functor (SSet.Truncated n) SSet
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.eq_2 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.done with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_2 ()
-- Lean.Meta.LetToHave
/-- Gives the type of `r.expr`. If it has not been computed yet, updates the cache.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.type : Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of
the determinants of the diagonal blocks. For the generalization to any number of blocks, see
`Matrix.det_of_isLowerTriangular`.  -/
Matrix.det_fromBlocks_zero₁₂ : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R),
  (Matrix.fromBlocks A 0 C D).det = A.det * D.det
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsZeroOrMarkovKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.IsZeroOrMarkovKernel (κ.compProd η)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator.  -/
Nat.isValue : Lean.Meta.Simp.DSimproc
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
/-- The increments of a Gaussian process are Gaussian.  -/
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_increments : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P →
    ∀ {n : ℕ} {t : Fin (n + 1) → T}, ProbabilityTheory.HasGaussianLaw (fun ω i => X (t i.succ) ω - X (t i.castSucc) ω) P
-- Mathlib.NumberTheory.Divisors
/-- Pairs of divisors of an integer as a finset.

`z.divisorsAntidiag` is the finset of pairs `(a, b) : ℤ × ℤ` such that `a * b = z`.
By convention, we set `Int.divisorsAntidiag 0 = ∅`.

O(|z|). Computed from `Nat.divisorsAntidiagonal`.  -/
Int.divisorsAntidiag : ℤ → Finset (ℤ × ℤ)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a given factorisation through a mono is initial.  -/
CategoryTheory.Limits.IsImage.lift_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F)
  (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m
-- Init.Data.Nat.ToString
Nat.ofDigitChars_replicate_zero : ∀ {b init n : ℕ}, b.ofDigitChars (List.replicate n '0') init = b ^ n * init
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.liftProp_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'},
  ChartedSpace.LiftProp P f ↔
    Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.integral_condDistrib_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable Y μ →
    MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x)
        (MeasureTheory.Measure.map X μ)
-- Mathlib.Data.Int.Log
Int.clog_one_left : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (r : R), Int.clog 1 r = 0
-- Mathlib.Algebra.Quandle
_private.Mathlib.Algebra.Quandle.0.Rack.toEnvelGroup.mapAux.match_1.splitter : {R : Type u_1} →
  (motive : Rack.PreEnvelGroup R → Sort u_2) →
    (x : Rack.PreEnvelGroup R) →
      (Unit → motive Rack.PreEnvelGroup.unit) →
        ((x : R) → motive (Rack.PreEnvelGroup.incl x)) →
          ((a b : Rack.PreEnvelGroup R) → motive (a.mul b)) → ((a : Rack.PreEnvelGroup R) → motive a.inv) → motive x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_modify : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : β k → β k}, (m.modify k f).contains k' = m.contains k'
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(NumberField.mixedEmbedding.polarCoordReal K).symm ''
      (NumberField.mixedEmbedding.polarCoordReal K).target =ᵐ[MeasureTheory.volume]
    Set.univ
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.saveEMatchTheorem : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GrindM Unit
-- Mathlib.Algebra.CharP.Two
/-- **Alias** of `CharTwo.sq_injective`. -/
CharTwo.CommRing.sq_injective : ∀ {R : Type u_1} [inst : CommRing R] [CharP R 2] [NoZeroDivisors R], Function.Injective fun x => x ^ 2
-- Std.Data.TreeSet.Basic
Std.TreeSet.mk.sizeOf_spec : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet._auto_1} [inst : SizeOf α]
  (inner : Std.TreeMap α Unit cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Data.Set.Card
Set.encard_le_encard : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.encard ≤ t.encard
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.image_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → ↑e '' (e.source ∩ s) = e.target ∩ t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGT_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, cmp a k = Ordering.gt} (h : t₁.Equiv t₂),
  Std.DTreeMap.Const.getEntryGT t₁ k h' = Std.DTreeMap.Const.getEntryGT t₂ k ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.E.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {i j k l : ι} (f₁ f₁_1 : i ⟶ j),
      f₁ = f₁_1 →
        ∀ (f₂ f₂_1 : j ⟶ k),
          f₂ = f₂_1 →
            ∀ (f₃ f₃_1 : k ⟶ l),
              f₃ = f₃_1 →
                ∀ (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1) (n₂ n₂_1 : ℤ) (e_n₂ : n₂ = n₂_1)
                  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
                  X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = X_1.E f₁_1 f₂_1 f₃_1 n₀_1 n₁_1 n₂_1 ⋯ ⋯
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)) (a : α), (f.comp g) a = f (g a)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- `S.map (chainsFunctor k G)` is short exact in each degree.  -/
groupHomology.map_chainsFunctor_eval_shortExact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact →
    ∀ (n : ℕ),
      (X.map
          ((groupHomology.chainsFunctor k G).comp
            (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) n))).ShortExact
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Adds the assignments `e' := v` to `a` for each `e'` in the equivalence class os `e`.
 -/
Lean.Meta.Grind.Arith.assignEqc : Lean.Meta.Grind.Goal → Lean.Expr → ℚ → Std.HashMap Lean.Expr ℚ → Std.HashMap Lean.Expr ℚ
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.mk : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → {X₁ : C₁} → (w : Φ.functor.obj X₁ ⟶ X₂) → W₂ w → Φ.LeftResolution X₂
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.mk : Array Lean.Expr → Array Lean.Expr → Lean.Expr.ReplaceLevelImpl.State
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  ModuleCat.Hom.hom (groupHomology.mapCycles₂ f φ) = (ModuleCat.Hom.hom (groupHomology.chainsMap₂ f φ)).restrict ⋯
-- Mathlib.Topology.Piecewise
continuous_if : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {p : α → Prop}
  [inst_2 : (a : α) → Decidable (p a)],
  (∀ a ∈ frontier {x | p x}, f a = g a) →
    ContinuousOn f (closure {x | p x}) →
      ContinuousOn g (closure {x | ¬p x}) → Continuous fun a => if p a then f a else g a
-- Mathlib.RingTheory.Ideal.Maps
Ideal.IsPrime.comap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {K : Ideal S} [inst_3 : RingHomClass F R S] [hK : K.IsPrime], (Ideal.comap f K).IsPrime
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat.injEq : ∀ (a b : Lean.Expr) (natStructId : ℕ) (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr) (a_1 b_1 : Lean.Expr)
  (natStructId_1 : ℕ) (la_1 lb_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a b natStructId la lb =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a_1 b_1 natStructId_1 la_1 lb_1) =
    (a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ la = la_1 ∧ lb = lb_1)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.span_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K)) =
    NumberField.mixedEmbedding.integerLattice K
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.catalan.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Init.Data.Range.Basic
Std.Legacy.Range.instForMNatOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForM m Std.Legacy.Range ℕ
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfigCtx.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Simp.ConfigCtx
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ), sq.unop.f₁₃ = sq.f₃₄.unop
-- Std.Http.Data.Status
Std.Http.instReprCustomStatus : Repr Std.Http.CustomStatus
-- Mathlib.SetTheory.Cardinal.Finite
Set.Infinite.card_eq_zero : ∀ {α : Type u_1} {s : Set α}, s.Infinite → Nat.card ↑s = 0
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.toClosedSubmodule_inj : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] {S T : StandardSubspace H},
  S.toClosedSubmodule = T.toClosedSubmodule ↔ S = T
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasProd.multipliable : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  {a : α}, HasProd f a L → Multipliable f L
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- The supremum of the elements of `s` less than `a` if there are some, otherwise `⊤`.  -/
Finset.truncatedSup : {α : Type u_1} → [inst : SemilatticeSup α] → [DecidableLE α] → [OrderTop α] → Finset α → α → α
-- Mathlib.Algebra.MonoidAlgebra.Opposite
AddMonoidAlgebra.opRingEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Add M] (a : (AddMonoidAlgebra R M)ᵐᵒᵖ),
  AddMonoidAlgebra.opRingEquiv a =
    (AddMonoidAlgebra.mapAddEquiv Mᵃᵒᵖ MulOpposite.opAddEquiv)
      ((AddMonoidAlgebra.mapDomainAddEquiv R AddOpposite.opEquiv) (MulOpposite.unop a))
-- Std.Do.PostCond
Std.Do.ExceptConds.snd_and : ∀ {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)},
  (x₁ ∧ₑ x₂).2 = (x₁.2 ∧ₑ x₂.2)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.inv_fun_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h =
    CategoryTheory.CategoryStruct.comp (e.unitInv.app X)
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h))
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  Differentiable 𝕜 a → ∀ (b : 𝔸), Differentiable 𝕜 fun y => a y * b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.compHom_hom : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (g : Y ⟶ Z),
  (f.compHom g).hom = CategoryTheory.CategoryStruct.comp f.hom g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  {f : β → β}, Std.DTreeMap.Const.get? (Std.DTreeMap.Const.modify t k f) k = Option.map f (Std.DTreeMap.Const.get? t k)
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.sup : ∀ {M : Type u_1} [inst : Monoid M] {P Q : Submonoid M}, P.FG → Q.FG → (P ⊔ Q).FG
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticRelatedInformation : Inhabited Lean.Lsp.DiagnosticRelatedInformation