mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_hom_comp_i_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 2)),
  (ModuleCat.Hom.hom (groupCohomology.shortComplexH2 A).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₂ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 2)) x)
-- Mathlib.Logic.Godel.GodelBetaFunction
Nat.chineseRemainderOfFinset.congr_simp : ∀ {ι : Type u_1} (a s : ι → ℕ) (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0)
  (pp : (↑t).Pairwise (Function.onFun Nat.Coprime s)),
  Nat.chineseRemainderOfFinset a s t hs pp = Nat.chineseRemainderOfFinset a s t hs pp
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.«termCoeff(_)» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyπ j)
      (HomologicalComplex.singleObjHomologySelfIso c j A).hom =
    (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ne_of_ne : ∀ {a b : UInt16}, a ≠ b → a.toBitVec ≠ b.toBitVec
-- Init.Data.Vector.Lemmas
Vector.foldrM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → β → m β} {b : β}
  {xs : Array α} (h : xs.size = n), Vector.foldrM f b (Vector.mk xs h) = Array.foldrM f b xs
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
le_minSmoothness : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}, n ≤ minSmoothness 𝕜 n
-- Mathlib.Analysis.Convex.Function
ConvexOn.add_strictConvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  ConvexOn 𝕜 s f → StrictConvexOn 𝕜 s g → StrictConvexOn 𝕜 s (f + g)
-- Std.Net.Addr
Std.Net.instDecidableEqMACAddr : DecidableEq Std.Net.MACAddr
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.IsInternal.baseChange : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [inst_4 : CommSemiring S]
  [inst_5 : Algebra R S], DirectSum.IsInternal ℳ → DirectSum.IsInternal fun i => Submodule.baseChange S (ℳ i)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Coefficients of Hahn series for each `baseDomain` element.  -/
HahnEmbedding.Seed.hahnCoeff : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              (seed : HahnEmbedding.Seed K M R) →
                                ↥seed.baseDomain →ₗ[K] DirectSum (FiniteArchimedeanClass M) fun x => R
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonPMF.eq_1 : ∀ (r : NNReal), ProbabilityTheory.poissonPMF r = ⟨fun n => ENNReal.ofReal (ProbabilityTheory.poissonPMFReal r n), ⋯⟩
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_push_lt : ∀ (data : ByteArray) (b : UInt8), ∀ i < data.size, (data.push b)[i]! = data[i]!
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Opens.coverDense_inducedFunctor : ∀ {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X},
  TopologicalSpace.Opens.IsBasis (Set.range B) →
    (CategoryTheory.inducedFunctor B).IsCoverDense (Opens.grothendieckTopology ↑X)
-- Init.Data.Option.Basic
instMonadExceptOfUnitOption : MonadExceptOf Unit Option
-- Lean.Expr
/-- Return `true` if the given `BinderInfo` is a regular implicit annotation (e.g., `{α : Type u}`)  -/
Lean.BinderInfo.isImplicit : Lean.BinderInfo → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.instIsCompatibleWithShiftIntUpQuasiIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.instDecidable.eq_1 : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : DecidableEq α] {s : Finset α},
  ThreeAPFree.instDecidable = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a + c = b + b → a = b) ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsImmersion (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.Algebra.Group.Shrink
Shrink.instPow.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Pow α M],
  Shrink.instPow = Equiv.pow M (equivShrink α).symm
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.normAtComplexPlaces
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x)) =
    NumberField.mixedEmbedding.normAtAllPlaces x
-- Mathlib.Data.Multiset.Antidiagonal
/-- The antidiagonal of a multiset `s` consists of all pairs `(t₁, t₂)`
such that `t₁ + t₂ = s`. These pairs are counted with multiplicities.  -/
Multiset.antidiagonal : {α : Type u_1} → Multiset α → Multiset (Multiset α × Multiset α)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (version? : Option ℤ) (isIncremental? : Option Bool)
  (diagnostics : Array Lean.Lsp.Diagnostic),
  sizeOf { uri := uri, version? := version?, isIncremental? := isIncremental?, diagnostics := diagnostics } =
    1 + sizeOf uri + sizeOf version? + sizeOf isIncremental? + sizeOf diagnostics
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleCompEval_hom_app : ∀ {J : Type u_1} (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) (X : C),
  (CategoryTheory.GradedObject.singleCompEval C j).hom.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).hom
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str : ∀ (X : FinBoolAlg),
  (CategoryTheory.HasForget₂.forget₂.obj X).str =
    BooleanAlgebra.toBiheytingAlgebra.toCoheytingAlgebra.toSemilatticeInf.toPartialOrder
-- Init.Data.List.Control
/-- Returns true if the monadic predicate `p` returns `true` for every element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `false`. The elements in `l` are examined in
order from left to right.
 -/
List.allM : {m : Type → Type u} → [Monad m] → {α : Type v} → (α → m Bool) → List α → m Bool
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.box.eq_1 : ∀ (n d : ℕ), Behrend.box n d = Fintype.piFinset fun x => Finset.range d
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- The forgetful functor from commutative comonoid objects to comonoid objects.  -/
CategoryTheory.CommComon.forget₂Comon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommComon C) (CategoryTheory.Comon C)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorRxcIteratorIdSigma.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α],
  Std.DTreeMap.Internal.instIteratorRxcIteratorIdSigma =
    { IsPlausibleStep := fun it step => it.internalState.step = step,
      step := fun it => pure (Std.Shrink.deflate ⟨it.internalState.step, ⋯⟩) }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.proj_apply : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i),
  (ContinuousLinearMap.proj i) b = b i
-- Mathlib.Algebra.Group.Basic
mul_mul_div_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a * c * (b / c) = a * b
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_incl_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I I₂ : LieIdeal R L},
  LieIdeal.comap I.incl I₂ = ⊥ ↔ Disjoint I I₂
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_edist_left : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {x : α},
  Measurable fun y => edist y x
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac.inj : ∀ {r₁ c r₂ : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {r₁_1 c_1 r₂_1 : Lean.Grind.AC.Seq}
  {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁ c r₂ c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁_1 c_1 r₂_1 c₁_1 c₂_1 →
    r₁ = r₁_1 ∧ c = c_1 ∧ r₂ = r₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Algebra.Lie.SemiDirect
/-- The canonical inclusion of L into the semi-direct sum K ⋊⁅ψ⁆ G.  -/
LieAlgebra.SemiDirectSum.inr : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → L →ₗ⁅R⁆ K ⋊⁅ψ⁆ L
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M), f.invtSubmodule = { carrier := {p | p ≤ Submodule.comap f p}, supClosed' := ⋯, infClosed' := ⋯ }
-- Mathlib.Combinatorics.Hindman
/-- `FP a` is the set of finite products in `a`, i.e. `m ∈ FP a` if `m` is the product of a nonempty
subsequence of `a`. We give a direct inductive definition instead of talking about subsequences.  -/
Hindman.FP : {M : Type u_1} → [Semigroup M] → Stream' M → Set M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.isIso_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ'),
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.left ∧ CategoryTheory.IsIso f.base ∧ CategoryTheory.IsIso f.right
-- Mathlib.Algebra.Ring.Commute
Commute.neg_left_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute (-a) b ↔ Commute a b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Compositional version of `Finset.stronglyMeasurable_prod` for use by `fun_prop`.  -/
MeasureTheory.StronglyMeasurable.Finset.stronglyMeasurable_prod_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} {n : MeasurableSpace β} {ι : Type u_6} {f : ι → α → β → M} {g : α → β} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable ↿(f i)) →
    Measurable g → MeasureTheory.StronglyMeasurable fun a => (∏ i ∈ s, f i a) (g a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivAtFilter.finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ} {l : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter φ φ' l →
    HasDerivAtFilter φs φs' l → HasDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') l
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)) (fr : (n : ℕ) → L.Relations n ≃ L'.Relations n) {n : ℕ}
  (a : L.BoundedFormula α n),
  (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr) a =
    FirstOrder.Language.BoundedFormula.mapTermRel (fun n => ⇑(ft n)) (fun n => ⇑(fr n)) (fun x => id) a
-- Init.Data.Range.Polymorphic.PRange
/-- `*...=b` is the range of elements less than or equal to `b`. See also `Std.Ric`.  -/
Std.«term*...=_» : Lean.ParserDescr
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.toFinset = { val := s.dedup, nodup := ⋯ }
-- Mathlib.Topology.Algebra.Ring.Basic
/-- **Alias** of `IsSemitopologicalSemiring.continuousNeg_of_mul`.

---

If `R` is a ring with a separately continuous multiplication, then negation is continuous as
well since it is just multiplication with `-1`.  -/
IsTopologicalSemiring.continuousNeg_of_mul : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocRing R] [SeparatelyContinuousMul R], ContinuousNeg R
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.continuous_pow : ∀ (n : ℕ+), Continuous fun x => x ^ n
-- Mathlib.Analysis.Real.Hyperreal
/-- The canonical map `ℝ → ℝ*` as an `OrderRingHom`.  -/
Hyperreal.coeRingHom : ℝ →+*o ℝ*
-- Init.Data.Rat.Lemmas
Rat.blt.eq_1 : ∀ (a b : ℚ),
  a.blt b =
    if (decide (a.num < 0) && decide (0 ≤ b.num)) = true then true
    else
      if a.num = 0 then decide (0 < b.num)
      else if (decide (0 < a.num) && decide (b.num ≤ 0)) = true then false else decide (a.num * ↑b.den < b.num * ↑a.den)
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smul.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} [inst : MulOneClass M'] [inst_1 : SMul M' α] (S : Submonoid M'), S.smul = inferInstance
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.leftToRight.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful],
  t.leftToRight =
    CategoryTheory.CategoryStruct.comp F.rightUnitor.inv
      (CategoryTheory.CategoryStruct.comp (F.whiskerLeft t.adj₂.unit)
        (CategoryTheory.CategoryStruct.comp (F.associator G H).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.whiskerRight t.adj₁.unit H))
            H.leftUnitor.hom)))
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp_mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {s : Set M'}
  (x : M'), MDiffAt g (f x) → MDiffAt[s] f x → UniqueMDiffAt[s] x → d[s] (g ∘ f) x = d% g (f x) ∘SL mfderiv[s] f x
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_roo_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_union_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} [inst : Inhabited β] {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k' =
        if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
        else Std.DTreeMap.Internal.Impl.Const.get! t k'
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C)
  [inst_5 : CategoryTheory.Limits.HasBiproduct f] [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F] {W : C}
  (g : (j : J) → f j ⟶ W),
  CategoryTheory.CategoryStruct.comp (F.mapBiproduct f).inv (F.map (CategoryTheory.Limits.biproduct.desc g)) =
    CategoryTheory.Limits.biproduct.desc fun j => F.map (g j)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_exponent_zero : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  (f : α → E), MeasureTheory.lpNorm f 0 μ = 0
-- Mathlib.Order.Atoms
IsStronglyCoatomic.exists_le_covBy_of_lt : ∀ {α : Type u_5} {inst : Preorder α} [self : IsStronglyCoatomic α] (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `L / K` is a `p`-radical field extension, then it is purely inseparable.  -/
IsPRadical.isPurelyInseparable : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (p : ℕ) [ExpChar K p]
  [IsPRadical (algebraMap K L) p], IsPurelyInseparable K L
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.mkControlInfoElemAttributeUnsafe : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Do.ControlInfoHandler)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, Std.DTreeMap.Const.get? t k = some v ↔ ∃ (h : k ∈ t), Std.DTreeMap.Const.get t k h = v
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.Icc_eq_pi : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, BoxIntegral.Box.Icc I = Set.univ.pi fun i => Set.Icc (I.lower i) (I.upper i)
-- Init.Data.Vector.Lemmas
Vector.replicate.eq_1 : ∀ {α : Type u_1} (n : ℕ) (v : α), Vector.replicate n v = Vector.mk (Array.replicate n v) ⋯
-- Mathlib.MeasureTheory.OuterMeasure.Induced
_private.Mathlib.MeasureTheory.OuterMeasure.Induced.0.Option.elim'.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.essentiallySmall_fullSubcategory_mem : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (s : Set C) [Small.{w, u} ↑s]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.EssentiallySmall.{w, v, u} (CategoryTheory.ObjectProperty.FullSubcategory fun x => x ∈ s)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFields.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.angleDiff_add_angleDiff : ∀ {x y : Circle}, x ≠ y → x.angleDiff y + y.angleDiff x = 2 * Real.pi
-- Mathlib.Analysis.Calculus.TangentCone.Seq
/-- In a vector space with first countable topology, a vector `y` belongs to `tangentConeAt 𝕜 s x`
if and only if there exist sequences `c n` and `d n` such that

- `d n` tends to zero as `n → ∞`;
- `x + d n ∈ s` for sufficiently large `n`;
- `c n • d n` tends to `y` as `n → ∞`.

See `mem_tangentConeAt_of_seq` and `exists_fun_of_mem_tangentConeAt`
for versions of two implications of this theorem that don't assume first countable topology.  -/
mem_tangentConeAt_iff_exists_seq : ∀ {R : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E]
  [FirstCountableTopology E] {s : Set E} {x y : E},
  y ∈ tangentConeAt R s x ↔
    ∃ c d,
      Filter.Tendsto d Filter.atTop (nhds 0) ∧
        (∀ᶠ (n : ℕ) in Filter.atTop, x + d n ∈ s) ∧ Filter.Tendsto (fun n => c n • d n) Filter.atTop (nhds y)
-- Mathlib.CategoryTheory.Iso
/-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`.  -/
CategoryTheory.Iso.homToEquiv : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → {Z : C} → (Z ⟶ X) ≃ (Z ⟶ Y)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : C ⥤ D`, this is the canonical bijection
`(X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj)`
for all `X : C` and `Y : F.PartialRightAdjointSource`.  -/
CategoryTheory.Functor.partialRightAdjointHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          {X : C} → {Y : F.PartialRightAdjointSource} → (X ⟶ F.partialRightAdjointObj Y) ≃ (F.obj X ⟶ Y.obj)
-- Init.Data.String.Basic
String.Slice.Pos.cast_eq_endPos : ∀ {s t : String.Slice} {p : s.Pos} {hst : s.copy = t.copy}, p.cast hst = t.endPos ↔ p = s.endPos
-- Init.Data.Iterators.Basic
Std.IterStep.mapIterator_id : ∀ {α : Type u} {β : Type w} {step : Std.IterStep α β}, Std.IterStep.mapIterator id step = step
-- Std.Data.ExtTreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.ExtTreeMap.union : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp → Std.ExtTreeMap α β cmp
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremsArray.eraseTheorem : Lean.Meta.SimpTheoremsArray → Lean.Meta.Origin → Lean.Meta.SimpTheoremsArray
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_const_lt_top_iff : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {p : ENNReal} {c : F}, p ≠ 0 → p ≠ ⊤ → (MeasureTheory.eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤)
-- Mathlib.Analysis.Convex.Basic
convex_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], Convex 𝕜 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.toRationalMap_representative : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y), f.representative.toRationalMap = f