mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_mk_iff : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N],
  CommRing.Pic.mk R M = CommRing.Pic.mk R N ↔ Nonempty (M ≃ₗ[R] N)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.prodMk : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G},
  f =O[𝕜; l] k → g =O[𝕜; l] k → (fun x => (f x, g x)) =O[𝕜; l] k
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.homQuotientZSMulOfHom_id : ∀ {A : Type u} [inst : AddCommGroup A] (n : ℤ),
  QuotientAddGroup.homQuotientZSMulOfHom (AddMonoidHom.id A) n = AddMonoidHom.id (A ⧸ (zsmulAddGroupHom n).range)
-- Init.Data.UInt.Lemmas
UInt64.not_le : ∀ {a b : UInt64}, ¬a ≤ b ↔ b < a
-- Mathlib.Order.Cofinal
isCofinal_singleton_iff : ∀ {α : Type u_1} [inst : LE α] {x : α}, IsCofinal {x} ↔ IsTop x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_comp_d₁₀ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₂₁ A) (groupHomology.d₁₀ A) = 0
-- Mathlib.CategoryTheory.Subobject.Types
subtype_val_mono : ∀ {α : Type u} (s : Set α), CategoryTheory.Mono (TypeCat.ofHom Subtype.val)
-- Mathlib.Data.Set.Lattice
Set.subset_powerset_iff : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.instNontrivial : ∀ {V : Type u} [Nontrivial V], Nontrivial (SimpleGraph V)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- Let `C` be a Grothendieck abelian category with a generator (`hG`),
`X : C`, `A₀ : Subobject X`. Let `J` be a well-ordered type. This is
the functor `J ⥤ MonoOver X` which corresponds to the evaluation
at `A₀` of the transfinite iteration of the map
`largerSubobject hG : Subobject X → Subobject X`.  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [inst_1 : CategoryTheory.Abelian C] →
        CategoryTheory.IsSeparator G →
          {X : C} →
            [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
              CategoryTheory.Subobject X →
                (J : Type w) →
                  [inst_3 : LinearOrder J] →
                    [OrderBot J] →
                      [SuccOrder J] → [WellFoundedLT J] → CategoryTheory.Functor J (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.instAddAction : {M : Type u_1} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction M αᵃᵒᵖ
-- Mathlib.Order.Category.PartOrd
/-- `PreordToPartOrd` and `OrderDual` commute.  -/
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd : preordToPartOrd.comp PartOrd.dual ≅ Preord.dual.comp preordToPartOrd
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instInhabited : (M : Type u_4) → [inst : AddZero M] → Inhabited (AddMonoid.End M)
-- Mathlib.CategoryTheory.Join.Final
/-- The category of `Join.inclRight C D`-structured arrows with source `left c` is equivalent to
`D`.  -/
CategoryTheory.Join.structuredArrowEquiv : (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] →
        (c : C) → CategoryTheory.StructuredArrow (CategoryTheory.Join.left c) (CategoryTheory.Join.inclRight C D) ≌ D
-- Mathlib.CategoryTheory.Galois.Basic
/-- In a `GaloisCategory` the set of morphisms out of a connected object is finite.  -/
CategoryTheory.PreGaloisCategory.instFiniteHomOfIsConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (A X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A], Finite (A ⟶ X)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isOpenEmbedding_sigmaToPi : ∀ {ι : Type u_1} (R : ι → Type u_2) [inst : (i : ι) → CommRing (R i)],
  Topology.IsOpenEmbedding (PrimeSpectrum.sigmaToPi R)
-- Mathlib.CategoryTheory.Action.Basic
/-- The composition of two `Action V G` homomorphisms is the composition of the underlying maps.
 -/
Action.Hom.comp : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → {M N K : Action V G} → M.Hom N → N.Hom K → M.Hom K
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `g` is a multilinear map and `f` is a collection of linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a multilinear map, that we call
`g.compLinearMap f`.  -/
MultilinearMap.compLinearMap : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₁' : ι → Type v₁'} →
        {M₂ : Type v₂} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : (i : ι) → Module R (M₁ i)] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] →
                      [inst_6 : (i : ι) → Module R (M₁' i)] →
                        MultilinearMap R M₁' M₂ → ((i : ι) → M₁ i →ₗ[R] M₁' i) → MultilinearMap R M₁ M₂
-- Mathlib.Algebra.Ring.Basic
NoZeroDivisors.to_isCancelMulZero : ∀ (R : Type u_3) [inst : NonUnitalNonAssocRing R] [NoZeroDivisors R], IsCancelMulZero R
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearCnstr : Type
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection_mem_dilatransvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hfv : f v = 0), LinearEquiv.transvection hfv ∈ LinearEquiv.dilatransvections R V
-- Init.Data.List.Nat.Basic
List.getElem_eq_getElem_intersperse_two_mul : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ} (h : i < l.length), l[i] = (List.intersperse sep l)[2 * i]
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F], Differentiable 𝕜 0
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.funext : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ}
  [inst_1 : TopologicalSpace β] [T2Space β] {f g : pkg.space → β},
  Continuous f → Continuous g → (∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) → f = g
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.equiv_symm_eq_conj : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B),
  HNNExtension.of ↑(φ.symm b) = HNNExtension.t⁻¹ * HNNExtension.of ↑b * HNNExtension.t
-- Std.Time.DateTime.Timestamp
/-- Converts a `Timestamp` to a `Minute.Offset`.
 -/
Std.Time.Timestamp.toMinutesSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Minute.Offset
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_le_of_ne`. -/
LE.le.lt_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonHighlightMatchesOptions.toJson : Lean.Lsp.HighlightMatchesOptions → Lean.Json
-- Lean.Parser.Types
Lean.Parser.SyntaxNodeKindSet : Type
-- Mathlib.Algebra.Module.Projective
/-- A quotient of a projective module is projective iff it is a direct summand.  -/
Module.Projective.iff_split_of_projective : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Projective R M] (s : M →ₗ[R] P),
  Function.Surjective ⇑s → (Module.Projective R P ↔ ∃ i, s ∘ₗ i = LinearMap.id)
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* P) (g : N →* P), f.coprod g = f.comp (MonoidHom.fst M N) * g.comp (MonoidHom.snd M N)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the atomic 2-morphism `η` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalOf : {m : Type → Type} → [self : Mathlib.Tactic.BicategoryLike.MkEval m] → Mathlib.Tactic.BicategoryLike.Atom → m Lean.Expr
-- Init.Data.Rat.Lemmas
Rat.pow_nonneg : ∀ {a : ℚ} {n : ℕ}, 0 ≤ a → 0 ≤ a ^ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.tan_eq_zero_iff : ∀ {θ : ℝ}, Real.tan θ = 0 ↔ ∃ k, ↑k * Real.pi / 2 = θ
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
/-- This is a version of `hasProdUniformlyOn_one_add` for sequences indexed by `ℕ`.  -/
Summable.hasProdUniformlyOn_nat_one_add : ∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] {f : ℕ → α → R},
  IsCompact K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) →
            HasProdUniformlyOn (fun n x => 1 + f n x) (fun x => ∏' (i : ℕ), (1 + f i x)) K
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoLeft_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G),
  (adj.ofNatIsoLeft iso).counit = CategoryTheory.CategoryStruct.comp (H.whiskerLeft iso.inv) adj.counit
-- Init.Data.SInt.Lemmas
Int64.toISize_sub : ∀ (a b : Int64), (a - b).toISize = a.toISize - b.toISize
-- Mathlib.Order.Concept
Concept.instMax : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Max (Concept α β r)
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.directedOn : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeInf α], CountableInfClosed s → DirectedOn (fun x1 x2 => x2 ≤ x1) s
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
left_lt_lineMap_iff_pos : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → (a < (AffineMap.lineMap a b) r ↔ 0 < r)
-- Lean.Elab.SyntheticMVars
/-- Report an error for each synthetic metavariable that could not be resolved.
Remark: we set `ignoreStuckTC := true` when elaborating `simp` arguments.
 -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.reportStuckSyntheticMVars : optParam Bool false → Lean.Elab.TermElabM Unit
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2) (it₁' : Std.Iter β)
  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.Iter β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 : (it₁' : Std.Iter β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  ⌊1⌋₊ = 1
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.fst_sum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Multiset (M × N)),
  s.sum.1 = (Multiset.map Prod.fst s).sum
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → ∀ [Module.Flat R ↥A], Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The chain complex `X ←0- X ←𝟙- X ←0- X ←𝟙- X ⋯`.
It is exact away from `0` and has homology `X` at `0`.  -/
ChainComplex.alternatingConst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.Functor C (ChainComplex C ℕ)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_union : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s₁ s₂ : Multiset α), (s₁ ∪ s₂).lcm = lcm s₁.lcm s₂.lcm
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.rewrites_reverse : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.reverse.Rewrites u.reverse v.reverse ↔ r.Rewrites u v
-- Mathlib.Topology.Category.Stonean.Basic
/-- Every Stonean space is projective in `Profinite`  -/
Stonean.instProjectiveProfiniteObjToProfinite : ∀ (X : Stonean), CategoryTheory.Projective (Stonean.toProfinite.obj X)
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- Etale space of a presheaf.  -/
TopCat.Presheaf.EtaleSpace : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [CategoryTheory.ConcreteCategory C FC] →
              [CategoryTheory.Limits.HasColimits C] → TopCat.Presheaf C X → Type v
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given an ordered finite partition `c` of `n`, a continuous multilinear map `f` in `c.length`
variables, and for each `m` a continuous multilinear map `p m` in `c.partSize m` variables,
one can form a continuous multilinear map in `n`
variables by applying `p m` to each part of the partition, and then
applying `f` to the resulting vector. It is called `c.compAlongOrderedFinpartition f p`.  -/
OrderedFinpartition.compAlongOrderedFinpartition : {𝕜 : 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] →
                      {n : ℕ} →
                        (c : OrderedFinpartition n) →
                          (F [×c.length]→L[𝕜] G) → ((i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) → E [×n]→L[𝕜] G
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprLambdaTheoremType.repr : Mathlib.Meta.FunProp.LambdaTheoremType → ℕ → Std.Format
-- Mathlib.Data.Bundle
Bundle.Pullback.lift_mk : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (x : B') (y : E (f x)),
  Bundle.Pullback.lift f ⟨x, y⟩ = ⟨f x, y⟩
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_4 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.mulAssoc = ∀ (x y z : K), x * y * z = x * (y * z)
-- Init.Data.List.Impl
/-- Auxiliary for `eraseTR`: `eraseTR.go l a xs acc = acc.toList ++ erase xs a`,
unless `a` is not present in which case it returns `l`  -/
_private.Init.Data.List.Impl.0.List.eraseTR.go : {α : Type u_1} → [BEq α] → List α → α → List α → Array α → List α
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- The number of equalities, or `none` in the case when we've reduced something
of the form `p ∧ True` to just `p`.
 -/
Mathlib.Tactic.MkIff.Shape.neqs : Mathlib.Tactic.MkIff.Shape → Option ℕ
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionClientCapabilities.mk.injEq : ∀ (dynamicRegistration? isPreferredSupport? disabledSupport? dataSupport? honorsChangeAnnotations? : Option Bool)
  (codeActionLiteralSupport? : Option Lean.Lsp.CodeActionLiteralSupport)
  (resolveSupport? : Option Lean.Lsp.ResolveSupport)
  (dynamicRegistration?_1 isPreferredSupport?_1 disabledSupport?_1 dataSupport?_1 honorsChangeAnnotations?_1 :
    Option Bool)
  (codeActionLiteralSupport?_1 : Option Lean.Lsp.CodeActionLiteralSupport)
  (resolveSupport?_1 : Option Lean.Lsp.ResolveSupport),
  ({ dynamicRegistration? := dynamicRegistration?, isPreferredSupport? := isPreferredSupport?,
        disabledSupport? := disabledSupport?, dataSupport? := dataSupport?,
        honorsChangeAnnotations? := honorsChangeAnnotations?, codeActionLiteralSupport? := codeActionLiteralSupport?,
        resolveSupport? := resolveSupport? } =
      { dynamicRegistration? := dynamicRegistration?_1, isPreferredSupport? := isPreferredSupport?_1,
        disabledSupport? := disabledSupport?_1, dataSupport? := dataSupport?_1,
        honorsChangeAnnotations? := honorsChangeAnnotations?_1,
        codeActionLiteralSupport? := codeActionLiteralSupport?_1, resolveSupport? := resolveSupport?_1 }) =
    (dynamicRegistration? = dynamicRegistration?_1 ∧
      isPreferredSupport? = isPreferredSupport?_1 ∧
        disabledSupport? = disabledSupport?_1 ∧
          dataSupport? = dataSupport?_1 ∧
            honorsChangeAnnotations? = honorsChangeAnnotations?_1 ∧
              codeActionLiteralSupport? = codeActionLiteralSupport?_1 ∧ resolveSupport? = resolveSupport?_1)
-- Mathlib.Data.Fin.VecNotation
Matrix.vecTail.eq_1 : ∀ {α : Type u} {n : ℕ} (v : Fin n.succ → α), Matrix.vecTail v = v ∘ Fin.succ
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.disjoint_right : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K), Disjoint K ↑C
-- Mathlib.CategoryTheory.Adhesive.Over
/-- Slices of adhesive categories are adhesive. See [adhesive2004], Proposition 8 (ii).  -/
CategoryTheory.adhesive_over : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Adhesive C]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPushouts C] (B : C),
  CategoryTheory.Adhesive (CategoryTheory.Over B)
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s' : Stream'.Seq1 α) → motive (some s')),
  (match none with
    | none => h_1 ()
    | some s' => h_2 s') =
    h_1 ()
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- An intermediate equivalence `A ≌ B` obtained as the composition of `equivalence₁` and
the inverse of `eB : B ≌ B'`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalence₂ : {A : Type u_1} →
  {A' : Type u_2} →
    {B : Type u_3} →
      {B' : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] →
                {eA : A ≌ A'} →
                  (B ≌ B') →
                    {e' : A' ≌ B'} → {F : CategoryTheory.Functor A B'} → (eA.functor.comp e'.functor ≅ F) → (A ≌ B)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
tendsto_div_comap_self : ∀ {α : Type u_1} {β : Type u_2} {hom : Type u_3} [inst : TopologicalSpace α] [inst_1 : Group α] [IsTopologicalGroup α]
  [inst_3 : TopologicalSpace β] [inst_4 : Group β] [inst_5 : FunLike hom β α] [MonoidHomClass hom β α] {e : hom},
  IsDenseInducing ⇑e →
    ∀ (x₀ : α), Filter.Tendsto (fun t => t.2 / t.1) (Filter.comap (fun p => (e p.1, e p.2)) (nhds (x₀, x₀))) (nhds 1)
-- Mathlib.Algebra.Torsor.Basic
Equiv.constSMul_mul : ∀ {G : Type u_1} (P : Type u_2) [inst : Group G] [inst_1 : Torsor G P] (v₁ v₂ : G),
  Equiv.constSMul P (v₁ * v₂) = Equiv.constSMul P v₁ * Equiv.constSMul P v₂
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- Uniqueness (up to a natural isomorphism) of the right derived functor.  -/
CategoryTheory.Functor.rightDerivedUnique : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (RF RF' : CategoryTheory.Functor D H) →
              {F : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : F ⟶ L.comp RF) →
                    (α'₂ : F ⟶ L.comp RF') →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] →
                          [RF.IsRightDerivedFunctor α W] → [RF'.IsRightDerivedFunctor α'₂ W] → RF ≅ RF'
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Topology.IsEmbedding ⇑h
-- Init.Data.Char.Basic
/-- Returns `true` if the character is an ASCII digit.

The ASCII digits are the following: `0123456789`.
 -/
Char.isDigit : Char → Bool
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- **Alias** of `TopologicalSpace.generatedBy_eq_coinduced`. -/
deltaGenerated_eq_coinduced : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  TopologicalSpace.generatedBy X = TopologicalSpace.coinduced (fun x => x.fst.snd x.snd) inferInstance
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_trans`. -/
Dvd.dvd.trans : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, x⁻¹y)` is measure-preserving.
This is the function `S⁻¹` in [Halmos, §59],
where `S` is the map `(x, y) ↦ (x, xy)`.  -/
MeasureTheory.measurePreserving_prod_inv_mul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [ν.IsMulLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.1⁻¹ * z.2)) (μ.prod ν) (μ.prod ν)
-- Mathlib.GroupTheory.Congruence.Star
ConGen.Rel.star : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : StarMul M] {r : M → M → Prop},
  (∀ (a b : M), r a b → r (star a) (star b)) → ∀ ⦃a b : M⦄, ConGen.Rel r a b → ConGen.Rel r (star a) (star b)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.Pentagonal.summable_pow_mul_prod_one_sub_pow : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] (k : ℕ),
  Summable fun n => PowerSeries.X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - PowerSeries.X ^ (k + i + 1))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.toCoalgHom_mulBialgHom : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Bialgebra R A],
  (Bialgebra.mulBialgHom R A).toCoalgHom = Bialgebra.mulCoalgHom R A
-- Init.Prelude
/-- The length of a list.

This function is overridden in the compiler to `lengthTR`, which uses constant stack space.

Examples:
* `([] : List String).length = 0`
* `["green", "brown"].length = 2`
 -/
List.length : {α : Type u_1} → List α → ℕ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, Option.all (fun x_2 => x_2 == k) (m.getKey? k) = true