mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_iff : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r ↔ 0 ≤ ArchimedeanClass.mk x ∧ ArchimedeanClass.stdPart x = r
-- Lean.Server.AsyncList
Lean.AsyncList.instCoeList : {α : Type u_1} → {ε : Type u_2} → Coe (List α) (Lean.AsyncList ε α)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_apply_eq : ∀ {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₂]
  (e : P₁ ≃ᴬ[k] P₂) {x : P₂} {y : P₁}, e.symm x = y ↔ x = e y
-- Mathlib.Algebra.Group.Invertible.Defs
/-- The inverse of an `Invertible` element  -/
«term⅟_» : Lean.ParserDescr
-- Lean.Elab.InfoTree.Types
/-- The InfoTree is a structure that is generated during elaboration and used
by the language server to look up information about objects at particular points
in the Lean document. For example, tactic information and expected type information in
the infoview and information about completions.

The infotree consists of nodes which may have child nodes. Each node
has an `Info` object that contains details about what kind of information
is present. Each `Info` object also contains a `Syntax` instance, this is used to
map positions in the Lean document to particular info objects.

An example of a function that extracts information from an infotree for a given
position is `InfoTree.goalsAt?` which finds `TacticInfo`.

Information concerning expressions requires that a context also be saved.
`context` nodes store a local context that is used to process expressions
in nodes below.

Because the info tree is generated during elaboration, some parts of the infotree
for a particular piece of syntax may not be ready yet. Hence InfoTree supports metavariable-like
`hole`s which are filled in later in the same way that unassigned metavariables are.
 -/
Lean.Elab.InfoTree : Type
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_pUnit : Ordinal.type emptyRelation = 1
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrRight_trans : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} {ψ : ι → Type u_2} {χ : ι → Type u_3}
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_4 : (i : ι) → Module R (ψ i)] [inst_5 : (i : ι) → AddCommMonoid (χ i)] [inst_6 : (i : ι) → Module R (χ i)]
  (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → ψ i ≃ₗ[R] χ i),
  LinearEquiv.piCongrRight e ≪≫ₗ LinearEquiv.piCongrRight f = LinearEquiv.piCongrRight fun i => e i ≪≫ₗ f i
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous* on all of `X` if it is equicontinuous at each point of `X`.  -/
Equicontinuous : {ι : Type u_1} →
  {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → (ι → X → α) → Prop
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.Small.{w, v, u} P.unop
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom_one : ∀ (V : Type u_1) [Countable V], SimpleGraph.binomialRandom V 1 = MeasureTheory.Measure.dirac ⊤
-- Mathlib.Algebra.DirectSum.Ring
/-- A direct sum of copies of a `CommRing` inherits the commutative multiplication structure.  -/
CommRing.directSumGCommRing : (ι : Type u_1) → {R : Type u_2} → [inst : AddCommMonoid ι] → [inst_1 : CommRing R] → DirectSum.GCommRing fun x => R
-- Mathlib.Data.Set.Function
Set.graphOn_univ_inj : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β}, Set.graphOn f Set.univ = Set.graphOn g Set.univ ↔ f = g
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.min_eq : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfOrdArgs α),
  let this := self.ord;
  let this_1 := self.le;
  let this_2 := self.min;
  have this_3 := ⋯;
  ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r')
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr).hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_of_eventually_ge : ∀ {u v : ℕ → ENNReal} {b : ENNReal},
  b ≠ 0 → (∀ᶠ (n : ℕ) in Filter.atTop, b * u n ≤ v n) → ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf v
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.isMulCommutative_iSup : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} [Nonempty ι] {S : ι → Submonoid M}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n), ↑(z₁ - z₂) = ↑z₁ - ↑z₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.dropLast.length = p.length - 1
-- Mathlib.Algebra.Homology.BifunctorHomotopy
toPrev.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (j : ι), toPrev j = AddMonoidHom.mk' (fun f => f j (c.prev j)) ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Init.Data.Nat.Basic
Nat.instCommutativeHMul : Std.Commutative fun x1 x2 => x1 * x2
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `eraseManyEntries` which can be used in absence of balance information but still
assumes the preconditions of `eraseManyEntries`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.eraseManyEntries! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} → [ForIn Id ρ ((a : α) × β a)] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.IteratedSlowErasureFrom
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.coe_injective : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X],
  Function.Injective DiscreteTiling.Protoset.tiles
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.HasFrame.mk : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {P' : outParam (Std.Do.SPred σs)} {φ : outParam Prop},
  (P ⊣⊢ₛ P' ∧ ⌜φ⌝) → Std.Do.SPred.Tactic.HasFrame P P' φ
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The **Cauchy-Davenport Theorem** for torsion-free groups. The size of `s * t` is lower-bounded
by `|s| + |t| - 1`.  -/
cauchy_davenport_of_isMulTorsionFree : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] [IsMulTorsionFree G] {s t : Finset G},
  s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s * t).card
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition of being a pointwise right Kan extension at an object `Y` is
unchanged by replacing `Y` by an isomorphic object `Y'`.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso' : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                (E : L.RightExtension F) →
                  {Y Y' : D} → (Y ≅ Y') → E.IsPointwiseRightKanExtensionAt Y ≃ E.IsPointwiseRightKanExtensionAt Y'
-- Std.Data.HashMap.Raw
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.HashMap.Raw.beq : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [BEq β] → Std.HashMap.Raw α β → Std.HashMap.Raw α β → Bool
-- Init.Core
/-- `HEq.ndrec` variant  -/
HEq.ndrecOn : {α : Sort u2} → {a : α} → {motive : {β : Sort u2} → β → Sort u1} → {β : Sort u2} → {b : β} → a ≍ b → motive a → motive b
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.comp_proof : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q R : CategoryTheory.Idempotents.Karoubi C}
  (g : Q.Hom R) (f : P.Hom Q),
  CategoryTheory.CategoryStruct.comp P.p
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f.f g.f) R.p) =
    CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.Data.Finset.Insert
Finset.Nontrivial.ne_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, s.Nontrivial → s ≠ {a}
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoRightCat_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d),
  (CategoryTheory.Bicategory.associatorNatIsoRightCat f g d).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator f g X).inv
-- Mathlib.Algebra.Star.Conjneg
conjneg_ne_one : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f : G → R},
  conjneg f ≠ 1 ↔ f ≠ 1
-- Mathlib.Topology.NhdsWithin
IsOpen.nhdsWithin_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, IsOpen s → a ∈ s → nhdsWithin a s = nhds a
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse_of_rightInverse_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) {h : P → N} (hgh : Function.RightInverse h ⇑g) (y : TensorProduct R Q N),
  (lTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.instNonemptyPair : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (X Y : C),
  (CategoryTheory.ObjectProperty.pair X Y).Nonempty
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.error.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticSeverity.error = 1
-- Mathlib.Order.RelSeries
LTSeries.last_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (p : LTSeries α) (f : α → β)
  (hf : StrictMono f), RelSeries.last (p.map f hf) = f (RelSeries.last p)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.mk : Lean.Name → Lean.Meta.MatcherInfo → Lean.Meta.Match.Extension.Entry
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_id_atTop : ∀ {E'' : Type u_9} [inst : NormedAddCommGroup E''] (c : E''), (fun _x => c) =o[Filter.atTop] id
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- A family of morphisms with the same target inducing an isomorphism from the coproduct to the target
is an `EffectiveEpiFamily`.
 -/
CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            [inst_1 : CategoryTheory.Limits.HasCoproduct X] →
              [CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)] → CategoryTheory.EffectiveEpiFamilyStruct X π
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The product of two non-unital star subalgebras is a non-unital star subalgebra.  -/
NonUnitalStarSubalgebra.prod : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalSemiring A] →
          [inst_2 : StarRing A] →
            [inst_3 : Module R A] →
              [inst_4 : NonUnitalSemiring B] →
                [inst_5 : StarRing B] →
                  [inst_6 : Module R B] →
                    NonUnitalStarSubalgebra R A → NonUnitalStarSubalgebra R B → NonUnitalStarSubalgebra R (A × B)
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_def : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)),
  o.volumeForm =
    Nat.casesAuxOn (motive := fun a => n = a → E [⋀^Fin n]→ₗ[ℝ] ℝ) n
      (fun h =>
        Eq.ndrec (motive := fun {n} =>
          [_i : Fact (Module.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ)
          (fun [Fact (Module.finrank ℝ E = 0)] o =>
            have opos := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1;
            ⋯.by_cases (fun x => opos) fun x => -opos)
          ⋯ o)
      (fun n_1 h =>
        Eq.ndrec (motive := fun {n} =>
          [_i : Fact (Module.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ)
          (fun [Fact (Module.finrank ℝ E = n_1 + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km → km ∈ t
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toIsScalarTower : ∀ {A : Type u_1} [self : NonUnitalCommCStarAlgebra A], IsScalarTower ℂ A A
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- If a sequence of almost everywhere strongly measurable functions converges almost everywhere,
one can select a strongly measurable function as the almost everywhere limit.  -/
exists_stronglyMeasurable_limit_of_tendsto_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [TopologicalSpace.PseudoMetrizableSpace β] {f : ℕ → α → β},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds l)) →
      ∃ f_lim,
        MeasureTheory.StronglyMeasurable f_lim ∧
          ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.mk.injEq : ∀ (isHoverPosOnStop : Bool) (size : ℕ) (isVariableInfo isPartialTermInfo isHoverPosOnStop_1 : Bool) (size_1 : ℕ)
  (isVariableInfo_1 isPartialTermInfo_1 : Bool),
  ({ isHoverPosOnStop := isHoverPosOnStop, size := size, isVariableInfo := isVariableInfo,
        isPartialTermInfo := isPartialTermInfo } =
      { isHoverPosOnStop := isHoverPosOnStop_1, size := size_1, isVariableInfo := isVariableInfo_1,
        isPartialTermInfo := isPartialTermInfo_1 }) =
    (isHoverPosOnStop = isHoverPosOnStop_1 ∧
      size = size_1 ∧ isVariableInfo = isVariableInfo_1 ∧ isPartialTermInfo = isPartialTermInfo_1)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.maximumIndepSet_exists : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α], ∃ s, G.IsMaximumIndepSet s
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveObjPostcompose₂ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive E] {E' : Type u_4}
  [inst_5 : CategoryTheory.Category.{v_4, u_4} E'] [inst_6 : CategoryTheory.Preadditive E']
  (G : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (F : CategoryTheory.Functor E E') [F.Additive]
  [G.Additive], ((CategoryTheory.Functor.postcompose₂.obj F).obj G).Additive
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- If a measure `ρ` is singular with respect to `μ`, then for `μ` almost every `x`, the ratio
`ρ a / μ a` tends to zero when `a` shrinks to `x` along the Vitali family. This makes sense
as `μ a` is eventually positive by `ae_eventually_measure_pos`.  -/
VitaliFamily.ae_eventually_measure_zero_of_singular : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.MutuallySingular μ → ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ρ a / μ a) (v.filterAt x) (nhds 0)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLE.toPosMulStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [PosMulReflectLE α], PosMulStrictMono α
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (p : PolynomialModule R M), (PolynomialModule.eval r) p = p.coeff.sum fun i m => r ^ i • m
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- The weight of a path is the product of the weights of its edges.  -/
Quiver.Path.weight : {V : Type u_1} →
  [inst : Quiver V] → {R : Type u_2} → [Monoid R] → ({i j : V} → (i ⟶ j) → R) → {i j : V} → Quiver.Path i j → R
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_iso_hom : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).iso.hom =
    CategoryTheory.CategoryStruct.id
      (X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalWithAnnotateState : Lean.Elab.Tactic.Tactic
-- Init.Data.SInt.Bitwise
Int16.or_self : ∀ {a : Int16}, a ||| a = a
-- Mathlib.Data.Nat.Factorial.BigOperators
/-- `k!` divides the product of any `k` consecutive integers.  -/
Nat.factorial_coe_dvd_prod : ∀ (k : ℕ) (n : ℤ), ↑k.factorial ∣ ∏ i ∈ Finset.range k, (n + ↑i)
-- Mathlib.Data.Finset.Insert
Finset.coe_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑(insert a s) = insert a ↑s
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.notMem_idealOfSet : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] {s : Set X} {f : C(X, R)}, f ∉ ContinuousMap.idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0
-- Batteries.Data.List.Basic
List.dropSlice.eq_1 : ∀ {α : Type u_1} (x x_1 : ℕ), List.dropSlice x x_1 [] = []
-- Mathlib.Order.Hom.Lex
RelIso.sumLexComplLeft_symm_apply : ∀ {α : Type u_1} {r : α → α → Prop} {x : α} [inst : IsTrans α r] [inst_1 : Std.Trichotomous r] [inst_2 : DecidableRel r]
  (a : { x_1 // r x_1 x } ⊕ { x_1 // ¬r x_1 x }), (RelIso.sumLexComplLeft r x) a = (Equiv.sumCompl fun x_1 => r x_1 x) a
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.encodeList.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Mathlib.Topology.Algebra.Module.TransferInstance
/-- Shrinking `α` to a smaller universe preserves the continuous module structure.  -/
Shrink.continuousLinearEquiv : (R : Type u_1) →
  (α : Type u_2) →
    [inst : Small.{v, u_2} α] →
      [inst_1 : AddCommMonoid α] →
        [inst_2 : TopologicalSpace α] → [inst_3 : Semiring R] → [inst_4 : Module R α] → Shrink.{v, u_2} α ≃L[R] α
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Composition of affine maps.  -/
AffineMap.comp : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          {V3 : Type u_6} →
            {P3 : Type u_7} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V1] →
                  [inst_2 : Module k V1] →
                    [inst_3 : AddTorsor V1 P1] →
                      [inst_4 : AddCommGroup V2] →
                        [inst_5 : Module k V2] →
                          [inst_6 : AddTorsor V2 P2] →
                            [inst_7 : AddCommGroup V3] →
                              [inst_8 : Module k V3] →
                                [inst_9 : AddTorsor V3 P3] → (P2 →ᵃ[k] P3) → (P1 →ᵃ[k] P2) → P1 →ᵃ[k] P3
-- Mathlib.Algebra.Order.Hom.Units
OrderMonoidIso.val_inv_unitsCongr_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Monoid α] [inst_2 : Preorder β] [inst_3 : Monoid β]
  (e : α ≃*o β) (a : βˣ), ↑(e.unitsCongr.symm a)⁻¹ = (↑e).symm ↑a⁻¹
-- Lean.Meta.CoeAttr
Lean.Meta.instReprCoeFnType : Repr Lean.Meta.CoeFnType
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_mono_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q : l},
  Lean.Order.PartialOrder.rel P P' → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) (Lean.Order.meet P' Q)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opENorm_flip : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G), ‖f.flip‖ₑ = ‖f‖ₑ