mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_apply : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] (f : WithConv (E →L[R] F)) (x : E), (star f).ofConv x = star (f.ofConv (star x))
-- Init.Data.Dyadic.Basic
Dyadic.blt_eq_false_iff : ∀ {x y : Dyadic}, x.blt y = false ↔ y.ble x = true
-- Batteries.Data.Array.Scan
Array.scanl_ne_empty : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β}, Array.scanl f init as ≠ #[]
-- Lean.Parser.Term
Lean.Parser.Term.rightact.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.NeZero
two_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], 2 ≠ 0
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l : L₂ ⟶ L₁),
  CategoryTheory.Comma.mapRight R l =
    {
      obj := fun X =>
        { left := X.left, right := X.right, hom := CategoryTheory.CategoryStruct.comp X.hom (l.app X.right) },
      map := fun {Y X} f => CategoryTheory.CommaMorphism.mk' f.right f.left ⋯, map_id := ⋯, map_comp := ⋯ }
-- Lean.Meta.AppBuilder
/-- Given `proof` s.t. `inferType proof` is definitionally equal to `expectedProp`, returns
term `@id expectedProp proof`.  -/
Lean.Meta.mkExpectedPropHint : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.homCategory_id : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮)
  (𝒴 : CategoryTheory.BasedCategory 𝒮) (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  CategoryTheory.CategoryStruct.id F = CategoryTheory.BasedNatTrans.id F
-- Lean.Elab.Tactic.Conv.Pattern
_private.Lean.Elab.Tactic.Conv.Pattern.0.Lean.Elab.Tactic.Conv.matchPattern?.go? : Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_neg_period : ∀ (p x : ℝ), ‖↑x‖ = ‖↑x‖
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subNegMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → SubNegMonoid (f i)],
  Pi.subNegMonoid =
    { toAddMonoid := Pi.addMonoid, toNeg := Pi.instNeg, toSub := Pi.instSub, zsmul := fun z x i => z • x i,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.Data.Set.Enumerate
Set.enumerate.eq_1 : ∀ {α : Type u_1} (sel : Set α → Option α) (x : Set α), Set.enumerate sel x 0 = sel x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.coprod_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] {G : Type u_6} [inst_5 : AddCommGroup G]
  [inst_6 : Module R F] [inst_7 : Module S G] (f : E →ₛₗ.[σ] G) (g : F →ₛₗ.[σ] G) (x : ↥(f.coprod g).domain),
  ↑(f.coprod g) x = ↑f ⟨(↑x).1, ⋯⟩ + ↑g ⟨(↑x).2, ⋯⟩
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₁_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  {Z : HomologicalComplex C c} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) h) =
    h
-- Mathlib.Data.TypeVec
TypeVec.comp_assoc : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} {γ : TypeVec.{w} n} {δ : TypeVec.{x} n} (h : γ.Arrow δ)
  (g : β.Arrow γ) (f : α.Arrow β), TypeVec.comp (TypeVec.comp h g) f = TypeVec.comp h (TypeVec.comp g f)
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- Indexing of the complex characters of `ZMod n`. `AddChar.zmod n x` is the character sending `y`
to `e ^ (2 * π * i * x * y / n)`.  -/
AddChar.zmod : (n : ℕ) → [NeZero n] → ZMod n → AddChar (ZMod n) Circle
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An integral domain in which there is an irreducible element `p`
such that every nonzero element is associated to a power of `p` is a unique factorization domain.
See `IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization`.  -/
IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid : ∀ {R : Type u_1} [inst : CommRing R] [IsCancelMulZero R],
  IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization R → UniqueFactorizationMonoid R
-- Mathlib.Data.FunLike.Module
FunLike.isCentralScalar : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [inst : SMul M F]
  [inst_1 : SMul Mᵐᵒᵖ F] [inst_2 : SMul M β] [inst_3 : SMul Mᵐᵒᵖ β] [IsCentralScalar M β] [IsSMulApply M F α β]
  [IsSMulApply Mᵐᵒᵖ F α β], IsCentralScalar M F
-- Mathlib.Data.Finset.Filter
Finset.coe_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α), ↑(Finset.filter p s) = {x | x ∈ s ∧ p x}
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.tactic.fun_induction.unfolding : Lean.Option Bool
-- Aesop.BaseM
/-- Aesop's base monad. Contains no interesting data, only various caches and
stats.  -/
Aesop.BaseM : Type → Type
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.limitSemiring : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] →
            Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format a `RefinedDiscrTree.StackEntry`.  -/
Lean.Meta.RefinedDiscrTree.StackEntry.format : Lean.Meta.RefinedDiscrTree.StackEntry → Std.Format
-- Mathlib.Data.Set.MemPartition
memPartition_succ : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ),
  memPartition f (n + 1) = {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
-- Mathlib.Data.Set.Insert
Set.mem_singleton_iff : ∀ {α : Type u_1} {a b : α}, a ∈ {b} ↔ a = b
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNIndepSet.card_eq : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsNIndepSet n s → s.card = n
-- Mathlib.Data.Sym.Basic
/-- Remove every `a` from a given `Sym α n`.
Yields the number of copies `i` and a term of `Sym α (n - i)`.  -/
Sym.filterNe : {α : Type u_1} → {n : ℕ} → [DecidableEq α] → α → Sym α n → (i : Fin (n + 1)) × Sym α (n - ↑i)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.inv_add_inv_eq_one : ∀ {p q : NNReal}, p.HolderConjugate q → p⁻¹ + q⁻¹ = 1
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_sum_subst_truncTotal : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {k : ℕ},
  MvPowerSeries.HasSubst a →
    (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
      (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
        (MvPowerSeries.truncTotal k)
          (∑ i ∈ Finset.range k,
            MvPowerSeries.subst (fun i => ↑((MvPowerSeries.truncTotal k) (a i)))
              ((MvPowerSeries.homogeneousComponent i) f))
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- The bijection between `n`-simplices of `X.op` and of `X`
that are constant on the boundary.  -/
SSet.PtSimplex.opEquiv : {X : SSet} →
  {n : ℕ} → {x : X.obj (Opposite.op { len := 0 })} → X.op.PtSimplex n (SSet.opObjEquiv.symm x) ≃ X.PtSimplex n x
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.mk.congr_simp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (hom hom_1 : M.V ⟶ N.V) (e_hom : hom = hom_1)
  (comm : ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g)),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubgroup.toIntSubmodule_symm : ∀ {M : Type u_3} [inst : AddCommGroup M], ⇑AddSubgroup.toIntSubmodule.symm = Submodule.toAddSubgroup
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.IsCollisionNode.mk : ∀ {α : Type u_1} {β : Type u_2} (keys : Array α) (vals : Array β) (h : keys.size = vals.size),
  Lean.PersistentHashMap.IsCollisionNode (Lean.PersistentHashMap.Node.collision keys vals h)
-- Batteries.Recycling.RBTree.WF
/-- When `p` is false, the red-red case is impossible so the tree is balanced.  -/
RBTree.RBNode.RedRed.of_false : ∀ {p : Prop} {α : Type u_1} {t : RBTree.RBNode α} {n : ℕ}, ¬p → RBTree.RBNode.RedRed p t n → ∃ c, t.Balanced c n
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all
subsets of `s`, and over all subsets of `s` to which one adds `x`.  -/
Finset.sum_powerset_cons : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β),
  ∑ t ∈ (Finset.cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
-- Lean.Message
Lean.instToMessageDataArray : {α : Type} → [Lean.ToMessageData α] → Lean.ToMessageData (Array α)
-- Init.Data.UInt.Lemmas
USize.toUInt16_mod : ∀ (a b : USize), a < 65536 → b < 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeft_unit_iso_of_R_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Full] [R.Faithful],
  CategoryTheory.IsIso (R.whiskerLeft h.unit)
-- Mathlib.Algebra.Star.StarAlgHom
/-- The left injection into a product is a non-unital algebra homomorphism.  -/
NonUnitalStarAlgHom.inl : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : StarAddMonoid B] → A →⋆ₙₐ[R] A × B
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.iSup_pow : ∀ {ι : Sort u_1} [Nonempty ι] {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → ∀ (n : ℕ), (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.StdWall.wall.sizeOf_spec : sizeOf Std.Time.TimeZone.StdWall.wall = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_piMap : ∀ {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)] {ψ : ι → Type u_6}
  [inst_4 : (i : ι) → TopologicalSpace (ψ i)] [inst_5 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_6 : (i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →L[R] ψ i),
  ↑(ContinuousLinearMap.piMap f) = LinearMap.piMap fun i => ↑(f i)
-- Mathlib.Logic.Relation
Relation.instTransReflTransGen : {α : Type u_1} → {r : α → α → Prop} → Trans r (Relation.ReflTransGen r) (Relation.ReflTransGen r)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5StarOfSize.ofShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {inst_1 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w', v, u} C}
  [self : CategoryTheory.AB5StarOfSize.{w, w', v, u} C] (J : Type w') [inst_2 : CategoryTheory.Category.{w, w'} J]
  [inst_3 : CategoryTheory.IsCofiltered J], CategoryTheory.HasExactLimitsOfShape J C
-- Mathlib.Algebra.Order.Group.End
OrderHom.instIsMulApplyEqComp : ∀ {α : Type u_1} [inst : Preorder α], IsMulApplyEqComp (α →o α) α
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instHasZeroObject : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasZeroObject (ModuleCat R)
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.coeff_modOf_of_exists_add`. -/
AddMonoidAlgebra.modOf_apply_of_exists_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g g' : G),
  (∃ d, g' = g + d) → (x.modOf g).coeff g' = 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coeff_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ : MvPolynomial σ R) (n : σ →₀ ℕ),
  (MvPowerSeries.coeff n) ↑φ = MvPolynomial.coeff n φ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.coe_iInf : ∀ {V : Type u} {G : SimpleGraph V} [inst : Finite V] {ι : Sort u_1} (f : ι → G.Finsubgraph), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Constructs the list of keys of the map.  -/
RBTree.RBMap.keysList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → List α
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instAdd : {K : Type u} → [inst : CommRing K] → Add (RatFunc K)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.instContinuousEvalConst : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X},
  ContinuousEvalConst (↑(GenLoop N X x)) (N → ↑unitInterval) X
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_id : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], (PiTensorProduct.map fun i => LinearMap.id) = LinearMap.id
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.complexBasis_apply : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α] (ψ : AddChar α ℂ), (AddChar.complexBasis α) ψ = ⇑ψ
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_eq_one : ∀ {α : Type u_1} [inst : One α] {a : Lex α}, ofLex a = 1 ↔ a = 1
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalars₁₂_apply_apply : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {N : Type u_7} {Pₗ : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ] [inst_5 : Module R M]
  [inst_6 : Module S N] [inst_7 : Module R Pₗ] [inst_8 : Module S Pₗ] [inst_9 : SMulCommClass S R Pₗ] (R' : Type u_14)
  (S' : Type u_15) [inst_10 : Semiring R'] [inst_11 : Semiring S'] [inst_12 : Module R' M] [inst_13 : Module S' N]
  [inst_14 : Module R' Pₗ] [inst_15 : Module S' Pₗ] [inst_16 : SMulCommClass S' R' Pₗ] [inst_17 : SMul S' S]
  [inst_18 : IsScalarTower S' S N] [inst_19 : IsScalarTower S' S Pₗ] [inst_20 : SMul R' R]
  [inst_21 : IsScalarTower R' R M] [inst_22 : IsScalarTower R' R Pₗ] (B : M →ₗ[R] N →ₗ[S] Pₗ) (m : M) (x2 : N),
  ((LinearMap.restrictScalars₁₂ R' S' B) m) x2 = (B m) x2
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₃ = h
-- Mathlib.Topology.Algebra.AsymptoticCone
Filter.Tendsto.asymptoticNhds_vadd_const : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {α : Type u_4} {l : Filter α} {f : α → V}
  {v : V} (p : P),
  Filter.Tendsto f l (AffineSpace.asymptoticNhds k V v) →
    Filter.Tendsto (fun x => f x +ᵥ p) l (AffineSpace.asymptoticNhds k P v)
-- Mathlib.Tactic.WLOG
/-- The pair `(HFVarId, negHypFVarId)` of `FVarIds` for `reductionGoal`:

* `HFVarId`: `H`, the statement that in the original context `P` suffices to prove the goal.
* `negHypFVarId`: `h : ¬ P`, the assumption that `P` does not hold
 -/
Mathlib.Tactic.WLOGResult.reductionFVarIds : Mathlib.Tactic.WLOGResult → Lean.FVarId × Lean.FVarId
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Combinators.Monadic.FilterMap.0.Std.Iterators.Types.Map.instProductivenessRelation : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [inst_1 : Std.Iterator α m β] →
          {lift : ⦃α : Type w⦄ → m α → n α} →
            {f : β → Std.Iterators.PostconditionT n γ} →
              [Std.Iterators.Productive α m] →
                Std.Iterators.ProductivenessRelation (Std.Iterators.Types.Map α m n lift f) n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionParams : Lean.ToJson Lean.Lsp.CompletionParams
-- Mathlib.Analysis.Convex.Hull
convexHull_eq_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E} {x : E}, (convexHull 𝕜) s = {x} ↔ s = {x}
-- Init.Data.Char.Ordinal
Char.le_iff_ordinal_le : ∀ {c d : Char}, c ≤ d ↔ c.ordinal ≤ d.ordinal
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.refl_symm_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G) (a : E), (AddGroupExtension.Equiv.refl S).symm a = a
-- Init.Data.UInt.Lemmas
instCommutativeUInt16HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.map'_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] {f : α →* β}, StrictMono ⇑f → StrictMono ⇑(WithZero.map' f)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ext : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y},
  (∀ (x : X), e x = e' x) → e = e'
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_succ : ∀ {f : Ordinal.{u} → Ordinal.{u}},
  Order.IsNormal f → ∀ (o : Ordinal.{u}), Ordinal.veblenWith f (Order.succ o) = Ordinal.deriv (Ordinal.veblenWith f o)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_ite_mem_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] (s : Finset ι) (f : ι → M)
  [inst_2 : DecidablePred fun x => x ∈ s], (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `s : Cocone F` is a colimit cocone, so is `s` whiskered by an equivalence `e`.  -/
CategoryTheory.Limits.IsColimit.whiskerEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cocone F} →
                CategoryTheory.Limits.IsColimit s →
                  (e : K ≌ J) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cocone.whisker e.functor s)
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'_loop_eq_forIn'_range' : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (r : Std.Legacy.Range) (init : β)
  (f : (a : ℕ) → a ∈ r → β → m (ForInStep β)) (i : ℕ) (w₁ : (i - r.start) % r.step = 0) (w₂ : r.start ≤ i),
  Std.Legacy.Range.forIn'.loop✝ r f init i w₁ w₂ =
    forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init fun a h => f a ⋯
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- If `D` is a monoidal category and we have a function `C → D`, then we have a
monoidal functor from the free monoidal category over `C` to the category `D`.  -/
CategoryTheory.FreeMonoidalCategory.project : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [CategoryTheory.MonoidalCategory D] → (C → D) → CategoryTheory.Functor (CategoryTheory.FreeMonoidalCategory C) D
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.toTrivialization'.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} [inst_3 : Nonempty I] (h : IsEvenlyCovered f x I),
  h.toTrivialization' =
    (fun U x_1 =>
        (fun H hH =>
            { toFun := fun e => if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I),
              invFun := fun xi => ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, ⋯⟩, xi.2)), source := f ⁻¹' U,
              target := U ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
              continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯, baseSet := U,
              open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ })
          (Classical.choose ⋯) ⋯)
      (Classical.choose ⋯) ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'.go.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0)) (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p))
  (k : ℤ),
  p = Lean.Grind.CommRing.Poly.num k →
    (k = 0 → False) →
      (match p with
        | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
        | Lean.Grind.CommRing.Poly.num k => h_2 k
        | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) ≍
        h_2 k
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.symm_apply_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y) {x : X}
  {y : Y}, e.symm y = x ↔ y = e x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instSMulCommClassSubtypeMem : ∀ {S : Type u'} {T : Type u''} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M]
  [hS : SMulMemClass S R M] (s : S) [inst_2 : SMul T M] [inst_3 : SMulMemClass S T M] [SMulCommClass T R M],
  SMulCommClass T R ↥s
-- Mathlib.Order.Category.PartOrd
PartOrd.hom_comp : ∀ {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z),
  PartOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (PartOrd.Hom.hom g).comp (PartOrd.Hom.hom f)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_mono_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q Q' : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel Q Q' → Lean.Order.PartialOrder.rel (Lean.Order.himp P Q) (Lean.Order.himp P Q')
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_addMonoidHom_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.pow_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ g i) → AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn f (g ^ n) s