mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesAux.eq_def : ∀ (G : Type u_1) [inst : Group G] (x : ℕ),
  Subgroup.upperCentralSeriesAux G x =
    match x with
    | 0 => ⟨⊥, ⋯⟩
    | n.succ =>
      let un := Subgroup.upperCentralSeriesAux G n;
      have _un_characteristic := ⋯;
      ⟨un.fst.upperCentralSeriesStep, ⋯⟩
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCastD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getValueCastD k l₁ fallback else fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.degree_polynomial : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} [Nontrivial R], W.polynomial.degree = 2
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `f ≫ g`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
/-- Inversion sends an affine subspace passing through the center to itself.  -/
EuclideanGeometry.image_inversion_affineSubspace_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c : P} {R : ℝ} {p : AffineSubspace ℝ P},
  R ≠ 0 → c ∈ p → EuclideanGeometry.inversion c R '' ↑p = ↑p
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition' : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F₁.obj i ⟶[V] F₂.obj i)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F₁.obj i ⟶[V] F₂.obj i)
            ((CategoryTheory.eHomEquiv V) (F₂.map f)))
          (CategoryTheory.eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F₁.obj j ⟶[V] F₂.obj j)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.eHomEquiv V) (F₁.map f))
            (F₁.obj j ⟶[V] F₂.obj j))
          (CategoryTheory.eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_pow`

---

The order multiplies by `n` when taking a meromorphic function to its `n`th power.  -/
fun_meromorphicOrderAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  MeromorphicAt f x → ∀ {n : ℕ}, meromorphicOrderAt (fun i => f i ^ n) x = ↑n * meromorphicOrderAt f x
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mul_def : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (f g : 𝒜 →+*ᵍ 𝒜),
  f * g = f.comp g
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.aeval_add : ∀ {R : Type u_1} [inst : CommRing R] {p : Polynomial R} {n : ℕ},
  p.IsMonicOfDegree n → ∀ (r : R), ((Polynomial.aeval (Polynomial.X + Polynomial.C r)) p).IsMonicOfDegree n
-- Mathlib.Data.Ordmap.Ordset
/-- O(1). Is the set empty?  -/
Ordset.Empty : {α : Type u_1} → [inst : Preorder α] → Ordset α → Prop
-- Mathlib.Order.BoundedOrder.Basic
OrderTop.ext_top : ∀ {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α),
  (∀ (x y : α), x ≤ y ↔ x ≤ y) → ⊤ = ⊤
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.end : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {P : Type u_5} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  [inst_7 : Module S P] [inst_8 : IsScalarTower R S P] [Module.Free R M] [Module.Finite R M] {α : M →ₗ[R] P}
  (j : IsBaseChange S α), IsBaseChange S j.endHom
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G` preserves every pointwise extensions of `F` along `L` at `c`.  -/
CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} A}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} D} {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} {c : C} [self : G.PreservesPointwiseRightKanExtensionAt F L c]
  (E : L.RightExtension F) (a : E.IsPointwiseRightKanExtensionAt c),
  Nonempty (((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.degree_eraseLead_lt : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f ≠ 0 → f.eraseLead.degree < f.degree
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeletonLT_zero_eq_base : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ↑(Topology.RelCWComplex.skeletonLT C 0) = D
-- Lean.Parser.Command
Lean.Parser.Command.ctor : Lean.Parser.Parser
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  {inst_3 : Semiring B} {inst_4 : Algebra R B} {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B}
  {toCoalgHom : A →ₗc[R] B} {map_one' : toCoalgHom.toFun 1 = 1}
  {map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y}
  {toCoalgHom_1 : A →ₗc[R] B} {map_one'_1 : toCoalgHom_1.toFun 1 = 1}
  {map_mul'_1 : ∀ (x y : A), toCoalgHom_1.toFun (x * y) = toCoalgHom_1.toFun x * toCoalgHom_1.toFun y},
  { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' } =
      { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toCoalgHom = toCoalgHom_1
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.instInhabitedArgsPacker : Inhabited Lean.Meta.ArgsPacker
-- Mathlib.Order.CompleteLattice.Defs
/-- Transfer `InfSet` across an `Equiv`.  -/
Equiv.infSet : {α : Type u_1} → {β : Type u_2} → α ≃ β → [InfSet β] → InfSet α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams.toTextDocumentPositionParams : Lean.Lsp.DocumentHighlightParams → Lean.Lsp.TextDocumentPositionParams
-- Init.Data.UInt.Bitwise
UInt32.ofFin_shiftLeft : ∀ (a b : Fin UInt32.size), ↑b < 32 → UInt32.ofFin (a <<< b) = UInt32.ofFin a <<< UInt32.ofFin b
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `L` and `G` are fully faithful and their domain
and codomain have all pullbacks resp. pushouts, the natural transformation `L ⟶ G` is an
epimorphism iff the natural transformation `R ⟶ F` is a monomorphism.  -/
CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R) [inst_2 : L.Full]
  [inst_3 : L.Faithful] [inst_4 : G.Full] [inst_5 : G.Faithful] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.HasPushouts D],
  CategoryTheory.Epi q.leftTriple.leftToRight ↔ CategoryTheory.Mono q.rightTriple.rightToLeft
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f pf s x r →
    HasFPowerSeriesWithinOnBall g pg s x r → HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r
-- Mathlib.Topology.Compactness.CountablyCompact
/-- Every infinite subset of a countably compact set has an accumulation point in the set.  -/
IsCountablyCompact.exists_accPt_of_infinite : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A B : Set E},
  IsCountablyCompact A → B ⊆ A → B.Infinite → ∃ a ∈ A, AccPt a (Filter.principal B)
-- Mathlib.AlgebraicGeometry.Scheme
/-- See Note [custom simps projection]  -/
AlgebraicGeometry.Scheme.Hom.Simps.toLRSHom : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → (X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_smul : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (r : R) (f : M →ₗ[R] N), LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
liminf_mul_le : ∀ {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot],
  0 ≤ᶠ[f] u →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v →
          Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.w.eq_1 : ∀ (u : PNat.XgcdType), u.w = u.wp.succPNat
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A measure space is a measurable space equipped with a
measure, referred to as `volume`.  -/
MeasureTheory.MeasureSpace : Type u_6 → Type u_6
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited β]
  (t t_1 : Std.ExtTreeMap α β cmp), t = t_1 → ∀ (a a_1 : α), a = a_1 → t.get! a = t_1.get! a_1
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option α
-- Mathlib.Data.Rel.Separated
SetRel.isSeparated_insert_of_notMem : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm],
  x ∉ s → (R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ y ∈ s, (x, y) ∉ R)
-- Init.Data.SInt.Lemmas
Int32.toInt64_ofIntLE : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt),
  (Int32.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
-- Std.Async.Basic
Std.Async.EAsync.instMonadFinally : {ε : Type} → MonadFinally (Std.Async.EAsync ε)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_ne_top : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {f : Ω → ENNReal},
  ∫⁻ (x : Ω), f x ∂P ≠ ⊤ → ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x ≠ ⊤
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findEntry? : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → Option (α × β)
-- Std.Sat.AIG.LawfulOperator
/-- If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an
index in bounds of `decls1` we can evaluate at `decls1`.
 -/
Std.Sat.AIG.denote.go_eq_of_isPrefix : ∀ {α : Type} {assign : α → Bool} (decls1 decls2 : Array (Std.Sat.AIG.Decl α)) (start : ℕ)
  {hdag1 : Std.Sat.AIG.IsDAG α decls1} {hdag2 : Std.Sat.AIG.IsDAG α decls2} {hbounds1 : start < decls1.size}
  {hbounds2 : start < decls2.size},
  Std.Sat.AIG.IsPrefix decls1 decls2 →
    Std.Sat.AIG.denote.go start decls2 assign hbounds2 hdag2 = Std.Sat.AIG.denote.go start decls1 assign hbounds1 hdag1
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.eventually_isUnit_resolvent : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), ∀ᶠ (z : 𝕜) in Bornology.cobounded 𝕜, IsUnit (resolvent a z)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.cos x = Real.sin b - Real.sin a
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_snd_v : ∀ {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 φ] (p q : ℤ)
  (hpq : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      ((CochainComplex.mappingCocone.snd φ).v p q hpq) =
    0
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.instNNRatCast : {K : Type u_1} → [Field K] → {a b : K} → NNRatCast (QuadraticAlgebra K a b)
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquivKer.eq_1 : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a : α),
  f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (Subgroup.leftCosetEquivSubgroup a)
-- Mathlib.Order.Filter.Lift
Filter.lift'_principal : ∀ {α : Type u_1} {β : Type u_2} {h : Set α → Set β} {s : Set α},
  Monotone h → (Filter.principal s).lift' h = Filter.principal (h s)
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_gate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {lhs rhs : Std.Sat.AIG.Fanin} {aig : Std.Sat.AIG α} {r : α → β}
  {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size},
  (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs →
    aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs
-- Mathlib.Algebra.Order.Group.Equiv
/-- `ofLex` as an `AddEquiv`.  -/
ofLexAddEquiv : (α : Type u_1) → [inst : Add α] → Lex α ≃+ α
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanDidOpenTextDocumentParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanDidOpenTextDocumentParams
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_unique : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (f f' : Ω[S⁄R] →ₗ[S] M), f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S) → f = f'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l →
    (∀ a ∈ m, (List.map Prod.fst l).contains a = false) → (Std.DHashMap.Const.insertMany m l).size = m.size + l.length
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
deriv_riemannZeta_add_inv_sub_sq_bounded : (fun s => deriv riemannZeta s + (s - 1)⁻¹ ^ 2) =O[nhdsWithin 1 {1}ᶜ] fun x => 1
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot_apply : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0)
  (a : S), (pb.equivOfRoot pb' h₁ h₂) a = (pb.lift pb'.gen h₂) a
-- Mathlib.Analysis.Normed.Group.Uniform
dist_sub_eq_dist_add_left : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a b c : E), dist (a - b) c = dist a (c + b)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Asymptotics.IsBigO.comp_summable : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [CompleteSpace F] {f : E → F},
  f =O[nhds 0] id → ∀ {g : ι → E}, Summable g → Summable (f ∘ g)
-- Mathlib.Topology.DerivedSet
derivedSet.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A : Set X), derivedSet A = {x | AccPt x (Filter.principal A)}
-- Lean.Declaration
Lean.DefinitionSafety : Type
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.hom_ext : ∀ {R : Type u} [inst : Ring R] {V W : FGModuleCat R} {f g : V ⟶ W},
  ModuleCat.Hom.hom f.hom = ModuleCat.Hom.hom g.hom → f = g
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_equivariantMap_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α},
  Function.Injective ⇑(SubMulAction.ofFixingSubgroup_equivariantMap M s)
-- Lean.Compiler.LCNF.Basic
/-- The reset instruction from Counting Immutable Beans. `n` is the amount of object fields stored in
the constructor in `var`.
 -/
Lean.Compiler.LCNF.LetValue.reset : {pu : Lean.Compiler.LCNF.Purity} →
  ℕ →
    Lean.FVarId →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17 →
        Lean.Compiler.LCNF.LetValue pu
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.serverBaseExts : Lean.Environment → Array Lean.EnvExtensionState
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.of_wellFoundedLT_associates : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α], WellFoundedLT (Associates α) → WfDvdMonoid α
-- Mathlib.Data.Erased
/-- Extracts the erased value, if it is a proof.  -/
Erased.out_proof : ∀ {p : Prop} (a : Erased p), p
-- Mathlib.Data.Real.Sign
/-- The sign function that maps negative real numbers to -1, positive numbers to 1, and 0
otherwise.  -/
Real.sign : ℝ → ℝ
-- Mathlib.Order.Monotone.Basic
List.foldl_strictMono : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {f : α → β → α},
  (∀ (b : β), StrictMono fun a => f a b) → ∀ (l : List β), StrictMono fun a => List.foldl f a l
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.mk : (carrier : Type u) → [str : AddCommGroup carrier] → AddCommGrpCat
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_eq_ofIntClamp : ∀ {x : ℤ} {h₁ : Int64.minValue.toInt ≤ x} {h₂ : x ≤ Int64.maxValue.toInt}, Int64.ofIntLE x h₁ h₂ = Int64.ofIntClamp x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X₀ : C₀)
  (i : (data (F.obj X₀)).I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv data G₀ X₀)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i) =
    CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj X₀)).f i)
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitorEquivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.leftUnitorEquivalence C).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Discrete PUnit.{w + 1} × C))
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- Expand the definition of `proximity f a₀` in case where `a₀` is zero.
 -/
ValueDistribution.proximity_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E},
  ValueDistribution.proximity f 0 = Real.circleAverage (fun x => ‖f x‖⁻¹.posLog) 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_roo_eq : ∀ {m n i : ℕ}, ((m<...n).toArray[i]?.isNone = true) = (n ≤ i + (m + 1))
-- Init.Data.Fin.Lemmas
Fin.not_lt_zero : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), ¬a < 0
-- Init.Data.List.Monadic
List.flatMapM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [inst : Monad m] [LawfulMonad m]
  {f : α → m (List β)},
  List.flatMapM f (a :: l) = do
    let bs ← f a
    let __do_lift ← List.flatMapM f l
    pure (bs ++ __do_lift)
-- Lean.Elab.App
/-- Infer the `motive` using the expected type by `kabstract`ing the discriminants.  -/
Lean.Elab.Term.ElabElim.mkMotive : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv_symm_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β), ↑(RelIso.ofOnFun r f).symm = f.symm
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff_null' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ (s₁ ∩ s₂) = 0 → μ (s₁ \ s₂) = μ s₁
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism version of `sup_le`.  -/
CategoryTheory.MonoOver.supLe : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasImages C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        {A : C} →
          (f g h : CategoryTheory.MonoOver A) → (f ⟶ h) → (g ⟶ h) → ((CategoryTheory.MonoOver.sup.obj f).obj g ⟶ h)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- `mapGrp` is functorial in the left-exact functor.  -/
CategoryTheory.Functor.mapGrpFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.Functor (CategoryTheory.Grp C) (CategoryTheory.Grp D))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_hom : ∀ {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 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp X.hom (e.inv.app X.right)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- The rank (supremum of the cardinalities of bases) of a matroid `M` as a `Cardinal`.
See `Matroid.eRank` for a better-behaved `ℕ∞`-valued version.  -/
Matroid.cRank : {α : Type u} → Matroid α → Cardinal.{u}
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `diagonal v` is invertible if `v` is  -/
Matrix.diagonalInvertible : {n : Type u'} →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] →
      {α : Type u_2} → [inst_2 : NonAssocSemiring α] → (v : n → α) → [Invertible v] → Invertible (Matrix.diagonal v)
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.ofNat : ℕ → Lean.Lsp.MarkupKind