mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt_invol : ∀ {N i : ℕ}, (Polynomial.revAt N) ((Polynomial.revAt N) i) = i
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_zero : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M], AddMonoidHom.ker 0 = ⊤
-- Mathlib.Analysis.Normed.Group.Basic
enorm_sum_le : ∀ {ι : Type u_3} {ε : Type u_9} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] (s : Finset ι)
  (f : ι → ε), ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postMap_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ⟶ G) (Y : CategoryTheory.Over X),
  (CategoryTheory.Over.postMap e).app Y = CategoryTheory.Over.homMk (e.app Y.left) ⋯
-- Mathlib.Algebra.Group.Action.Hom
/-- If an action is transitive, then composing this action with a surjective homomorphism gives
again a transitive action.  -/
MulAction.isPretransitive_compHom : ∀ {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : Monoid E] [inst_1 : Monoid F] [inst_2 : MulAction F G]
  [MulAction.IsPretransitive F G] {f : E →* F}, Function.Surjective ⇑f → MulAction.IsPretransitive E G
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.comap` as a `RingHom`.  -/
LocallyConstant.comapRingHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} → [inst_2 : Semiring Z] → C(X, Y) → LocallyConstant Y Z →+* LocallyConstant X Z
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- To give an object in the under category, it suffices to give an arrow with domain `X`.  -/
CategoryTheory.Under.mk : {T : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} T] → {X Y : T} → (X ⟶ Y) → CategoryTheory.Under X
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPOUFun_eq_mul_prod : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X)
  (t : Finset ι),
  (∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t) →
    f.toPOUFun i x = (f i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (f j) x)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_pullback_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {X : C}
  (R : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f R).arrows ↔
    CategoryTheory.Presieve.IsSheafFor P R.arrows
-- Init.Data.List.Zip
List.zipWith_map_right : ∀ {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : β → β'}
  {g : α → β' → γ}, List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun a b => g a (f b)) l₁ l₂
-- Init.MetaTypes
Lean.Meta.LiftLetsConfig.mk.sizeOf_spec : ∀ (toExtractLetsConfig : Lean.Meta.ExtractLetsConfig),
  sizeOf { toExtractLetsConfig := toExtractLetsConfig } = 1 + sizeOf toExtractLetsConfig
-- Mathlib.Tactic.Translate.GuessName
Mathlib.Tactic.GuessName.GuessNameData.mk.inj : ∀ {nameDict : Std.HashMap String (List String)} {abbreviationDict : Std.HashMap String String}
  {nameDict_1 : Std.HashMap String (List String)} {abbreviationDict_1 : Std.HashMap String String},
  { nameDict := nameDict, abbreviationDict := abbreviationDict } =
      { nameDict := nameDict_1, abbreviationDict := abbreviationDict_1 } →
    nameDict = nameDict_1 ∧ abbreviationDict = abbreviationDict_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forIn_eq_forIn : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.forIn f init t = forIn t init fun a b => f a.fst a.snd b
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
/-- Given a parametrized adjunction `F ⊣₂ G` between bifunctors, and structures
`sq₁₂ : F.PushoutObjObj f₁ f₂` and `sq₁₃ : G.PullbackObjObj f₁ f₃`, there are
as many commutative squares with left map `sq₁₂.ι` and right map `f₃`
as commutative squares with left map `f₂` and right map `sq₁₃.π`.  -/
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (F ⊣₂ G) →
                  {X₁ Y₁ : C₁} →
                    {f₁ : X₁ ⟶ Y₁} →
                      {X₂ Y₂ : C₂} →
                        {f₂ : X₂ ⟶ Y₂} →
                          {X₃ Y₃ : C₃} →
                            {f₃ : X₃ ⟶ Y₃} →
                              (sq₁₂ : F.PushoutObjObj f₁ f₂) →
                                (sq₁₃ : G.PullbackObjObj f₁ f₃) →
                                  (CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃) ≃
                                    (CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- A version of `Commute.cfcₙ` or `IsSelfAdjoint.commute_cfcₙ` which does not require any
interaction with `star` when the base ring is `ℝ`.  -/
Commute.cfcₙ_real : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : IsScalarTower ℝ A A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → ∀ (f : ℝ → ℝ), Commute (cfcₙ f a) b
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.mul_add_mul_ne_mul : ∀ {m n a b : ℕ}, m.Coprime n → a ≠ 0 → b ≠ 0 → a * m + b * n ≠ m * n
-- Mathlib.CategoryTheory.Limits.Over
/-- If `c` is a limit cone, then so is the cone `c.toUnder` with cone point `𝟙 c.pt`.  -/
CategoryTheory.Under.isLimitToUnder : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit c.toUnder
-- Mathlib.Order.Category.Lat
Lat.inv_hom_apply : ∀ {X Y : Lat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
TopologicalSpace.PositiveCompacts.piIcc01.eq_1 : ∀ (ι : Type u_1) [inst : Finite ι],
  TopologicalSpace.PositiveCompacts.piIcc01 ι =
    { carrier := Set.univ.pi fun x => Set.Icc 0 1, isCompact' := ⋯, interior_nonempty' := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Construct a pseudo-metric space structure whose underlying topological space structure
(definitionally) agrees which a pre-existing topology which is compatible with a given distance
function.  -/
PseudoMetricSpace.ofDistTopology : {α : Type u} →
  [inst : TopologicalSpace α] →
    (dist : α → α → ℝ) →
      (∀ (x : α), dist x x = 0) →
        (∀ (x y : α), dist x y = dist y x) →
          (∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
            (∀ (s : Set α), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : α), dist x y < ε → y ∈ s) → PseudoMetricSpace α
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instSingletonSigmaOfBEqOfHashable : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Singleton ((a : α) × β a) (Std.DHashMap.Raw α β)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.hasSum_eval : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {α : Type u_5}
  {p : α → ContinuousMultilinearMap 𝕜 E F} {q : ContinuousMultilinearMap 𝕜 E F},
  HasSum p q → ∀ (m : (i : ι) → E i), HasSum (fun a => (p a) m) (q m)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cochain.leftShiftAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n a n' : ℤ) →
          n + a = n' →
            CochainComplex.HomComplex.Cochain K L n ≃+
              CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- See Note [custom simps projection].  -/
ContinuousAffineEquiv.Simps.symm_apply : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] → [inst_8 : TopologicalSpace P₂] → (P₁ ≃ᴬ[k] P₂) → P₂ → P₁
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x)
  {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.lift F M hM).map f =
    match X, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      F.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => M x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.eq_1 : ∀ {s : String.Slice} (p : s.Pos), p.nextn 0 = p
-- Mathlib.Order.Basic
ne_of_not_ge : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, ¬b ≤ a → a ≠ b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFiniteHom : ∀ (X Y : FintypeCat), Finite (X ⟶ Y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β k → β k} {fallback : α},
      Std.Internal.List.minKeyD (Std.Internal.List.modifyKey k f l) fallback = Std.Internal.List.minKeyD l fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCocycle_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cocycle M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (hαβ : CochainComplex.HomComplex.δ m n β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  ↑(CochainComplex.mappingCocone.liftCocycle φ α β h hαβ) = CochainComplex.mappingCocone.liftCochain φ (↑α) β h
-- Init.Data.Option.Attach
Option.any_attach : ∀ {α : Type u_1} {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool},
  (∀ (x : α) (h : o = some x), q ⟨x, h⟩ = p x) → Option.any q o.attach = Option.any p o
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.utf8Decode?go_eq_utf8Decode?go_extract : ∀ {i : ℕ} {b : ByteArray} {hi : i ≤ b.size} {acc : Array Char},
  ByteArray.utf8Decode?.go b i acc hi =
    Option.map (fun x => acc ++ x) (ByteArray.utf8Decode?.go (b.extract i b.size) 0 #[] ⋯)
-- Mathlib.SetTheory.Lists
/-- Converts a ZFA list to a `List` of ZFA lists. Atoms are sent to `[]`.  -/
Lists.toList : {α : Type u_1} → Lists α → List (Lists α)
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_iterate_powMonoidHom' : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n m : ℕ),
  m ≤ n → (Perfection.coeffMonoidHom M p n) ((⇑(powMonoidHom p))^[m] f) = (Perfection.coeffMonoidHom M p (n - m)) f
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.min_dist_le_dist_pi : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → PseudoMetricSpace (F i)]
  (x y : (i : ι) → F i) (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i)) ≤ dist x y
-- Mathlib.FieldTheory.Galois.Basic
/-- The Galois correspondence from intermediate fields to subgroups.  -/
IsGalois.intermediateFieldEquivSubgroup : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [FiniteDimensional F E] → [IsGalois F E] → IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈ
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Category.{max v u_1, max (max (u_1 + 1) v) u} (AlgebraicGeometry.SheafedSpace C)
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.toProd_mul : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s t : NonemptyInterval α), (s * t).toProd = s.toProd * t.toProd
-- Lean.Data.Lsp.Diagnostics
/-- Tags representing additional metadata about the diagnostic.  -/
Lean.Lsp.DiagnosticTag : Type
-- Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Real.tendstoLocallyUniformlyOn_rpow_sub_one_log : TendstoLocallyUniformlyOn (fun p x => p⁻¹ * (x ^ p - 1)) Real.log (nhdsWithin 0 (Set.Ioi 0)) (Set.Ioi 0)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.symm_inv : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G],
  (Homeomorph.inv G).symm = Homeomorph.inv G
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Functor.isoCopyObj_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (X : C),
  (F.isoCopyObj obj e).inv.app X = (e X).inv
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 : ℕ →
  Lean.Meta.Grind.Arith.CommRing.EqCnstr →
    Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instNatCastQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → NatCast (Lean.Grind.Ring.OfSemiring.Q α)
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizeUsingInstances : List Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The associator isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.associator_inv_natural_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z_1 : C}
  (h_1 : (X ⊞ Y) ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
        h_1)
-- Aesop.Frontend.Saturate
Aesop.Frontend.elabForwardRule : Lean.Term → Aesop.ElabM Aesop.LocalRuleSetMember
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_ric : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice xs *...=hi) = List.take (hi + 1) (Std.Slice.toList xs)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_domain_iff_of_eq_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F},
  f.graph = g.graph → ∀ {x : E}, x ∈ f.domain ↔ x ∈ g.domain
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_mul : ∀ {w : ℕ} (x y : BitVec w) (i : ℕ), (x * y).getMsbD i = (x.mulRec y w).getMsbD i
-- Init.Data.BitVec.Lemmas
BitVec.toInt_intMax : ∀ {w : ℕ}, (BitVec.intMax w).toInt = 2 ^ (w - 1) - 1
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.liftp_iff' : ∀ {P : PFunctor.{uA, uB}} {α : Type u} (p : α → Prop) (a : P.A) (f : P.B a → α),
  Functor.Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)
-- Mathlib.Order.PiLex
Pi.instBoundedOrderColexForallOfWellFoundedGT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedGT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → BoundedOrder (β a)] → BoundedOrder (Colex ((a : ι) → β a))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.self_le_sinh_iff : ∀ {x : ℝ}, x ≤ Real.sinh x ↔ 0 ≤ x
-- Init.Data.Option.Lemmas
Option.min_pfilter_left : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {o : Option α} {p : (a : α) → o = some a → Bool},
  o.pfilter p ⊓ o = o.pfilter p
-- Lean.Server.Requests
Lean.Server.RequestError.mk.inj : ∀ {code : Lean.JsonRpc.ErrorCode} {message : String} {code_1 : Lean.JsonRpc.ErrorCode} {message_1 : String},
  { code := code, message := message } = { code := code_1, message := message_1 } → code = code_1 ∧ message = message_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The (left) homology class `A ⟶ H` attached to a cycle `k : A ⟶ S.X₂`  -/
CategoryTheory.ShortComplex.LeftHomologyData.liftH : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.LeftHomologyData) → {A : C} → (k : A ⟶ S.X₂) → CategoryTheory.CategoryStruct.comp k S.g = 0 → (A ⟶ h.H)
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (mvarId : Lean.MVarId) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.mvar mvarId with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_2 mvarId
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
affineSpan_insert_zero : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] (s : Set V),
  ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k s)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Applying a continuous linear map commutes with taking an (infinite) sum.  -/
ContinuousLinearEquiv.hasSum : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {σ' : R₂ →+* R}
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {L : SummationFilter ι} {f : ι → M} (e : M ≃SL[σ] M₂)
  {y : M₂}, HasSum (fun b => e (f b)) y L ↔ HasSum f (e.symm y) L
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_intMin : Int32.ofBitVec (BitVec.intMin 32) = Int32.minValue
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.IsImmersion f
-- Mathlib.Algebra.Ring.Action.Basic
/-- Multiplying `1` by a scalar gives `1`  -/
MulSemiringAction.smul_one : ∀ {M : Type u} {R : Type v} {inst : Monoid M} {inst_1 : Semiring R} [self : MulSemiringAction M R] (g : M), g • 1 = 1
-- Init.Control.Lawful.Instances
StateT.run_restoreM : ∀ {m : Type u_1 → Type u_2} {σ α : Type u_1} [inst : Monad m] [LawfulMonad m] (x : stM m (StateT σ m) α) (s : σ),
  (restoreM x).run s = pure x
-- Mathlib.Data.Set.Restrict
Set.restrictPreimage_bijective : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Bijective f → Function.Bijective (t.restrictPreimage f)
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instCountableHomObjAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α]
  {i j : CategoryTheory.CountableCategory.ObjAsType α}, Countable (i ⟶ j)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty) →
          ((l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
              (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b))) →
            (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit) → motive x