mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Count
List.IsInfix.count_le : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α} (a : α), l₁ <:+: l₂ → List.count a l₁ ≤ List.count a l₂
-- Mathlib.Algebra.Star.Subsemiring
/-- A (unital) star subsemiring is a non-associative ring which is closed under the `star`
operation.  -/
StarSubsemiring : (R : Type v) → [NonAssocSemiring R] → [Star R] → Type v
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If every vector is a multiple of some `v : M`, then `M` has dimension at most one.  -/
finrank_le_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  (v : M), (∀ (w : M), ∃ c, c • v = w) → Module.finrank R M ≤ 1
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (i j : ι), (b.toDual (b i)) (b j) = if i = j then 1 else 0
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.continue.sizeOf_spec : ∀ {F : PFunctor.{uA, uB}}, sizeOf PFunctor.Approx.CofixA.continue = 1
-- Mathlib.Order.Filter.Pointwise
Filter.addRightMono : ∀ {α : Type u_2} [inst : Add α], AddRightMono (Filter α)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.instAdditiveTensorRight : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C),
  (CategoryTheory.MonoidalCategory.tensorRight X).Additive
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.smul_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_4} [inst_1 : SMul R Y] (r : R)
  (f : LocallyConstant X Y) (x : X), (r • f) x = r • f x
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcCallParams.fromJson : Lean.Json → Except String Lean.Lsp.RpcCallParams
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- The forgetful braided functor from a full braided subcategory into the original category
("forgetting" the condition).
 -/
CategoryTheory.ObjectProperty.instBraidedFullSubcategoryι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) →
        [inst_2 : P.IsMonoidal] → [inst_3 : CategoryTheory.BraidedCategory C] → P.ι.Braided
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Icc_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic a ∪ Set.Icc a b = Set.Iic b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mem_cycles₁_of_mem_boundaries₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G},
  ∀ f ∈ groupHomology.boundaries₁ A, f ∈ groupHomology.cycles₁ A
-- Mathlib.Algebra.Star.SelfAdjoint
/-- Functions in a `StarHomClass` preserve self-adjoint elements.  -/
IsSelfAdjoint.map : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Star R] [inst_1 : Star S] [inst_2 : FunLike F R S]
  [StarHomClass F R S] {x : R}, IsSelfAdjoint x → ∀ (f : F), IsSelfAdjoint (f x)
-- Init.Data.Array.Attach
Array.attach_push : ∀ {α : Type u_1} {a : α} {xs : Array α},
  (xs.push a).attach =
    (Array.map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          xs.attach).push
      ⟨a, ⋯⟩
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.toSubsemigroup_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], Monotone NonUnitalSubsemiring.toSubsemigroup
-- Mathlib.Topology.Homotopy.Lifting
ContinuousMap.mk.hcongr_6 : ∀ (X X' : Type u_1),
  X = X' →
    ∀ (Y Y' : Type u_2),
      Y = Y' →
        ∀ (inst : TopologicalSpace X) (inst' : TopologicalSpace X'),
          inst ≍ inst' →
            ∀ (inst_1 : TopologicalSpace Y) (inst'_1 : TopologicalSpace Y'),
              inst_1 ≍ inst'_1 →
                ∀ (toFun : X → Y) (toFun' : X' → Y'),
                  toFun ≍ toFun' →
                    ∀ (continuous_toFun : Continuous toFun) (continuous_toFun' : Continuous toFun'),
                      continuous_toFun ≍ continuous_toFun' →
                        { toFun := toFun, continuous_toFun := continuous_toFun } ≍
                          { toFun := toFun', continuous_toFun := continuous_toFun' }
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- If `S` is an `R`-algebra and `p` a prime of `S`, we say that `S` is `R`-quasi-finite at `p`
if `Sₚ` is `R`-quasi-finite. In the case where `S` is (essentially) of finite type over `R`,
this is equivalent to the usual definition that `p` is isolated in its fiber.
See `Ideal.exists_notMem_forall_mem_of_ne_of_liesOver`.  -/
Algebra.QuasiFiniteAt : (R : Type u_1) →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → (p : Ideal S) → [p.IsPrime] → Prop
-- Mathlib.Data.Subtype
Subtype.val_inj : ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.TreeMap.getEntryLE? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option (α × β)
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_3.splitter : (motive : List String → List String → Sort u_1) →
  (x x_1 : List String) →
    (Unit → motive [] []) →
      ((x : String) → (s : List String) → motive [] (x :: s)) →
        ((pre : String) → (l s' : List String) → motive (pre :: l) s') → motive x x_1
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanDeclIdent : Lean.ToJson Lean.Lsp.LeanDeclIdent
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.isRed.eq_1 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).isRed = c
-- Mathlib.RingTheory.Localization.Module
Module.Basis.localizationLocalization_apply : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {A : Type u_3} [inst_4 : CommSemiring A] [inst_5 : Algebra R A]
  (Aₛ : Type u_4) [inst_6 : CommSemiring Aₛ] [inst_7 : Algebra A Aₛ] [inst_8 : Algebra Rₛ Aₛ] [inst_9 : Algebra R Aₛ]
  [inst_10 : IsScalarTower R Rₛ Aₛ] [inst_11 : IsScalarTower R A Aₛ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Module.Basis ι R A) (i : ι),
  (Module.Basis.localizationLocalization Rₛ S Aₛ b) i = (algebraMap A Aₛ) (b i)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
MeasureTheory.Measure.toPMF_apply : ∀ {α : Type u_1} [inst : Countable α] [inst_1 : MeasurableSpace α] [inst_2 : MeasurableSingletonClass α]
  (μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsProbabilityMeasure μ] (x : α), μ.toPMF x = μ {x}
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} →
        (obj : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X)) →
          (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj X ≤ Submodule.comap (M.restrictₛₗ f) (obj Y)) → M.Submodule
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.is_const_of_fderiv_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E},
  IsOpen s →
    IsPreconnected s → DifferentiableOn 𝕜 f s → Set.EqOn (fderiv 𝕜 f) 0 s → ∀ {x y : E}, x ∈ s → y ∈ s → f x = f y
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.memLp_lineDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E},
  LipschitzWith C f → ∀ (v : E), MeasureTheory.MemLp (fun x => lineDeriv ℝ f x v) ⊤ μ
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsFinitelySemisimple → ∀ (μ : R) {k : ℕ∞}, 0 < k → (f.genEigenspace μ) k = f.eigenspace μ
-- Mathlib.Order.Hom.Basic
OrderIso.orderIsoCongr_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ≃o γ) (g : β ≃o δ) (h : γ ≃o δ), (f.orderIsoCongr g).symm h = (f.trans h).trans g.symm
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_snd : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.snd R M M₂).ker = (LinearMap.inl R M M₂).range
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- Contracting the closure of a set is the same as contracting the set,
and then deleting the rest of its elements.  -/
Matroid.contract_closure_eq_contract_delete : ∀ {α : Type u_1} (M : Matroid α) (C : Set α), M.contract (M.closure C) = (M.contract C).delete (M.closure C \ C)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- **Alias** of the reverse direction of `Matrix.nondegenerate_transpose_iff`. -/
Matrix.Nondegenerate.transpose : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.Nondegenerate → M.transpose.Nondegenerate
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Group isomorphism between `SkewMonoidAlgebra k G` and `G →₀ k`.  -/
SkewMonoidAlgebra.coeffAddEquiv : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → SkewMonoidAlgebra k G ≃+ (G →₀ k)
-- Mathlib.Topology.Separation.Hausdorff
/-- The largest T2 quotient of a topological space is indeed T2.  -/
T2Quotient.instT2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space (T2Quotient X)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_id : ∀ (α : Type u_5) [inst : NonUnitalNonAssocSemiring α], ⇑(CentroidHom.id α) = id
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_assoc_flip_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [inst_2 : CategoryTheory.ComonObj X] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul X) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.comul)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).inv h))
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.mk_add_mk : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.Ring.OfSemiring.Q.mk (a₁, a₂) + Lean.Grind.Ring.OfSemiring.Q.mk (b₁, b₂) =
    Lean.Grind.Ring.OfSemiring.Q.mk (a₁ + b₁, a₂ + b₂)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} →
          (n : ℕ) →
            aig.RefVec w → aig.RefVec n → ℕ → Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w
-- Mathlib.Algebra.Category.ModuleCat.Descent
ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat : ∀ {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.Flat →
    CategoryTheory.Limits.PreservesFiniteLimits
      (CategoryTheory.MonoidalCategory.tensorLeft ((ModuleCat.restrictScalars f).obj (ModuleCat.of B B)))
-- Init.Data.Slice.Lemmas
Std.Slice.foldl_toList : ∀ {γ : Type u} {α β : Type v} {δ : Type u_1} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [Std.Iterators.Finite α Id] {s : Std.Slice γ}
  {init : δ} {f : δ → β → δ}, List.foldl f init s.toList = Std.Slice.foldl f init s
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The comultiplication morphism of a comonoid object.  -/
CategoryTheory.ComonObj.termΔ : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.contains.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.contains a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => false
    | Std.DHashMap.Internal.AssocList.cons k value l => k == a || Std.DHashMap.Internal.AssocList.contains a l
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyGT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option α
-- Mathlib.Topology.Compactness.Compact
isCompact_univ_iff : ∀ {X : Type u} [inst : TopologicalSpace X], IsCompact Set.univ ↔ CompactSpace X
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldl_mul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (a b : CliffordAlgebra Q),
  ((CliffordAlgebra.foldl Q f hf) n) (a * b) = ((CliffordAlgebra.foldl Q f hf) (((CliffordAlgebra.foldl Q f hf) n) a)) b
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsSelfAdjoint.norm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsSelfAdjoint a → IsSelfAdjoint b → a * b = 0 → ‖a + b‖ = max ‖a‖ ‖b‖
-- Mathlib.SetTheory.ZFC.VonNeumann
Ordinal.card_le_card_vonNeumann : ∀ (o : Ordinal.{u_1}), o.card ≤ (ZFSet.vonNeumann o).card
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.arrayEnd : Lean.Json.CompressWorkItemKind✝
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.HasProjectiveDimensionLT X 0
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.IterM.toArray_toIter : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.IterM Id β},
  it.toIter.toArray = it.toArray.run
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit.app (HomotopicalAlgebra.CofibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.CofibrantObject.toHoCat.map X.iBifibrantResolutionObj
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.step_toTake : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toTake.step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield it'.toTake out ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip it'.toTake ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.TreeMap.filter f t)[k]? = t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
EisensteinSeries.gammaSetDivGcdEquiv.congr_simp : ∀ (r : ℕ) [inst : NeZero r], EisensteinSeries.gammaSetDivGcdEquiv r = EisensteinSeries.gammaSetDivGcdEquiv r
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_intCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : IntCast F] (z : ℤ), HasDerivAt (↑z) 0 x
-- Mathlib.Analysis.Complex.JensenFormula
/-- Let `D : ℂ → ℤ` be a function with locally finite support within the closed ball with center `c` and
radius `R`, such as the zero- and pole divisor of a meromorphic function.  Then, the circle average
of the function `∑ᶠ u, (D u * log ‖· - u‖)` over the boundary of the ball equals
`∑ᶠ u, D u * log R`.
 -/
circleAverage_log_norm_factorizedRational : ∀ {R : ℝ} {c : ℂ} (D : Function.locallyFinsuppWithin (Metric.closedBall c |R|) ℤ),
  Real.circleAverage (∑ᶠ (u : ℂ), fun x => ↑(D u) * Real.log ‖x - u‖) c R = ∑ᶠ (u : ℂ), ↑(D u) * Real.log R
-- Mathlib.Topology.LocallyFinite
LocallyFinite.of_comp_surjective : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {g : ι' → ι},
  Function.Surjective g → LocallyFinite (f ∘ g) → LocallyFinite f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Equivalent monoids have additively isomorphic monoid algebras.

`MonoidAlgebra.mapDomain` as an `AddEquiv`.  -/
MonoidAlgebra.mapDomainAddEquiv : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → [inst_1 : Mul M] → [inst_2 : Mul N] → M ≃ N → MonoidAlgebra R M ≃+ MonoidAlgebra R N
-- Init.Data.Iterators.Basic
/-- The output value could plausibly be emitted in the next step.  -/
Std.IterM.IsPlausibleIndirectOutput.direct : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it : Std.IterM m β} {out : β},
  it.IsPlausibleOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictMono_tendsto' : ∀ {α : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [DenselyOrdered α] [OrderTopology α]
  [FirstCountableTopology α] {x y : α},
  y < x → ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k fallback : α},
  m.contains k = true → m.getKeyD k fallback = k
-- Mathlib.NumberTheory.NumberField.ClassNumber
RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  ↑|NumberField.discr K| <
      (2 * (Real.pi / 4) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K).factorial)) ^
        2 →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.Topology.MetricSpace.Bounded
/-- Given a point, a bounded subset is included in some ball around this point  -/
Metric.isBounded_iff_subset_closedBall : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] (c : α), Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.closedBall c r
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.add.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : Lean.Syntax), sizeOf (Simps.ProjectionRule.add a a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, (Std.TreeSet.ofList l cmp).size ≤ l.length
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.pi_div_four_le_arcsin : ∀ {x : ℝ}, Real.pi / 4 ≤ Real.arcsin x ↔ √2 / 2 ≤ x
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.Integrable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_apply_zero : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
      Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
        UpperHalfPlane.cuspFunction h f 0 = UpperHalfPlane.valueAtInfty f
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.unop_sub : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : Cᵒᵖ}
  (f g : X ⟶ Y), (f - g).unop = f.unop - g.unop
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iic_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (S : Set α), LowerSet.Iic (sInf S) = ⨅ a ∈ S, LowerSet.Iic a
-- Mathlib.Topology.Neighborhoods
/-- A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`.  -/
isOpen_iff_eventually : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Localizing away from powers of `f` homogeneously.  -/
HomogeneousLocalization.Away : {ι : Type u_1} → {A : Type u_2} → {σ : Type u_3} → [CommRing A] → [SetLike σ A] → (ι → σ) → A → Type (max u_1 u_2)
-- Mathlib.Order.Irreducible
InfPrime.ne_top : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α} [inst_1 : OrderTop α], InfPrime a → a ≠ ⊤
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (v : β k) (ht : t.Balanced),
  t.getThenInsertIfNew? k v ht =
    match t.get? k with
    | none => (none, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ht).impl)
    | some b => (some b, t)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instArray : {α : Type} → [Lean.Elab.ConfigEval.EvalTerm α] → Lean.Elab.ConfigEval.EvalTerm (Array α)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_left_injective : ∀ {R : Type u} [inst : CommSemiring R] [IsDomain R] {x : R}, x ≠ 0 → Function.Injective fun I => I * Ideal.span {x}