mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
/-- Given surjections `⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀` in a concrete category whose forgetful functor
preserves sequential limits, the projection map `lim Xₙ ⟶ X₀` is surjective.
 -/
CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget C)] {F : CategoryTheory.Functor ℕᵒᵖ C}
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
  (∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) →
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app (Opposite.op 0)))
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.instNeBotAtImInfty : UpperHalfPlane.atImInfty.NeBot
-- Init.Data.UInt.Lemmas
UInt64.zero_sub : ∀ (a : UInt64), 0 - a = -a
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom.injEq : ∀ (α α_1 : Mathlib.Tactic.BicategoryLike.StructuralAtom),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α = Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α_1) =
    (α = α_1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap✝ t n φ).hom₂ = φ
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a Haar measure under map of a left action is again a Haar measure.  -/
MeasureTheory.Measure.isHaarMeasure_map_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] {α : Type u_3} [BorelSpace G] [IsTopologicalGroup G]
  [inst_6 : Group α] [inst_7 : MulAction α G] [SMulCommClass α G G] [ContinuousConstSMul α G] (a : α),
  (MeasureTheory.Measure.map (fun x => a • x) μ).IsHaarMeasure
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExceptSeries_of_notMem : ∀ (L : PeriodPair), ∀ l₀ ∉ L.lattice, L.weierstrassPExceptSeries l₀ = L.weierstrassPSeries
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.name.sizeOf_spec : ∀ (n : String), sizeOf (Lean.Lsp.InlayHintLabel.name n) = 1 + sizeOf n
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.one_def : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  1 = LinearIsometryEquiv.refl R E
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
Std.Tactic.BVDecide.BVExpr.bitblast.blastNot : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a b : α), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Mathlib.Order.RelSeries
RelSeries.last_smash : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head), (p.smash q h).last = q.last
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.colStochastic.eq_1 : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R],
  Matrix.colStochastic R n =
    { carrier := {M | (∀ (i j : n), 0 ≤ M i j) ∧ Matrix.vecMul 1 M = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_roc_eq_mkSlice_rcc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Rcc.Sliceable.mkSlice xs (lo + 1)...=hi
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_self : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : M →ₗ[R] M'),
  ((b.constr S) fun i => f (b i)) = f
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- Pointwise, the indicators of closed δ-thickenings of a set eventually coincide
with the indicator of the set as δ tends to zero.  -/
indicator_cthickening_eventually_eq_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] (f : α → β) (E : Set α) (x : α),
  ∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).indicator f x = (closure E).indicator f x
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_comp_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.quotTensorEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R (R ⧸ I) M) 1 = (I • ⊤).mkQ
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (x : G), x ∈ K.toSubmonoid ↔ x ∈ K
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.stxTrav : Lean.PrettyPrinter.Parenthesizer.State → Lean.Syntax.Traverser
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreFunctor_obj_obj_of : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Core (CategoryTheory.Functor C D)) (X : CategoryTheory.Core C),
  (((CategoryTheory.coreFunctor C D).obj F).obj X).of = F.of.obj X.of
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_single_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M},
  a ≠ a' → (Finsupp.erase a fun₀ | a' => b) = fun₀ | a' => b
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf : ∀ (R : Type u) [inst : Ring R],
  (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Full
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_mvPolynomial : ∀ {R : Type u} {ι : Type w} [inst : CommRing R], (Algebra.Generators.mvPolynomial R ι).ker = ⊥
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_nat_mul_two_pi : ∀ (n : ℕ), Complex.cos (↑n * (2 * ↑Real.pi)) = 1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_inv : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  (ϕ : A₁ ≃ₐ[R] A₁), ⇑ϕ⁻¹ = ⇑ϕ.symm
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ A`, the centralizer of `S ⊗ 1 ⊆ A ⊗ B` is `C_A(S) ⊗ B` where `C_A(S)` is the
centralizer of `S` in `A`.
 -/
Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Set A) [Module.Free R B],
  Subalgebra.centralizer R (⇑Algebra.TensorProduct.includeLeft '' S) =
    (Algebra.TensorProduct.map (Subalgebra.centralizer R S).val (AlgHom.id R B)).range
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.resFunctor_map_hom : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type u_1} {H : Type u_2} [inst_2 : Group G]
  [inst_3 : Monoid H] (φ : H →* G) {A B : TopRep k G} (f : A ⟶ B),
  TopRep.Hom.hom ((TopRep.resFunctor φ).map f) = ContIntertwiningMap.restrict φ (TopRep.Hom.hom f)
-- Std.Sat.AIG.CachedLemmas
/-- The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices that are valid for
both.
 -/
Std.Sat.AIG.mkAtomCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (var : α) (idx : ℕ)
  {h : idx < aig.decls.size} {hbound : idx < (aig.mkAtomCached var).aig.decls.size},
  (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]
-- Std.Http.Test.Helpers
/-- Assert the response starts with `prefix_` (e.g. `"HTTP/1.1 200"`).
 -/
Std.Http.Internal.Test.assertStatus : ByteArray → String → IO Unit
-- Mathlib.Probability.UniformOn
ProbabilityTheory.pred_true_of_uniformOn_eq_one : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω},
  (ProbabilityTheory.uniformOn s) t = 1 → s ⊆ t
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (X : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom.hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Lean.Util.ReplaceLevel
Lean.Level.replace : (Lean.Level → Option Lean.Level) → Lean.Level → Lean.Level
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Given a map `f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)` and an estimate
`H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `MultilinearMap`s in the type to
`ContinuousMultilinearMap`s.  -/
MultilinearMap.mkContinuousMultilinear : {𝕜 : Type u} →
  {ι : Type v} →
    {ι' : Type v'} →
      {E : ι → Type wE} →
        {E' : ι' → Type wE'} →
          {G : Type wG} →
            [inst : Fintype ι'] →
              [inst_1 : NontriviallyNormedField 𝕜] →
                [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] →
                  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] →
                    [inst_4 : SeminormedAddCommGroup G] →
                      [inst_5 : NormedSpace 𝕜 G] →
                        [inst_6 : Fintype ι] →
                          [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] →
                            [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)] →
                              (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) →
                                (C : ℝ) →
                                  (∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i),
                                      ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) →
                                    ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_mk : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f),
  ⇑{ toLinearMap := f, isIntertwining' := h } = ⇑f
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.pnatCast.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] (a a_1 : ℕ+),
  a = a_1 → ↑a = ↑a_1
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_eval₂_eq_zero : ∀ {k : Type u} [inst : Field k] {R : Type u_1} [inst_1 : Ring R] [IsSimpleRing R] [IsAlgClosed k] (f : R →+* k)
  (p : Polynomial R), p.degree ≠ 0 → ∃ x, Polynomial.eval₂ f x p = 0
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {a : α}, m.WF → (m.insert a).WF
-- Init.Data.Array.Lemmas
Array.filterMap_replicate_of_none : ∀ {α : Type u_1} {β : Type u_2} {a : α} {n : ℕ} {f : α → Option β},
  f a = none → Array.filterMap f (Array.replicate n a) = #[]
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_mul : ∀ (m n : ℕ), m.lcm n ∣ m * n
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- `Circle.exp`, applied to a `Real.Angle`.  -/
Real.Angle.toCircle : Real.Angle → Circle
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SSet.stdSimplex.toSSetObj_app_const_one : (CategoryTheory.ConcreteCategory.hom (SSet.stdSimplex.toSSetObjI.app (Opposite.op { len := 0 })))
    (SSet.stdSimplex.const 1 1 (Opposite.op { len := 0 })) =
  TopCat.toSSetObj₀Equiv.symm 1
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_le_self : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s : Set α), (MeasureTheory.OuterMeasure.restrict s) m ≤ m
-- Mathlib.Algebra.Star.Unitary
Unitary.instStarMulSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → StarMul ↥(unitary R)
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
/-- The counit of the derived adjunction, see `Adjunction.derived`.  -/
CategoryTheory.Adjunction.derivedε : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      {L₁ : CategoryTheory.Functor C₁ D₁} →
                        {L₂ : CategoryTheory.Functor C₂ D₂} →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            [inst_4 : L₂.IsLocalization W₂] →
                              {G' : CategoryTheory.Functor D₁ D₂} →
                                {F' : CategoryTheory.Functor D₂ D₁} →
                                  (L₁.comp G' ⟶ G.comp L₂) →
                                    (β : F.comp L₁ ⟶ L₂.comp F') →
                                      [(F'.comp G').IsRightDerivedFunctor
                                            (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom)
                                            W₂] →
                                        F'.comp G' ⟶ CategoryTheory.Functor.id D₂
-- Mathlib.Algebra.Ring.Invertible
invOf_neg : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) [inst_2 : Invertible a]
  [inst_3 : Invertible (-a)], ⅟(-a) = -⅟a
-- Mathlib.RingTheory.Perfection
PerfectionMap.surjective : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₂}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R},
  PerfectionMap p π →
    ∀ (f : ℕ → R), (∀ (n : ℕ), f (n + 1) ^ p = f n) → ∃ x, ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n
-- Std.Sat.AIG.Lemmas
/-- `AIG.mkConst` never shrinks the underlying AIG.
 -/
Std.Sat.AIG.mkConst_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool),
  aig.decls.size ≤ (aig.mkConst val).aig.decls.size
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.toList_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [inst_1 : Std.Iterators.Finite α Id],
  (it.attachWith P hP).toList = it.toList.attachWith P ⋯
-- Init.Data.List.Basic
/-- Removes all elements of `xs` that are present in `ys`.

`O(|xs| * |ys|)`.

Examples:
* `[1, 1, 5, 1, 2, 4, 5].removeAll [1, 2, 2] = [5, 4, 5]`
* `[1, 2, 3, 2].removeAll [] = [1, 2, 3, 2]`
* `[1, 2, 3, 2].removeAll [3] = [1, 2, 2]`
 -/
List.removeAll : {α : Type u} → [BEq α] → List α → List α → List α
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityUnit'_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D)
  (c : CategoryTheory.Limits.Cone (K.comp G)), ((adj.functorialityUnit' K).app c).hom = adj.unit.app c.pt
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
-- Lean.Compiler.IR.Basic
Lean.IR.instReprJoinPointId : Repr Lean.IR.JoinPointId
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_sub : ∀ {R : Type u_1} [inst : Ring R] {S : Type u_2} [inst_1 : Ring S] (p : SkewPolynomial R) (f g : ℕ → R → S),
  (p.sum fun n x => f n x - g n x) = p.sum f - p.sum g
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonDeclInfo : Lean.ToJson Lean.Lsp.DeclInfo
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toArray_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {f : α → Bool},
  t.WF → (Std.TreeSet.Raw.filter f t).toArray = Array.filter f t.toArray
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.iUnion_openCell_eq_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (n : ℕ∞), D ∪ ⋃ m, ⋃ (_ : ↑m < n + 1), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeleton C n)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.dualEquiv_inverse : FinBoolAlg.dualEquiv.inverse = FinBoolAlg.dual
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumToIter_Xr : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₂),
  (MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inr c)) = MvPolynomial.C (MvPolynomial.X c)
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies the expression `Int.natAbs n` such that
`norm_num` successfully recognizes `n`.  -/
Mathlib.Meta.NormNum.evalIntNatAbs : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.BinaryCofan.ext.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryCofan A B}
  (e e_1 : c.pt ≅ c'.pt) (e_e : e = e_1) (h₁ : CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl)
  (h₂ : CategoryTheory.CategoryStruct.comp c.inr e.hom = c'.inr),
  CategoryTheory.Limits.BinaryCofan.ext e h₁ h₂ = CategoryTheory.Limits.BinaryCofan.ext e_1 ⋯ ⋯
-- Init.Grind.Order
Lean.Grind.Order.le_of_eq_1_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α}, a = b → a ≤ b + ↑0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.eta_hom_hom : ∀ {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.Cocone F),
  c.eta.hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.mk : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w) →
    (∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
        (map.get k h1)[i].gate < aig.decls.size) →
      Std.Tactic.BVDecide.BVExpr.Cache aig
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_le_comap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup N),
  f.ker ≤ AddSubgroup.comap f H
-- Init.Core
Function.true_comp : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, (fun x => true) ∘ f = fun x => true
-- Mathlib.Order.Compare
/-- Like `cmp`, but uses a `≤` on the type instead of `<`. Given two elements `x` and `y`, returns a
three-way comparison result `Ordering`.  -/
cmpLE : {α : Type u_3} → [inst : LE α] → [DecidableLE α] → α → α → Ordering
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → γ)
  (c : γ), ⇑(MeasureTheory.SimpleFunc.map g f) ⁻¹' {c} = ⇑f ⁻¹' ↑({b ∈ f.range | g b = c})
-- Init.Data.Order.FactoriesExtra
Std.compare_ne_eq : ∀ {α : Type u} [inst : Ord α] [inst_1 : BEq α] [inst_2 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulOrderBEq α] {a b : α},
  compare a b ≠ Ordering.eq ↔ ¬(a == b) = true
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coxeterWeight_swap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.coxeterWeight i j = P.coxeterWeight j i
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).inverse.obj X).obj.map f = X.obj.map (e.functor.map f.unop).op
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.apply_inl : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Combinatorics.Subspace η α ι} {x : η → α} {i : ι} {a : α},
  l.idxFun i = Sum.inl a → ↑l x i = a
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.select : Std.Async.Waiter (Option Std.Http.Chunk) → Std.Http.Body.Channel.Consumer✝
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl α β)
  (next : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.size✝ (Std.DTreeMap.Internal.Zipper.cons k v tree next) =
    1 + tree.treeSize + Std.DTreeMap.Internal.Zipper.size✝ next
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- `LinearMap.toMatrix₂ b₁ b₂` is the equivalence between `R`-sesquilinear maps
`M₁ →ₛₗ[σ₁] M₂ →ₗ[σ₂] N₂` and `n`-by-`m` matrices with entries in `N₂`,
if `b₁` and `b₂` are `R`-bases for `M₁` and `M₂`,
respectively.  -/
LinearMap.toMatrix₂ : {R : Type u_1} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      {N₂ : Type u_10} →
        {n : Type u_11} →
          {m : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid M₁] →
                [inst_2 : Module R M₁] →
                  [inst_3 : AddCommMonoid M₂] →
                    [inst_4 : Module R M₂] →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Module R N₂] →
                          {σ₁ σ₂ : R →+* R} →
                            [Fintype n] →
                              [Fintype m] →
                                [DecidableEq m] →
                                  [DecidableEq n] →
                                    Module.Basis n R M₁ →
                                      Module.Basis m R M₂ → (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂