mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ.eq_2 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (hd : α)
  (tl : List α),
  Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m (hd :: tl) =
    Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ (m.insertIfNew hd ()) tl
-- Mathlib.CategoryTheory.Types.Basic
/-- The underlying function  -/
TypeCat.Hom.hom' : {X Y : Type u} → TypeCat.Hom X Y → TypeCat.Fun X Y
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.checkSystem : Lean.Meta.SynthInstance.SynthM Unit
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM.Context.mk.injEq : ∀ (unify zetaDelta : Bool) (lctxInitialNextIndex : ℕ) (mvarsNew mvarsToCheckType : Array Lean.MVarId)
  (unify_1 zetaDelta_1 : Bool) (lctxInitialNextIndex_1 : ℕ) (mvarsNew_1 mvarsToCheckType_1 : Array Lean.MVarId),
  ({ unify := unify, zetaDelta := zetaDelta, lctxInitialNextIndex := lctxInitialNextIndex, mvarsNew := mvarsNew,
        mvarsToCheckType := mvarsToCheckType } =
      { unify := unify_1, zetaDelta := zetaDelta_1, lctxInitialNextIndex := lctxInitialNextIndex_1,
        mvarsNew := mvarsNew_1, mvarsToCheckType := mvarsToCheckType_1 }) =
    (unify = unify_1 ∧
      zetaDelta = zetaDelta_1 ∧
        lctxInitialNextIndex = lctxInitialNextIndex_1 ∧ mvarsNew = mvarsNew_1 ∧ mvarsToCheckType = mvarsToCheckType_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_filterMap_le_size : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → Option (γ a)},
  m.WF → (Std.DHashMap.Raw.filterMap f m).size ≤ m.size
-- Init.Data.Int.Gcd
Int.natAbs_dvd_lcm_right : ∀ (a b : ℤ), b.natAbs ∣ a.lcm b
-- Batteries.Data.MLList.Basic
/-- Performs a monadic case distinction on a `MLList` when the motive is a `MLList` as well.  -/
MLList.casesM : {m : Type u_1 → Type u_1} →
  {α β : Type u_1} → [Monad m] → MLList m α → (Unit → m (MLList m β)) → (α → MLList m α → m (MLList m β)) → MLList m β
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x * x'` to `y * y'`.  -/
SemiconjBy.mul_right : ∀ {S : Type u_1} [inst : Semigroup S] {a x y x' y' : S},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.rightUnitor_hom_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).hom.app j =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj j)).hom
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteLemma.mk.injEq : ∀ (name : Lean.Name) (symm : Bool) (name_1 : Lean.Name) (symm_1 : Bool),
  ({ name := name, symm := symm } = { name := name_1, symm := symm_1 }) = (name = name_1 ∧ symm = symm_1)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.not_matchesAt_of_get : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  ¬p (pos.get h) → ¬String.Slice.Pattern.Model.MatchesAt p pos
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the sequence of partial denominators `bᵢ` of `g`.  -/
GenContFract.partDens : {α : Type u_1} → GenContFract α → Stream'.Seq α
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.instIsIrreducibleFlip : ∀ {ι : 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) [P.IsIrreducible],
  P.flip.IsIrreducible
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.exists_length_eq_zero_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, (∃ p, p.length = 0) ↔ u = v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The range of a surjective semigroup hom is the whole of the codomain.  -/
MulHom.srange_eq_top_of_surjective : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] (f : M →ₙ* N), Function.Surjective ⇑f → f.srange = ⊤
-- Mathlib.RingTheory.Length
Module.length_eq_height : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = Order.height ⊤
-- Std.Data.Iterators.Producers.Array
/-- Returns a finite iterator for the given array starting at the given index.
The iterator yields the elements of the array in order and then terminates.

The monadic version of this iterator is `Array.iterFromIdxM`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Array.iterFromIdx : {α : Type w} → Array α → ℕ → Std.Iter α
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ),
  (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).s =
    -(CochainComplex.mappingCone.inl φ).v (n + 1) n ⋯
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
IsUltraUniformity.iInf : ∀ {X : Type u_1} {ι : Type u_3} {U : ι → UniformSpace X}, (∀ (i : ι), IsUltraUniformity X) → IsUltraUniformity X
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.lift_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S' : CategoryTheory.SubmonoidFunctor M') (hp : CategoryTheory.SubmonoidFunctor.image p ⊤ ≤ S'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SubmonoidFunctor.lift p S' hp) S'.ι = p
-- Mathlib.Algebra.GCDMonoid.Basic
Prime.not_dvd_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b p : α},
  Prime p → ¬p ∣ a → ¬p ∣ b → ¬p ∣ lcm a b
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.comp_preservesFiniteCoproducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteCoproducts F]
  [CategoryTheory.Limits.PreservesFiniteCoproducts G], CategoryTheory.Limits.PreservesFiniteCoproducts (F.comp G)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) {X_1 Y : F.DescentDataAsCoalgebra fun x => f} (φ : X_1 ⟶ Y),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor.map φ).f = φ.hom default
-- Init.Data.UInt.Lemmas
UInt64.toFin_sub : ∀ (a b : UInt64), (a - b).toFin = a.toFin - b.toFin
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ici a).OrdConnected
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.fst f g)) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_eq_getValueCastD : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β},
  Std.Internal.List.getValueD a l fallback = Std.Internal.List.getValueCastD a l fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zero_ne_top : ∀ {α : Type u} [inst : Zero α], 0 ≠ ⊤
-- Mathlib.MeasureTheory.Integral.CircleTransform
/-- A useful bound for circle integrals (with complex codomain)  -/
Complex.circleTransformBoundingFunction : ℝ → ℂ → ℂ × ℝ → ℂ
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.inter : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsUpperSet s → IsUpperSet t → IsUpperSet (s ∩ t)
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.remainder.eq_1 : ∀ (p n : ℕ),
  WittVector.remainder p n =
    (∑ x ∈ Finset.range (n + 1),
        (MvPolynomial.rename (Prod.mk 0)) ((MvPolynomial.monomial fun₀ | x => p ^ (n + 1 - x)) (↑p ^ x))) *
      ∑ x ∈ Finset.range (n + 1),
        (MvPolynomial.rename (Prod.mk 1)) ((MvPolynomial.monomial fun₀ | x => p ^ (n + 1 - x)) (↑p ^ x))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rio_eq_some_iff : ∀ {k n i : ℕ}, (*...n).toArray[i]? = some k ↔ i < n ∧ i = k
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁IsoOfIsTrivial_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial] (x : G →₀ ↑A),
  ↑((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) x) = x
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'Aux_single : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁) (i j : n), (M.toBilin'Aux (Pi.single i 1)) (Pi.single j 1) = M i j
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sub_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z T : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        MeasureTheory.MemLp T 2 μ →
          ProbabilityTheory.covariance (X - Y) (Z - T) μ =
            ProbabilityTheory.covariance X Z μ - ProbabilityTheory.covariance X T μ -
                ProbabilityTheory.covariance Y Z μ +
              ProbabilityTheory.covariance Y T μ
-- Mathlib.Topology.Subpath
/-- Concatenating two paths `F 0` and `F 1` is homotopic to `Path.trans (F 0) (F 1)`.  -/
Path.Homotopic.concat_two : ∀ {X : Type u_1} [inst : TopologicalSpace X] (p : Fin 3 → X) (F : (k : Fin 2) → Path (p k.castSucc) (p k.succ)),
  (Path.concat p F).Homotopic ((F 0).trans (F 1))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- An element `a : α` is `MulLECancellable` if `x ↦ a * x` is order-reflecting.
We will make a separate version of many lemmas that require `[MulLeftReflectLE α]` with
`MulLECancellable` assumptions instead. These lemmas can then be instantiated to specific types,
like `ENNReal`, where we can replace the assumption `AddLECancellable x` by `x ≠ ∞`.
 -/
MulLECancellable : {α : Type u_1} → [Mul α] → [LE α] → α → Prop
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.ofList_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {hd : α} {tl : List α},
  Std.HashSet.Raw.ofList (hd :: tl) = (∅.insert hd).insertMany tl
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializedParams.noConfusionType : Sort v✝ → Lean.Lsp.InitializedParams → Lean.Lsp.InitializedParams → Sort v✝
-- Mathlib.Order.WithBot
WithTop.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b : α), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Init.Data.Nat.Gcd
Nat.gcd_sub_right_left_of_dvd : ∀ {n k : ℕ} (m : ℕ), k ≤ n → m ∣ k → (n - k).gcd m = n.gcd m
-- Lean.Declaration
/-- A reduction for each Constructor  -/
Lean.RecursorVal.rules : Lean.RecursorVal → List Lean.RecursorRule
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalClosed_closed_adj_unit : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X : (i : I) → C i), CategoryTheory.Closed.adj.unit = CategoryTheory.Pi.closedUnit X
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.support_ceilDiv_subset : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] {f : ι →₀ β}
  {a : α}, (f ⌈/⌉ a).support ⊆ f.support
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
/-- A `FinMeasAdditive` set function whose norm on every set is less than the measure of the
set (up to a multiplicative constant).  -/
MeasureTheory.DominatedFinMeasAdditive : {α : Type u_1} →
  {β : Type u_7} →
    [SeminormedAddCommGroup β] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → β) → ℝ → Prop
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.CoGrothendieck),
  (CategoryTheory.CategoryStruct.id X).fiber = (F.mapId { as := Opposite.op X.base }).inv.toNatTrans.app X.fiber
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalTermBehaviorIfUnchanged : Lean.Elab.ConfigEval.EvalTerm Mathlib.Tactic.BehaviorIfUnchanged
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w n : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc =
    if curr < n - 1 then
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig
          { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
      let aig_1 := res.aig;
      have acc_1 := res.vec;
      have this := ⋯;
      have distance := distance.cast this;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig_1 distance (curr + 1) acc_1
    else { aig := aig, vec := acc }
-- Init.Grind.Attr
/-- The `intro` modifier instructs `grind` to use the constructors (introduction rules)
of an inductive predicate as E-matching theorems.Example:
```
inductive Even : Nat → Prop where
| zero : Even 0
| add2 : Even x → Even (x + 2)

attribute [grind intro] Even
example (h : Even x) : Even (x + 6) := by grind
example : Even 0 := by grind
```
Here `attribute [grind intro] Even` acts like a macro that expands to
`attribute [grind] Even.zero` and `attribute [grind] Even.add2`.
This is especially convenient for inductive predicates with many constructors.
 -/
Lean.Parser.Attr.grindIntro : Lean.ParserDescr
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Integer powers of meromorphic functions in normal form are in normal form.
 -/
MeromorphicNFAt.zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℤ} {x : 𝕜},
  MeromorphicNFAt f x → MeromorphicNFAt (f ^ n) x
-- Mathlib.Order.Bounds.Image
/-- See also `Monotone.map_bddBelow`.  -/
BddBelow.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_zero : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R (insert 0 s) = Algebra.adjoin R s
-- Std.Do.WP.Sound
Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure],
  Std.Do.WPSound (OptionT m) (Std.Do.PostShape.except PUnit.{u_1 + 1} Std.Do.PostShape.pure)
-- Mathlib.Data.Num.Basic
Num.zero : Num
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_eq_pure : ∀ {α : Type u_1} [inst : Preorder α] {s : NonemptyInterval α} {a : α},
  ↑s = Interval.pure a ↔ s = NonemptyInterval.pure a
-- Mathlib.Algebra.Group.Defs
NSMul.toSMul.eq_1 : ∀ {M : Type u_2} [inst : NSMul M], NSMul.toSMul = { smul := fun n x => NSMul.nsmul n x }
-- Init.Data.Array.Attach
Array.getElem_unattach : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} (i : ℕ) (h : i < xs.unattach.size), xs.unattach[i] = ↑xs[i]
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_nsmulRec : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : AddMonoid β]
  [inst_3 : BoundedAdd β] [inst_4 : ContinuousAdd β] (f : BoundedContinuousFunction α β) (n : ℕ),
  ⇑(nsmulRec n f) = n • ⇑f
-- Mathlib.GroupTheory.Coxeter.Basic
/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the right
by a simple reflection, then it holds for all elements of `W`.  -/
CoxeterSystem.simple_induction_right : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {p : W → Prop} (w : W),
  p 1 → (∀ (w : W) (i : B), p w → p (w * cs.simple i)) → p w
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateUset! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Lean.FVarId → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_comp_add_left : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (a : E),
  HasFDerivWithinAt (fun x => f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOver.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C),
  CategoryTheory.toOver X =
    { obj := fun A => CategoryTheory.Over.mk (CategoryTheory.SemiCartesianMonoidalCategory.snd A X),
      map := fun {X_1 Y} f => CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) ⋯,
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
val_cfcUnits : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [inst_10 : ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0)
  (hf : autoParam (ContinuousOn f (spectrum R a)) cfcUnits._auto_1) (ha : autoParam (p a) cfcUnits._auto_3),
  ↑(cfcUnits f a hf' hf ha) = cfc f a
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_self_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : CommRing L] (i : K →+* L) (p : ℕ) [inst_2 : ExpChar K p]
  [inst_3 : ExpChar L p] [inst_4 : PerfectRing L p] [inst_5 : IsPerfectClosure i p] (x : L),
  (IsPerfectClosure.equiv i i p) x = x
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.upperBound?.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Option α → Sort u_2) (ub : Option α)
  (h_1 : (ub : Option α) → motive RBTree.RBNode.nil ub)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) → (b : RBTree.RBNode α) → (ub : Option α) → motive (RBTree.RBNode.node c a y b) ub),
  (match RBTree.RBNode.nil, ub with
    | RBTree.RBNode.nil, ub => h_1 ub
    | RBTree.RBNode.node c a y b, ub => h_2 c a y b ub) =
    h_1 ub
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLT_lt_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos}, s.posLT p h < q ↔ p ≤ q.offset
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_max : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a b : α),
  (a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.toMvFunctor : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [self : MvQPF F] → MvFunctor F
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsBasis'.inter_coloops_subset : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → X ∩ M.coloops ⊆ I
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instSingletonProd : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Singleton (α × β) (Std.TreeMap.Raw α β cmp)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_eq_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, k ∈ m → m.getD k fallback = k
-- Std.Internal.UV.Timer
/-- This function has different behavior depending on the state and configuration of the `Timer`:
- If it is initial or finished this is a no-op.
- If it is running and `repeating` is `false` this will delay the resolution of the timer until
  `timeout` milliseconds after the call of this function.
- Delay the resolution of the next tick of the timer until `timeout` milliseconds after the
  call of this function, then continue normal ticking behavior from there.
 -/
Std.Internal.UV.Timer.reset : Std.Internal.UV.Timer → IO Unit
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.aleph0_add_ofENat : ∀ (m : ℕ∞), Cardinal.aleph0 + ↑m = Cardinal.aleph0
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExists.distrib_add : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f : M → E} {g g' : M → E'} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.ConvolutionExists L f g →
    DiscreteConvolution.ConvolutionExists L f g' →
      DiscreteConvolution.convolution L f (g + g') =
        DiscreteConvolution.convolution L f g + DiscreteConvolution.convolution L f g'
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.congr_fun : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] {f g : R ≃+* S},
  f = g → ∀ (x : R), f x = g x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_lt_sq₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} [MulPosMono M₀],
  0 ≤ a → 0 ≤ b → (a ^ 2 < b ^ 2 ↔ a < b)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_δ : ∀ {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i) (SimplexCategoryGenRel.δ j.succ) =
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ j) (SimplexCategoryGenRel.δ i.castSucc)
-- Mathlib.Logic.Relation
Relation.SymmGen.of_ge : ∀ {α : Type u_7} [inst : LE α] {a b : α}, b ≤ a → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b