mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (t : Std.DTreeMap.Internal.Impl α β) → k ∈ t → Sort u_3) →
          (t : Std.DTreeMap.Internal.Impl α β) →
            (hlk : k ∈ t) →
              ((size : ℕ) →
                  (k' : α) →
                    (v' : β k') →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (hlk : k ∈ Std.DTreeMap.Internal.Impl.inner size k' v' l r) →
                          motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) hlk) →
                motive t hlk
-- Mathlib.Order.LiminfLimsup
limsup_finset_sup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLinearOrder β] [inst_1 : OrderBot β]
  {f : Filter α} {F : ι → α → β} {s : Finset ι},
  autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) limsup_finset_sup._auto_1 →
    autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) limsup_finset_sup._auto_3 →
      Filter.limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => Filter.limsup (F i) f
-- Lean.Attributes
Lean.instInhabitedAttributeKind.default : Lean.AttributeKind
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul_left_eq_one : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  (r : R) (x : TrivSqZeroExt R M),
  r * x.fst = 1 → (TrivSqZeroExt.inl r + TrivSqZeroExt.inr (-(MulOpposite.op r • r • x.snd))) * x = 1
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The projection from `CostructuredArrow K B` to `C` creates any connected limit.  -/
CategoryTheory.CostructuredArrow.instCreatesLimitsOfShapeProjOfIsConnected : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Functor C D} →
              [CategoryTheory.IsConnected J] →
                {B : D} → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.CostructuredArrow.proj K B)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.Fan.IsLimit.lift`.

---

Constructor for morphisms to the point of a limit fan.  -/
CategoryTheory.Limits.Fan.IsLimit.desc : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : β → C} →
        {c : CategoryTheory.Limits.Fan F} → CategoryTheory.Limits.IsLimit c → {A : C} → ((i : β) → A ⟶ F i) → (A ⟶ c.pt)
-- Init.Data.String.Basic
String.Pos.offset_toSlice : ∀ {s : String} {pos : s.Pos}, pos.toSlice.offset = pos.offset
-- Mathlib.Topology.NhdsKer
nhdsKer_sInter_subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set (Set X)}, nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.mul₀` -/
TendstoLocallyUniformlyOn.fun_mul₀ : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {s : Set X} {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s →
        ContinuousOn g s → TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l s
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N], Function.Surjective ⇑Monoid.Coprod.mk
-- Init.Grind.Module.Basic
Lean.Grind.AddCommMonoid.zero_add : ∀ {M : Type u} [inst : Lean.Grind.AddCommMonoid M] (a : M), 0 + a = a
-- Mathlib.Order.Interval.Set.Monotone
monotone_Iic : ∀ {α : Type u_1} [inst : Preorder α], Monotone Set.Iic
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.List.NodupKeys.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : List (Sigma β)), l.NodupKeys = l.keys.Nodup
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.addBuiltinHandler : Lean.Name → Lean.Linter.MissingDocs.Handler → IO Unit
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {g : β → γ}, IsUniformInducing g → ∀ {f : α → β}, IsUniformInducing f → IsUniformInducing (g ∘ f)
-- Mathlib.Data.Finset.Range
Multiset.toFinset_range : ∀ (n : ℕ), (Multiset.range n).toFinset = Finset.range n
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.add : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x y : WittVector p R),
  WittVector.mapFun (⇑f) (x + y) = WittVector.mapFun (⇑f) x + WittVector.mapFun (⇑f) y
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instTop : {R : Type u} → {M : Type v} → [inst : SMul R M] → Top (SubMulAction R M)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
eq_or_eq_inv_of_mabs_eq : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a b : α}, |a|ₘ = b → a = b ∨ a = b⁻¹
-- Mathlib.Data.Finset.NatDivisors
Multiset.nat_divisors_prod : ∀ (s : Multiset ℕ), s.prod.divisors = (Multiset.map Nat.divisors s).prod
-- Mathlib.Data.Part
Part.getOrElse_some : ∀ {α : Type u_1} (a d : α) [inst : Decidable (Part.some a).Dom], (Part.some a).getOrElse d = a
-- Mathlib.Data.Rat.Floor
/-- `norm_num` extension for `round`  -/
Rat.evalRound : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a b : α}, a < b → frontier (Set.Ico a b) = {a, b}
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.of.eq_1 : ∀ (M : Type u) [inst : AddCommMonoid M], AddCommMonCat.of M = { carrier := M, str := inst }
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- Whiskering right and then taking a colimit is the same as taking the colimit and applying the
functor.  -/
CategoryTheory.colimitCompWhiskeringRightIsoColimitComp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {E : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {J : Type u_4} →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D] →
                  (F : CategoryTheory.Functor D E) →
                    [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F] →
                      (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) →
                        CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ≅
                          (CategoryTheory.Limits.colimit G).comp F
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.Small.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  {E : J.ZeroHypercover S}, (∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S) → E.Small
-- Mathlib.RepresentationTheory.Basic
/-- The trivial representation of `G` on a `k`-module V.
 -/
Representation.trivial : (k : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) →
      [inst : Semiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V
-- Mathlib.Data.Bool.Basic
Bool.coe_sort_true : (true = true) = True
-- Mathlib.Topology.Order.Monotone
/-- A monotone continuous function is right-continuous in the order-theoretic sense.  -/
Continuous.rightOrdContinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β],
  Continuous f → Monotone f → RightOrdContinuous f
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.isStronglyConnected_iff : ∀ (V : Type u_2) [inst : Quiver V], Quiver.IsStronglyConnected V ↔ ∀ (i j : V), Nonempty (Quiver.Path i j)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.aeval_val_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) (i : σ), (MvPolynomial.aeval P.val) (P.relation i) = 0
-- Mathlib.RingTheory.AdjoinRoot
PowerBasis.quotientEquivQuotientMinpolyMap.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (I : Ideal R),
  pb.quotientEquivQuotientMinpolyMap I =
    (AlgEquiv.ofRingEquiv ⋯).trans (AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.differentiable_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 1 f → Differentiable 𝕜 f
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.triangleRemovalBound_mul_cube_lt : ∀ {ε : ℝ}, 0 < ε → SimpleGraph.triangleRemovalBound ε * ↑⌈4 / ε⌉₊ ^ 3 < 1
-- Mathlib.CategoryTheory.Comma.LocallySmall
CategoryTheory.StructuredArrow.locallySmall : ∀ {B : Type u₂} {T : Type u₃} [inst : CategoryTheory.Category.{v₂, u₂} B] [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  (S : T) (T_1 : CategoryTheory.Functor B T) [CategoryTheory.LocallySmall.{w, v₂, u₂} B],
  CategoryTheory.LocallySmall.{w, v₂, max u₂ v₃} (CategoryTheory.StructuredArrow S T_1)
-- Lean.Util.Trace
/-- A version of `Lean.withTraceNode` which allows generating the message within the computation.  -/
Lean.withTraceNode' : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        [Lean.MonadRef m] →
          [Lean.AddMessageContext m] →
            [Lean.MonadOptions m] →
              [Lean.MonadAlwaysExcept Lean.Exception m] →
                [MonadLiftT BaseIO m] →
                  Lean.Name → m (α × Lean.MessageData) → optParam Bool true → optParam String "" → m α
-- Mathlib.MeasureTheory.Measure.Regular
/-- **Alias** of `MeasurableSet.exists_isClosed_sdiff_lt`. -/
MeasurableSet.exists_isClosed_diff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [OpensMeasurableSpace α] [μ.WeaklyRegular] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.color_classes_independent : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (c : α), IsAntichain G.Adj (C.colorClass c)
-- Mathlib.Data.Vector3
/-- `VectorAllP p v` is equivalent to `∀ i, p (v i)`, but unfolds directly to a conjunction,
i.e. `VectorAllP p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`.  -/
VectorAllP : {α : Type u_1} → {n : ℕ} → (α → Prop) → Vector3 α n → Prop
-- Mathlib.Topology.Category.TopCat.OpenNhds
IsOpenMap.functorNhds_map : ∀ {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X)
  {X_1 Y_1 : TopologicalSpace.OpenNhds x} (i : X_1 ⟶ Y_1), (h.functorNhds x).map i = h.functor.map i
-- Mathlib.Algebra.Ring.Submonoid.Basic
/-- The product of an element of `S` and an element of the additive closure of a multiplicative
submonoid `S` is contained in the additive closure of `S`.  -/
MulMemClass.mul_left_mem_add_closure : ∀ {M : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R] [MulMemClass M R] {S : M}
  {a b : R}, a ∈ S → b ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_le_encard_sdiff_add_encard`. -/
Set.encard_le_encard_diff_add_encard : ∀ {α : Type u_1} (s t : Set α), s.encard ≤ (s \ t).encard + t.encard
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_ofFin : ∀ (n : Fin (2 ^ 8)), { toBitVec := { toFin := n } } = UInt8.ofFin n
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_T_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : MulActionWithZero R S]
  [inst_3 : Monoid S] (n : ℤ) (x : Sˣ), (LaurentPolynomial.T n).smeval x = ↑(x ^ n)
-- Mathlib.Data.SetLike.Basic
/-- Note: implementers of `SetLike` must copy this lemma in order to tag it with `@[ext]`.  -/
SetLike.ext : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (∀ (x : B), x ∈ p ↔ x ∈ q) → p = q
-- Lean.Parser.Term
Lean.Parser.Term.binop_lazy.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Sym.Card
/-- The `diag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s`.  -/
Sym2.card_image_diag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), (Finset.image (Function.uncurry Sym2.mk) s.diag).card = s.card
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_inl_inl : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₁)
  (b : β₁), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inl b) = Finset.map Function.Embedding.inl (f₁ a b)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldl_toArray : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Std.Iter β},
  Array.foldl f init it.toArray = Std.Iter.fold f init it
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Iic : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrderBot α] (a : α), (Set.Iic a).Finite
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_def : ∀ {R : Type u_3} {A : Type u_4} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfcₙ f a =
    if h : p a ∧ ContinuousOn f (quasispectrum R a) ∧ f 0 = 0 then
      (cfcₙHom ⋯) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.isClopen : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), IsClopen ↑s
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  LeftOrdContinuous f → ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y
-- Lean.MetavarContext
/-- Low level API for adding/declaring metavariable declarations.
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique".  -/
Lean.MetavarContext.addExprMVarDecl : Lean.MetavarContext →
  Lean.MVarId →
    Lean.Name →
      Lean.LocalContext →
        Lean.LocalInstances →
          Lean.Expr → optParam Lean.MetavarKind Lean.MetavarKind.natural → optParam ℕ 0 → Lean.MetavarContext
-- Mathlib.MeasureTheory.Group.Integral
/-- Translating a function by left-multiplication does not change its integral with respect to a
left-invariant measure.  -/
MeasureTheory.integral_mul_left_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure G} [inst_3 : Group G] [MeasurableMul G] [μ.IsMulLeftInvariant] (f : G → E) (g : G),
  ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
-- Lean.Util.HasConstCache
Lean.HasConstCache.mk : {declNames : Array Lean.Name} → Std.HashMap.Raw Lean.Expr Bool → Lean.HasConstCache declNames
-- Init.Data.Nat.Lemmas
Nat.sub_max_sub_left : ∀ (a b c : ℕ), max (a - b) (a - c) = a - min b c
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_eq : ∀ (a b : UInt64), a.toUInt8 = b.toUInt8 ↔ a % 256 = b % 256
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_maxKey!_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (Std.DTreeMap.Internal.Impl.Const.modify k f t).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.CategoryTheory.Center.Linear
CategoryTheory.Linear.smulOfRingMorphism_smul_eq : ∀ {R : Type w} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] (φ : R →+* CategoryTheory.CatCenter C) {X Y : C} (a : R) (f : X ⟶ Y),
  a • f = CategoryTheory.CategoryStruct.comp ((φ a).app X) f
-- Mathlib.Algebra.Category.MonCat.Shrink
/-- A functor `F : C ⥤ MonCat.{w'}` factors through `MonCat.{w}` if all the
monoids are `w`-small.  -/
MonCat.shrinkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C MonCat) → [∀ (X : C), Small.{w, w'} ↑(F.obj X)] → CategoryTheory.Functor C MonCat
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {k : α}, Std.HashMap.unitOfList [k] = ∅.insertIfNew k ()
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedDep.mk.sizeOf_spec : ∀ (name : Lean.Name) (ident : Lean.TSyntax `ident) (binderType : Lean.TSyntax `term) (isClass : Bool),
  sizeOf { name := name, ident := ident, binderType := binderType, isClass := isClass } =
    1 + sizeOf name + sizeOf ident + sizeOf binderType + sizeOf isClass
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.instOrdRwKey : Ord Mathlib.Tactic.ClickSuggestions.RwKey
-- Init.Data.Subtype.Basic
Subtype.exists : ∀ {α : Sort u} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) ↔ ∃ a, ∃ (b : p a), q ⟨a, b⟩
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioi_comp_mul_left_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℝ → E) (c : ℝ) {a : ℝ},
  0 < a →
    (MeasureTheory.IntegrableOn (fun x => f (a * x)) (Set.Ioi c) MeasureTheory.volume ↔
      MeasureTheory.IntegrableOn f (Set.Ioi (a * c)) MeasureTheory.volume)
-- Init.Data.Rat.Lemmas
Rat.add_neg_cancel : ∀ (a : ℚ), a + -a = 0
-- Mathlib.Analysis.Fourier.Inversion
Real.tendsto_integral_gaussian_smul' : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    ∀ {v : V},
      ContinuousAt f v →
        Filter.Tendsto
          (fun c =>
            ∫ (w : V),
              ((↑Real.pi * ↑c) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w)
          Filter.atTop (nhds (f v))
-- Std.Time.Duration
Std.Time.Duration.mk.inj : ∀ {second : Std.Time.Second.Offset} {nano : Std.Time.Nanosecond.Span}
  {proof : second.val ≥ 0 ∧ ↑nano ≥ 0 ∨ second.val ≤ 0 ∧ ↑nano ≤ 0} {second_1 : Std.Time.Second.Offset}
  {nano_1 : Std.Time.Nanosecond.Span} {proof_1 : second_1.val ≥ 0 ∧ ↑nano_1 ≥ 0 ∨ second_1.val ≤ 0 ∧ ↑nano_1 ≤ 0},
  { second := second, nano := nano, proof := proof } = { second := second_1, nano := nano_1, proof := proof_1 } →
    second = second_1 ∧ nano = nano_1
-- Init.Data.Range.Polymorphic.PRange
/-- For every pair of elements `init` and `hi`, there exists a chain of successors that
  results in an element that either has no successors or is greater than `hi`.
   -/
Std.Rxo.IsAlwaysFinite.finite : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : LT α} [self : Std.Rxo.IsAlwaysFinite α] (init hi : α),
  ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x < hi
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.instAddAction : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → AddAction V (AffineBasis ι k P)
-- Mathlib.CategoryTheory.Localization.Preadditive
CategoryTheory.Localization.liftNatTrans_zero : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [inst_4 : CategoryTheory.Localization.Lifting L W F₁ F₁'] [inst_5 : CategoryTheory.Localization.Lifting L W F₂ F₂']
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms E], CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' 0 = 0
-- Mathlib.RingTheory.Ideal.Operations
/-- A variant of `Finsupp.linearCombination` that takes in vectors valued in `I`.  -/
Ideal.finsuppTotal : (ι : Type u_1) →
  (M : Type u_2) →
    [inst : AddCommGroup M] →
      {R : Type u_3} → [inst_1 : CommRing R] → [inst_2 : Module R M] → (I : Ideal R) → (ι → M) → (ι →₀ ↥I) →ₗ[R] M
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofIntTruncate : ∀ {n : ℤ}, Int64.minValue.toInt ≤ n → n ≤ Int64.maxValue.toInt → (Int64.ofIntClamp n).toBitVec = BitVec.ofInt 64 n
-- Mathlib.Topology.Bases
Topology.IsEmbedding.firstCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] [FirstCountableTopology β]
  {f : α → β}, Topology.IsEmbedding f → FirstCountableTopology α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : (a : α) × β a → Bool} {l : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getEntry? k (List.filter f l) = Option.filter f (Std.Internal.List.getEntry? k l)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.comp_lift_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (f : L →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p] (x : L), (PerfectRing.lift i (f.comp i) p) x = f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.dblXYZ P 1 = W'.dblY P
-- Mathlib.Algebra.Star.Pointwise
Set.Nonempty.star : ∀ {α : Type u_1} [inst : InvolutiveStar α] {s : Set α}, s.Nonempty → (star s).Nonempty
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseText : (Std.Time.Text → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_5 : Std.Rci.HasRcoIntersection ℕ
-- Init.Control.Lawful.Basic
LawfulApplicative.toLawfulFunctor : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f], LawfulFunctor f
-- Lean.Declaration
Lean.DefinitionVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (value : Lean.Expr) (hints : Lean.ReducibilityHints)
  (safety : Lean.DefinitionSafety) (all : List Lean.Name),
  sizeOf { toConstantVal := toConstantVal, value := value, hints := hints, safety := safety, all := all } =
    1 + sizeOf toConstantVal + sizeOf value + sizeOf hints + sizeOf safety + sizeOf all
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.le : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g