mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.SDiff
Finset.Nontrivial.sdiff_singleton_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {c : α} {s : Finset α}, s.Nontrivial → (s \ {c}).Nonempty
-- Init.Grind.Config
Lean.Grind.CutsatConfig.mk.injEq : ∀ (toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig),
  ({ toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 }) = (toNoopConfig = toNoopConfig_1)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.Equiv.eq_1 : ∀ (self : Batteries.UnionFind) (a b : ℕ), self.Equiv a b = (self.rootD a = self.rootD b)
-- Mathlib.Data.NNReal.Defs
NNReal.bot_eq_zero : ⊥ = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Polynomial.Chebyshev.complex_ofReal_eval_T : ∀ (x : ℝ) (n : ℤ), ↑(Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.T ℂ n)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.Limits.imageSubobjectIso f = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.image.ι f)
-- Mathlib.Data.Num.Bitwise
/-- Multiply two `SNum`s.  -/
SNum.mul : SNum → SNum → SNum
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mk_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A →ₐ[R] B} (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
        { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r),
  { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
-- Mathlib.RingTheory.Localization.BaseChange
instIsLocalizationAlgebraMapSubmonoidSubmonoid : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization (Algebra.algebraMapSubmonoid S (IsUnit.submonoid R)) S
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.instDecidableEqList.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (head : α) → (tail : List α) → motive (head :: tail)),
  (match [] with
    | [] => h_1 ()
    | head :: tail => h_2 head tail) =
    h_1 ()
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodComm_symm : ∀ (R₁ : Type u_1) [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  (M₂ : Type u_5) [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂], (ContinuousLinearEquiv.prodComm R₁ M₁ M₂).symm = ContinuousLinearEquiv.prodComm R₁ M₂ M₁
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
  Filter.map (⇑h.symm) (nhds (h x)) = nhds x
-- Mathlib.Data.Vector.Defs
/-- `take` of vectors corresponds under `toList` to `take` of lists.  -/
List.Vector.toList_take : ∀ {α : Type u_1} {n m : ℕ} (v : List.Vector α m), (List.Vector.take n v).toList = List.take n v.toList
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.neBot_or_eq_bot : ∀ {β : Type u_2} (L : SummationFilter β), L.NeBot ∨ L.filter = ⊥
-- Lean.Parser.Command
Lean.Parser.Command.visibility.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.CoreM
Lean.Core.instantiateTypeLevelParams : Lean.ConstantVal → List Lean.Level → Lean.CoreM Lean.Expr
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₄ =
    CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.right φ)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.median.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex k P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.median i = s_1.median i_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.instIsIsoHomHomCone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d), CategoryTheory.IsIso f.hom.hom
-- Std.Do.WP.SimpLemmas
Std.Do.WP.getThe_MonadStateOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond σ ps} [inst : Std.Do.WP m ps]
  [inst_1 : MonadStateOf σ m], (Std.Do.wp (getThe σ)).apply Q = (Std.Do.wp MonadStateOf.get).apply Q
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.instFintypeElemSym2EdgeSetEdge : {V : Type u_1} → {s t : V} → [DecidableEq V] → Fintype ↑(SimpleGraph.edge s t).edgeSet
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.tactic.sizeOf_spec : ∀ (tacticCode : Lean.Syntax) (ctx : Lean.Elab.Term.SavedContext) (kind : Lean.Elab.Term.TacticMVarKind)
  (delayOnMVars : optParam Bool false),
  sizeOf (Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode ctx kind delayOnMVars) =
    1 + sizeOf tacticCode + sizeOf ctx + sizeOf kind + sizeOf delayOnMVars
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.pi_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [inst_1 : MulOneClass γ]
  (g : (i : I) → γ →* f i) (x : γ) (i : I), (MonoidHom.pi g) x i = (g i) x
-- Mathlib.Data.Complex.Basic
Complex.commRing : CommRing ℂ
-- Mathlib.Algebra.Group.Defs
SubtractionCommMonoid.toSubtractionMonoid : {G : Type u} → [self : SubtractionCommMonoid G] → SubtractionMonoid G
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  AlgebraicGeometry.Scheme.Hom.appLE f U V e =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (X.presheaf.map (CategoryTheory.homOfLE e).op)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_eq_get_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m.getKey a h = (m.getKey? a).get ⋯
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (xi : ↥(𝒰.X i))
  (xj : ↥(𝒰.X j)), (𝒰.f i) xi = (𝒰.f j) xj → ∃ k fi fj xk, (𝒰.trans fi) xk = xi ∧ (𝒰.trans fj) xk = xj
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.instFunLike.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} [inst : Group G],
  FreeGroupBasis.instFunLike = { coe := fun b i => b.repr.symm (FreeGroup.of i), coe_injective := ⋯ }
-- Mathlib.LinearAlgebra.Orientation
Module.Oriented.mk : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] → {ι : Type u_4} → Orientation R M ι → Module.Oriented R M ι
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  α.naturality (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.Bicategory.whiskerRightIso (F.mapComp f g) (α.app c) ≪≫
      CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c) ≪≫
        CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (α.naturality g) ≪≫
          (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).symm ≪≫
            CategoryTheory.Bicategory.whiskerRightIso (α.naturality f) (G.map g) ≪≫
              CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g) ≪≫
                CategoryTheory.Bicategory.whiskerLeftIso (α.app a) (G.mapComp f g).symm
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_le_smul_left : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M M' : AddSubmonoid R} {P : AddSubmonoid A}, M ≤ M' → M • P ≤ M' • P
-- Mathlib.CategoryTheory.Comma.Basic
/-- The equality between `map α β ⋙ snd L' R'` and `snd L R ⋙ F₂`,
where `β : R ⋙ F ⟶ F₂ ⋙ R'`.  -/
CategoryTheory.Comma.map_snd : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} A']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'}
  {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'}
  (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R'),
  (CategoryTheory.Comma.map β α).comp (CategoryTheory.Comma.snd L' R') = (CategoryTheory.Comma.snd L R).comp F₂
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.restrict_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) (x : S), H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) (φ x)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Finpartition.energy.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α)
  [inst_1 : DecidableRel G.Adj], P.energy G = (∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑P.parts.card ^ 2
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_mem : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R),
  (MvPolynomial.homogeneousComponent n) φ ∈ MvPolynomial.homogeneousSubmodule σ R n
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit'_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I C) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.op.comp CategoryTheory.coyoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (D.obj i)))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.op.comp CategoryTheory.coyoneda) (Opposite.op i)).app (D.obj i)))
            (CategoryTheory.CategoryStruct.id (D.obj i))) }
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.nonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), (↑s).Nonempty
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.congr_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y),
  F.map f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯))
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d))
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.instHasFiniteBiproducts : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R)
-- Std.Data.TreeMap.Raw.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.TreeMap.Raw.Equiv : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.coneOfAdj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} (adj : CategoryTheory.Functor.const J ⊣ L)
  (F : CategoryTheory.Functor J C), (CategoryTheory.Limits.coneOfAdj adj F).pt = L.obj F
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYonedaComponents_hom : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : LightProfinite) [inst_1 : Finite ↑X.toTop],
  (LightCondensed.isoFinYonedaComponents F X).hom =
    TypeCat.ofHom fun y x =>
      (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op)) y
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`, provided `a` is not a bottom element.  -/
mem_nhdsLE_iff_exists_Ioc_subset' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a l' : α} {s : Set α},
  l' < a → (s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l ∈ Set.Iio a, Set.Ioc l a ⊆ s)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl} {f : ℝ → ℝ},
  coef.Trimmed →
    ¬coef.IsZero →
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
          (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Trimmed
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_eq_getD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.get! a = m.getD a default
-- Mathlib.Util.CountHeartbeats
/-- Given a `List Nat`, log an info message with the minimum, maximum, and standard deviation.
 -/
Mathlib.CountHeartbeats.logVariation : {m : Type → Type} → [Monad m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → List ℕ → m Unit
-- Mathlib.Control.Traversable.Lemmas
Traversable.traverse_id : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {α : Type u}, traverse pure = pure
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.mapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y')
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  (CategoryTheory.Limits.cokernel.mapIso f f' p q w).hom = CategoryTheory.Limits.cokernel.map f f' p.hom q.hom w
-- Mathlib.Data.ENNReal.Basic
/-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
and is relevant as the codomain of a measure.  -/
ENNReal.«termℝ≥0∞» : Lean.ParserDescr
-- Mathlib.NumberTheory.MulChar.Duality
/-- The order reversing bijection that sends a subgroup of `Mˣ` to its dual subgroup in
`MulChar M R` where `M` is a finite commutative monoid and `R` is a ring with enough
roots of unity.
 -/
MulChar.subgroupOrderIsoSubgroupMulChar : (M : Type u_1) →
  (R : Type u_2) →
    [inst : CommMonoid M] →
      [inst_1 : CommRing R] →
        [Finite M] → [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] → Subgroup Mˣ ≃o (Subgroup (MulChar M R))ᵒᵈ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h_1 : (self.map (CategoryTheory.CategoryStruct.comp f h)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) h_1 =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp ((self.mapComp f h).inv.toNatTrans.app X) h_1))
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- If an additive group `G` acts faithfully on `α`,
then it acts faithfully on `powersetCard α n`,
provided `1 ≤ n < ENat.card α`.  -/
Set.powersetCard.faithfulVAdd : ∀ {α : Type u_2} [inst : DecidableEq α] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G α] {n : ℕ},
  1 ≤ n → ↑n < ENat.card α → ∀ [FaithfulVAdd G α], FaithfulVAdd G ↑(Set.powersetCard α n)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.not : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  FreeGroup.Red.Step (L₁ ++ (x, b) :: (x, !b) :: L₂) (L₁ ++ L₂)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.entryAtIdx! : {α : Type u} → {β : Type v} → [Inhabited (α × β)] → (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → α × β
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toUInt32 = UInt32.ofNat ↑n
-- Mathlib.RingTheory.AdicCompletion.Topology
Submodule.instPowNat.congr_simp : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A], Submodule.instPowNat = Submodule.instPowNat
-- Mathlib.Algebra.Category.AlgCat.Monoidal
/-- Auxiliary definition used to fight a timeout when building
`AlgCat.instMonoidalCategory`.  -/
AlgCat.instMonoidalCategory.tensorObj : {R : Type u} → [inst : CommRing R] → AlgCat R → AlgCat R → AlgCat R
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- API for PullbackCone.IsLimit.lift for `IsPullback`  -/
CategoryTheory.IsPullback.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P X Y Z : C} →
      {fst : P ⟶ X} →
        {snd : P ⟶ Y} →
          {f : X ⟶ Z} →
            {g : Y ⟶ Z} →
              CategoryTheory.IsPullback fst snd f g →
                {W : C} →
                  (h : W ⟶ X) →
                    (k : W ⟶ Y) →
                      CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g → (W ⟶ P)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toZPow : {K : Type u_2} → [self : DivisionSemiring K] → ZPow K
-- Std.Internal.Do.PredTrans
/-- Apply the predicate transformer to a postcondition and exception postcondition.  -/
Std.Internal.Do.PredTrans.apply : {Pred : Type u} → {EPred : Type v} → {α : Type w} → Std.Internal.Do.PredTrans Pred EPred α → (α → Pred) → EPred → Pred
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Equivalence.pi_inverse : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i),
  (CategoryTheory.Equivalence.pi E).inverse = CategoryTheory.Functor.pi fun i => (E i).inverse
-- Mathlib.Data.Sym.NatCard
Sym2.ncard_diagSet_compl : ∀ (α : Type u_1), Sym2.diagSetᶜ.ncard = (Nat.card α).choose 2
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] [Finite G],
  Representation.Coinvariants.ker (Representation.leftRegular k G) =
    ((Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_lt_two_pow : ∀ (n k : ℕ), 0 < n → n.choose k < 2 ^ n
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_prod : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {ι : Type u_4} (t : Finset ι) (f : ι → M) (s : ι → ↥S),
  ∏ i ∈ t, Localization.mk (f i) (s i) = Localization.mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.union_nonempty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ},
  AEMeasurable f μ → AEMeasurable (fun z => f z.1) (μ.prod ν)
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_natCast : ∀ (n : ℕ), (↑n).toNNReal = ↑n
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.isEmpty_eq_false_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false ↔ ¬t = ∅