mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationDomain.radical_neg_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizationMonoid R] [inst_2 : UniqueFactorizationMonoid R],
  UniqueFactorizationMonoid.radical (-1) = 1
-- Mathlib.Data.Finset.Card
Finset.sdiff_nonempty_of_card_lt_card : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s.card < t.card → (t \ s).Nonempty
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instIsIsoFunctorOfIsLeftKanExtensionOppositeType : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α], CategoryTheory.IsIso α
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step_cons_of_isLT_eq_false : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β} [inst : Ord α] {upper : α} {h : (compare k upper).isLT = false},
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step = Std.IterStep.done
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- Constructor for morphisms in a full subcategory.  -/
CategoryTheory.ObjectProperty.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} → {X Y : P.FullSubcategory} → (X.obj ⟶ Y.obj) → (X ⟶ Y)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.erase_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α},
  ∅.erase k = ∅
-- Init.Data.List.Lemmas
List.getLast_dropLast : ∀ {α : Type u_1} {xs : List α} (h : xs.dropLast ≠ []), xs.dropLast.getLast h = xs[xs.length - 2]
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `x : K` is the valuation of `r` divided by the valuation of `s`,
where `r` and `s` are chosen so that `x = r/s`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → Valuation K (WithZero (Multiplicative ℤ))
-- Mathlib.Data.NNRat.Defs
NNRat.num_coe : ∀ (q : ℚ≥0), (↑q).num = ↑q.num
-- Lean.Meta.Instances
Lean.Meta.isInstanceCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.Algebra.Order.UpperLower
HasUpperLowerClosure.isLowerSet_closure : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α),
  IsLowerSet s → IsLowerSet (closure s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter!_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, (Std.DTreeMap.Internal.Impl.alter! k f t).size ≤ t.size + 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- If `M` is a monoid object acting on `X`, then morphisms into `M` act on
morphisms into `X`.  -/
CategoryTheory.Hom.mulAction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.MonObj M] → {X : C} → [CategoryTheory.ModObj M X] → (Z : C) → MulAction (Z ⟶ M) (Z ⟶ X)
-- Mathlib.Order.Filter.Extr
IsExtrFilter.filter_inf : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → ∀ (l' : Filter α), IsExtrFilter f (l ⊓ l') a
-- Std.Data.DHashMap.Basic
Std.DHashMap.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, LawfulSingleton ((a : α) × β a) (Std.DHashMap α β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl =
    (!compare k a == Ordering.eq && Std.DTreeMap.Internal.Impl.contains a t)
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasDerivAtFilter.hasGradientAtFilter : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} {L' : Filter 𝕜},
  HasDerivAtFilter g g' (L' ×ˢ pure u) → HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A sequence of functions `(fₙ)` is uniformly integrable in the probability sense if for all
`ε > 0`, there exists some `C` such that `∫ x in {|fₙ| ≥ C}, fₙ x ∂μ ≤ ε` for all `n`.  -/
MeasureTheory.uniformIntegrable_of : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {p : ENNReal} {f : ι → α → β} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
        (∀ (ε : ℝ),
            0 < ε → ∃ C, ∀ (i : ι), MeasureTheory.eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε) →
          MeasureTheory.UniformIntegrable f p μ
-- Mathlib.Algebra.Algebra.Spectrum.Pi
Prod.spectrum_eq : ∀ {A : Type u_2} {B : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : A) (b : B), spectrum R (a, b) = spectrum R a ∪ spectrum R b
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.differentiable_arsinh : Differentiable ℝ Real.arsinh
-- Mathlib.Computability.TuringMachine.Config
/-- The type of continuations, built up during evaluation of a `Code` expression.  -/
Turing.ToPartrec.Cont : Type
-- Mathlib.Topology.Algebra.AffineSubspace
/-- `AffineEquiv.ofEq` as a continuous affine equivalence.  -/
AffineSubspace.ofEq : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] →
            [inst_3 : TopologicalSpace P] →
              [inst_4 : AddTorsor V P] →
                {s t : AffineSubspace R P} → [inst_5 : Nonempty ↥s] → [inst_6 : Nonempty ↥t] → s = t → ↥s ≃ᴬ[R] ↥t
-- Std.Data.DTreeMap.Internal.Operations
/-- The value.  -/
Std.DTreeMap.Internal.Impl.RawView.v : {α : Type u} → {β : α → Type v} → (self : Std.DTreeMap.Internal.Impl.RawView α β) → β self.k
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra homomorphism* is an algebra homomorphism between `R`-algebras `A` and `B`
equipped with a `star` operation, and this homomorphism is also `star`-preserving.  -/
«term_→⋆ₐ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.mul_prod_eraseIdx : ∀ {M : Type u_4} [inst : Monoid M] {l : List M} {i : ℕ} (hlen : i < l.length),
  (∀ a' ∈ List.take i l, Commute l[i] a') → l[i] * (l.eraseIdx i).prod = l.prod
-- Init.Data.SInt.Lemmas
Int64.toInt_toISize : ∀ (x : Int64), x.toISize.toInt = x.toInt.bmod (2 ^ System.Platform.numBits)
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.ne_zero' : ∀ {p q r : NNReal}, p.HolderTriple q r → r ≠ 0
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the largest key.
 -/
Std.DTreeMap.maxKey : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → t.isEmpty = false → α
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s` is a subgroup of the additive group `α`, and `t` is a subset of `α ⧸ s`, then
there is a (typically non-canonical) bijection between the preimage of `t` in `α` and the product
`s × t`.  -/
QuotientAddGroup.preimageMkEquivAddSubgroupProdSet : {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → (t : Set (α ⧸ s)) → ↑(QuotientAddGroup.mk ⁻¹' t) ≃ ↥s × ↑t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldl_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldl f init t = Array.foldl (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.whiskerRight_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C) {H I : CategoryTheory.Grp C} (f : H ⟶ I),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f).hom.hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.X f.hom.hom
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.gcdCoeffs.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → ℤ → Sort u_1) (k k_1 : ℤ)
  (h_1 : (k k_2 : ℤ) → motive (Int.Internal.Linear.Poly.num k) k_2)
  (h_2 :
    (k' : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → (k : ℤ) → motive (Int.Internal.Linear.Poly.add k' v p) k),
  (match Int.Internal.Linear.Poly.num k, k_1 with
    | Int.Internal.Linear.Poly.num k, k_2 => h_1 k k_2
    | Int.Internal.Linear.Poly.add k' v p, k => h_2 k' v p k) =
    h_1 k k_1
-- Mathlib.Order.WellFoundedSet
Set.isWF_insert : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α}, (insert a s).IsWF ↔ s.IsWF
-- Mathlib.Algebra.GroupWithZero.Associated
associated_one_of_associated_mul_one : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, Associated (a * b) 1 → Associated a 1
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.isPartial_sSupFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} [IsOrderedAddMonoid R]
  {c : Set (HahnEmbedding.Partial seed)},
  c.Nonempty →
    ∀ (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c), HahnEmbedding.IsPartial seed (HahnEmbedding.Partial.sSupFun hc)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsAccessibleCategory.exists_cardinal : ∀ (C : Type u) [hC : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.IsAccessibleCategory.{w, v, u} C],
  ∃ κ, ∃ (x : Fact κ.IsRegular), CategoryTheory.IsCardinalAccessibleCategory C κ
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_pow_iff : ∀ {n k : ℕ}, n ≠ 1 → k ≠ 0 → (Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1)
-- Mathlib.Algebra.Group.Shrink
Shrink.instDiv.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Div α], Shrink.instDiv = (equivShrink α).symm.div
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.IsAnisotropic.corootForm_coroot_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : Fintype ι} {inst_1 : AddCommGroup M}
  {inst_2 : AddCommGroup N} {inst_3 : CommRing R} {inst_4 : Module R M} {inst_5 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsAnisotropic] (i : ι), (P.CorootForm (P.coroot i)) (P.coroot i) ≠ 0
-- Init.Omega.LinearCombo
/-- Coefficients of the atoms.  -/
Lean.Omega.LinearCombo.coeffs : Lean.Omega.LinearCombo → Lean.Omega.Coeffs
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_eq_top_iff : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.center G = ⊤ ↔ IsAddCommutative G
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalDistrib.toIsMonoidalLeftDistrib : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalDistrib C],
  CategoryTheory.IsMonoidalLeftDistrib C
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.mul : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f →
    AkraBazziRecurrence.GrowsPolynomially g → AkraBazziRecurrence.GrowsPolynomially fun x => f x * g x
-- Mathlib.Data.Fintype.Basic
Fintype.univ_empty : Finset.univ = ∅
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_1.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVBinPred → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinPred.eq)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinPred.ult),
  (match Std.Tactic.BVDecide.BVBinPred.eq with
    | Std.Tactic.BVDecide.BVBinPred.eq => h_1 ()
    | Std.Tactic.BVDecide.BVBinPred.ult => h_2 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Help typeclass inference to infer preservation of finite limits for the forgetful functor.  -/
CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetFunObjFinite : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget FintypeCat)
-- Mathlib.Topology.ClusterPt
ClusterPt.neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F → (nhds x ⊓ F).NeBot
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- `CliffordAlgebra.involute` as an `AlgEquiv`.  -/
CliffordAlgebra.involuteEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra Q
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_lt_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] {a b c d : α}, a < b * c → c ≤ d → a < b * d
-- Mathlib.Topology.Category.Stonean.Adjunctions
/-- The forgetful functor from Stonean spaces, being a right adjoint, preserves limits.  -/
Stonean.forget.preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget Stonean)
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_univ_iff : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → Set α}, ⋃ i, f i = Set.univ ↔ ∀ (x : α), ∃ i, x ∈ f i
-- Init.Data.UInt.Lemmas
UInt32.toUSize_neg : ∀ (a : UInt32), (-a).toUSize = -a.toUSize % 4294967296
-- Lean.Environment
/-- Plumbing function for `Lean.Meta.realizeConst`; see documentation there.  -/
Lean.Environment.realizeConst : Lean.Environment →
  Lean.Name →
    Lean.Name →
      (Lean.Environment → Lean.Options → BaseIO (Lean.Environment × Dynamic)) →
        IO (Lean.Environment × Task (Option Lean.Kernel.Exception) × Dynamic)
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.leftOp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor D Cᵒᵖ} (a : F ⊣ G.leftOp),
  a.leftOp.unit = CategoryTheory.NatTrans.unop a.counit
-- Mathlib.Algebra.Group.Conj
/-- Certain instances trigger further searches when they are considered as candidate instances;
these instances should be assigned a priority lower than the default of 1000 (for example, 900).

The conditions for this rule are as follows:
* a class `C` has instances `instT : C T` and `instT' : C T'`;
* types `T` and `T'` are both reducible specializations of another type `S`;
* the parameters supplied to `S` to produce `T` are not (fully) determined by `instT`,
  instead they have to be found by instance search.

If those conditions hold, the instance `instT` should be assigned lower priority.

Note that there is no issue unless `T` and `T'` are reducibly equal to `S`, Otherwise the instance
discrimination tree can distinguish them, and the note does not apply.

If the type involved is a free variable (rather than an instantiation of some type `S`),
the instance priority should be even lower, see Note [lower instance priority].
 -/
LibraryNote.«slow-failing_instance_priority» : Batteries.Util.LibraryNote
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.eq_mul_inv : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (v : ℚ) (n : ℤ) (d : ℕ),
  (v.num == n && v.den == d) = true → a = Lean.Grind.Field.NormNum.ofRat v → a = IntCast.intCast n * (↑d)⁻¹
-- Mathlib.Algebra.Group.Action.Prod
Prod.smulCommClassBoth : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul N] [inst_1 : Mul P] [inst_2 : SMul M N] [inst_3 : SMul M P]
  [SMulCommClass M N N] [SMulCommClass M P P], SMulCommClass M (N × P) (N × P)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.apply_eq_pow_smul_coeff : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} {z : 𝕜}, ((p n) fun x => z) = z ^ n • p.coeff n
-- Init.Data.UInt.Lemmas
USize.div_zero : ∀ {a : USize}, a / 0 = 0
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_zero_eq_top_iff : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.upperCentralSeries G 1 = ⊤ ↔ IsAddCommutative G
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Coercion to function as an additive monoid homomorphism.  -/
MeasureTheory.Measure.coeAddHom : {α : Type u_1} → {x : MeasurableSpace α} → MeasureTheory.Measure α →+ Set α → ENNReal
-- Lean.Meta.Basic
/-- A predicate to control whether a constant can be unfolded or not at `whnf`.
Note that we do not cache results at `whnf` when `canUnfold?` is not `none`.  -/
Lean.Meta.Context.canUnfold? : Lean.Meta.Context → Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.Fork.IsWeakLimit.mk_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y}
  (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt)
  (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι)
  (s : CategoryTheory.Limits.Fork f g), (CategoryTheory.Limits.Fork.IsWeakLimit.mk t lift fac).lift s = lift s
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofBitVec : ∀ (n : BitVec 16), { toBitVec := n }.toBitVec = n
-- Mathlib.Topology.NhdsWithin
mem_closure_pi : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)}
  {x : (i : ι) → α i}, x ∈ closure (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure (s i)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_image_homothety : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (x : E) (r : ℝ) (s : Set E),
  μ (⇑(AffineMap.homothety x r) '' s) = ENNReal.ofReal |r ^ Module.finrank ℝ E| * μ s
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.mpr : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n}, T.Iff φ ψ → T.Imp ψ φ
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charAlgHom.eq_1 : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (hL : Continuous fun p => (L p.1) p.2),
  BoundedContinuousFunction.charAlgHom he hL =
    (AddMonoidAlgebra.lift ℂ (BoundedContinuousFunction V ℂ) W) (BoundedContinuousFunction.charMonoidHom he hL)
-- Mathlib.GroupTheory.Commutator.Finite
instFiniteElemProdCommutatorRepresentatives : ∀ {G : Type u_1} [inst : Group G] [Finite ↑(commutatorSet G)], Finite ↑(commutatorRepresentatives G)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_smul_of_nullMeasurableSet : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : SMul G α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (c : G), μ ((fun x => c • x) ⁻¹' s) = μ s
-- Init.Data.Queue
/-- `O(1)`. Is the queue empty?  -/
Std.Queue.isEmpty : {α : Type u} → Std.Queue α → Bool
-- Mathlib.Data.Fintype.EquivFin
Function.Embedding.nonempty_iff_card_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β],
  Nonempty (α ↪ β) ↔ Fintype.card α ≤ Fintype.card β
-- Batteries.Data.List.Count
List.leftInverse_idxToSigmaCount_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : List α},
  Function.LeftInverse xs.idxToSigmaCount xs.sigmaCountToIdx
-- Lean.Parser.Command
Lean.Parser.Command.meta.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.lift_restrict : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E), IntermediateField.lift (IntermediateField.restrict h) = F
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ι_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), CategoryTheory.CategoryStruct.comp h.ι h.g' = 0
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.extendFun.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain),
  f.extendFun hx = (↑f).supSpanSingleton x (f.eval x) hx
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.iteratedDeriv_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {N : ℕ∞} {n : ℕ},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun x => x ^ n • f x) MeasureTheory.volume) →
    ↑n ≤ N →
      iteratedDeriv n (FourierTransform.fourier f) =
        FourierTransform.fourier fun x => (-2 * ↑Real.pi * Complex.I * ↑x) ^ n • f x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_add_pow : ∀ {R : Type u} [inst : CommSemiring R] (n k : ℕ) (c : R),
  (⇑Polynomial.derivative)^[k] ((Polynomial.X + Polynomial.C c) ^ n) =
    n.descFactorial k • (Polynomial.X + Polynomial.C c) ^ (n - k)
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.expectedType? : Lean.Elab.TermInfo → Option Lean.Expr
-- Std.Sat.CNF.Basic
/-- Evaluating a `Clause` with respect to an assignment `a`.
 -/
Std.Sat.CNF.Clause.eval : {α : Type u_1} → (α → Bool) → Std.Sat.CNF.Clause α → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.boundary_ι_mem_I : ∀ (n : ℕ), SSet.modelCategoryQuillen.I (SSet.boundary n).ι
-- Mathlib.Data.List.Forall2
List.rel_flatten : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop},
  Relator.LiftFun (List.Forall₂ (List.Forall₂ R)) (List.Forall₂ R) List.flatten List.flatten
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectMonomorphisms.mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectMonomorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.Mono ((F i).map f)], CategoryTheory.Mono f
-- Mathlib.Topology.Algebra.FilterBasis
/-- The trivial additive group filter basis consists of `{0}` only. The associated
topology is discrete.  -/
AddGroupFilterBasis.instInhabited : {G : Type u} → [inst : AddGroup G] → Inhabited (AddGroupFilterBasis G)