mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.toFun_eq_toNNReal_apply : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K : TopologicalSpace.Compacts G),
  μ.toFun K = (μ K).toNNReal
-- Mathlib.Data.PNat.Find
PNat.le_find_iff : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ+), n ≤ PNat.find h ↔ ∀ m < n, ¬p m
-- Init.Data.List.BasicAux
/-- Applies a function to each element of a list, returning the list of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new list if the result of each function call is
pointer-equal to its argument.

For verification purposes, `List.mapMono = List.map`.
 -/
List.mapMono : {α : Type u_1} → List α → (α → α) → List α
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.neg_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Neg (G i)] (f : (i : ι) → G i), -f = fun i => -f i
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- If `D` is an enriched ordinary category then `Dᵒᵖ` is an enriched ordinary category.  -/
CategoryTheory.EnrichedOrdinaryCategory.opposite : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      [CategoryTheory.BraidedCategory V] →
        {D : Type u} →
          [inst_3 : CategoryTheory.Category.{v, u} D] →
            [CategoryTheory.EnrichedOrdinaryCategory V D] → CategoryTheory.EnrichedOrdinaryCategory V Dᵒᵖ
-- Mathlib.Tactic.DefEqTransformations
/-- For the main goal, use `m` to transform the types of locations specified by `loc?`.
If `loc?` is none, then transforms the type of target. `m` is provided with an expression
with instantiated metavariables as well as, if the location is a local hypothesis, the fvar.

`m` *must* transform expressions to defeq expressions.
If `checkDefEq = true` (the default) then `runDefEqTactic` will throw an error
if the resulting expression is not definitionally equal to the original expression.  -/
Mathlib.Tactic.runDefEqTactic : (Option Lean.FVarId → Lean.Expr → Lean.MetaM Lean.Expr) →
  Option (Lean.TSyntax `Lean.Parser.Tactic.location) → String → optParam Bool true → Lean.Elab.Tactic.TacticM Unit
-- Std.Sync.Barrier
/-- Creates a new barrier that can block a given number of threads.
 -/
Std.Barrier.new : ℕ → BaseIO Std.Barrier
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.updateCell.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)) (sz : ℕ) (ky : α)
  (y : β ky) (l_2 r : Std.DTreeMap.Internal.Impl α β)
  (hl_2 : (Std.DTreeMap.Internal.Impl.inner sz ky y l_2 r).Balanced),
  Std.DTreeMap.Internal.Impl.updateCell k f (Std.DTreeMap.Internal.Impl.inner sz ky y l_2 r) hl_2 =
    match h : compare k ky with
    | Ordering.lt =>
      match Std.DTreeMap.Internal.Impl.updateCell k f l_2 ⋯ with
      | { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance ky y newL r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.eq =>
      match (f (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)).inner with
      | none => { impl := l_2.glue r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some ⟨ky', y'⟩ =>
        { impl := Std.DTreeMap.Internal.Impl.inner sz ky' y' l_2 r, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.gt =>
      match Std.DTreeMap.Internal.Impl.updateCell k f r ⋯ with
      | { impl := newR, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance ky y l_2 newR ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.toPartialOrderOfLEArgs : {α : Type u} → Std.Packages.LinearOrderOfLEArgs α → Std.Packages.PartialOrderOfLEArgs α
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
/-- The composition-product of a measure and a kernel.  -/
ProbabilityTheory.«term_⊗ₘ_» : Lean.TrailingParserDescr
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.getNumEqsFromDiscrInfos : Array Lean.Meta.Match.DiscrInfo → ℕ
-- Mathlib.AlgebraicGeometry.Restrict
/-- A variant where `r` is first mapped into `Γ(X, U)` before taking the basic open.  -/
AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen' : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ((↑U).basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) r)
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.mk.injEq : ∀ (response? : Option Lean.Json) (serialized : String) (isComplete : Bool) (response?_1 : Option Lean.Json)
  (serialized_1 : String) (isComplete_1 : Bool),
  ({ response? := response?, serialized := serialized, isComplete := isComplete } =
      { response? := response?_1, serialized := serialized_1, isComplete := isComplete_1 }) =
    (response? = response?_1 ∧ serialized = serialized_1 ∧ isComplete = isComplete_1)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk : ∀ {R : Type u} [inst : CommRing R] {I J : Ideal R} (h : I ≤ J),
  (↑(DoubleQuot.quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = DoubleQuot.quotQuotMk I J
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_inv_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.unmop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.unmop).inv
-- Init.Data.String.TakeDrop
/-- Returns a `String.Slice` that contains the first `n` characters \(Unicode code points\) of
`s`.

If `n` is greater than `s.toList.length`, returns `s.toSlice`.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

Examples:

* `"red green blue".take 3 == "red".toSlice`

* `"red green blue".take 1 == "r".toSlice`

* `"red green blue".take 0 == "".toSlice`

* `"red green blue".take 100 == "red green blue".toSlice`

* `"مرحبا بالعالم".take 5 == "مرحبا".toSlice`
 -/
String.take : String → ℕ → String.Slice
-- Init.Data.String.Lemmas.Pattern.Find.String
String.Slice.contains_slice_eq_false_iff : ∀ {t s : String.Slice}, s.contains t = false ↔ ¬t.copy.toList <:+: s.copy.toList
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instLawfulEqOrdUnitVal : ∀ {x : ℚ}, Std.LawfulEqOrd (Std.Time.Internal.UnitVal x)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.mulEquivCongr_apply_smul : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : IsDomain B] [inst_5 : Algebra A B] [inst_6 : FaithfulSMul A B]
  [inst_7 : MulSemiringAction G B] [inst_8 : MulSemiringAction G' B] [inst_9 : IsGaloisGroup G A B]
  [inst_10 : IsGaloisGroup G' A B] [inst_11 : Finite G] [inst_12 : Finite G'] (g : G) (x : B),
  (IsGaloisGroup.mulEquivCongr G G' A B) g • x = g • x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_const : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] (c : E),
  ∫ (x : ℝ) in a..b, c = (b - a) • c
-- Mathlib.Data.Set.Monotone
Set.monotoneOn_insert_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  MonotoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddMonoid.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid Y],
  LocallyConstant.instAddMonoid = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Similarity
similar_comm : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Similar v₁ v₂ ↔ Similar v₂ v₁
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isPullback_inr_inr_coprodMap : ∀ {X Y X' Y' : AlgebraicGeometry.Scheme} (f : X ⟶ X') (g : Y ⟶ Y'),
  CategoryTheory.IsPullback g CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr
    (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_omega0_opow : ∀ {a b : Ordinal.{u_1}}, b ≠ 0 → (a < Ordinal.omega0 ^ b ↔ ∃ c < b, ∃ n, a < Ordinal.omega0 ^ c * ↑n)
-- Lean.Data.Json.Parser
Lean.Json.Parser.escapedChar : Std.Internal.Parsec.String.Parser Char
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult.Different.sizeOf_spec : sizeOf Mathlib.Linter.TextBased.ComparisonResult.Different✝ = 1
-- Mathlib.Data.TypeVec
TypeVec.lastFun_from_append1_drop_last : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)}, TypeVec.lastFun TypeVec.fromAppend1DropLast = id
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.surjective_of_epi : ∀ {A B : GrpCat} (f : A ⟶ B) [CategoryTheory.Epi f], Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_ext : ∀ {M N : MagmaCat} {f g : M ⟶ N}, MagmaCat.Hom.hom f = MagmaCat.Hom.hom g → f = g
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
      h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_ne_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [Finite α], AddChar.doubleDualEmb a ≠ 0 ↔ a ≠ 0
-- Mathlib.Data.List.SplitLengths
List.splitLengths.eq_2 : ∀ {α : Type u_1} (x : List α) (n : ℕ) (ns : List ℕ),
  (n :: ns).splitLengths x =
    match List.splitAt n x with
    | (x0, x1) => x0 :: ns.splitLengths x1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofInv_Y' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s), (CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).Y' = X
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinder_eq_empty_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [h_nonempty : Nonempty ((i : ι) → α i)] (s : Finset ι) (S : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S = ∅ ↔ S = ∅
-- Lean.Server.GoTo
_private.Lean.Server.GoTo.0.Lean.Server.locationLinksFromBinder.binderInfo? : Lean.FVarId → Lean.Server.GoToM (Option Lean.Elab.Info)
-- Mathlib.Topology.Constructions
Continuous.finInit : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin (n + 1)) → A j},
  Continuous f → Continuous fun a => Fin.init (f a)
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Compose two isomorphisms in a bicategorical category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.Bicategory.«term_≪⊗≫_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.leibniz_iff_X : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] [IsScalarTower R (MvPolynomial σ R) A] (D : MvPolynomial σ R →ₗ[R] A),
  D 1 = 0 →
    ((∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p) ↔
      ∀ (s : σ →₀ ℕ) (i : σ),
        D ((MvPolynomial.monomial s) 1 * MvPolynomial.X i) =
          (MvPolynomial.monomial s) 1 • D (MvPolynomial.X i) + MvPolynomial.X i • D ((MvPolynomial.monomial s) 1))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_lt_of_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b < c → a ≤ 0 → b + a < c
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.toPreorderOfLEArgs : {α : Type u} → Std.Packages.PartialOrderOfLEArgs α → Std.Packages.PreorderOfLEArgs α
-- Lean.Parser.Do
Lean.Parser.Term.doIfLet : Lean.Parser.Parser
-- Lean.Meta.Basic
/-- Eta expand the given expression.
Example:
```
etaExpand (mkConst ``Nat.add)
```
produces `fun x y => Nat.add x y`
 -/
Lean.Meta.etaExpand : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
hasMFDerivAt_extChartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 1 M] {x y : M},
  y ∈ (chartAt H x).source → HasMFDerivAt% (↑(extChartAt I x)) y (mfderiv% ↑(chartAt H x) y)
-- Batteries.Util.ExtendedBinder
/-- A extended binder in parentheses  -/
Batteries.ExtendedBinder.extBinderParenthesized : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} {X Y : CategoryTheory.Limits.Cocone F.leftOp} (f : X ⟶ Y),
  CategoryTheory.Limits.coconeLeftOpOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
-- Mathlib.Data.List.Basic
List.of_mem_filter : ∀ {α : Type u} {p : α → Bool} {a : α} {l : List α}, a ∈ List.filter p l → p a = true
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_eventually_monotone : ∀ {u v : ℕ → ENNReal}, u ≤ᶠ[Filter.atTop] v → ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf v
-- Mathlib.Computability.StateTransition
StateTransition.EvalsTo.mk.sizeOf_spec : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} [inst : SizeOf σ] (steps : ℕ)
  (evals_in_steps : (flip bind f)^[steps] (some a) = b),
  sizeOf { steps := steps, evals_in_steps := evals_in_steps } = 1 + sizeOf steps + sizeOf evals_in_steps
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- If a pair has a split coequalizer, it has a coequalizer.  -/
CategoryTheory.Limits.hasCoequalizer_of_hasSplitCoequalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [CategoryTheory.HasSplitCoequalizer f g], CategoryTheory.Limits.HasCoequalizer f g
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.comapDomainAddMonoidHom_apply : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : MonoidAlgebra R N), (MonoidAlgebra.comapDomainAddMonoidHom f hf) x = MonoidAlgebra.comapDomain f hf x
-- Mathlib.Topology.Algebra.Monoid
/-- Given an open neighborhood `U` of `0` there is an open neighborhood `V` of `0`
such that `V + V ⊆ U`.  -/
exists_open_nhds_zero_add_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [ContinuousAdd M] {U : Set M},
  U ∈ nhds 0 → ∃ V, IsOpen V ∧ 0 ∈ V ∧ V + V ⊆ U
-- Init.Data.List.Nat.BEq
List.beq_eq_decide : ∀ {α : Type u_1} [inst : BEq α] {as bs : List α},
  (as == bs) =
    if h : as.length = bs.length then decide (∀ (i : ℕ) (h' : i < as.length), (as[i] == bs[i]) = true) else false
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_mul_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) * t ⊆ ⋂ i, ⋂ j, s i j * t
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → Std.ExtDHashMap.Const.get? (m₁ \ m₂) k = Std.ExtDHashMap.Const.get? m₁ k
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.mainSum.eq_1 : ∀ {s : BoundingSieve} (muPlus : ℕ → ℝ), BoundingSieve.mainSum muPlus = ∑ d ∈ s.prodPrimes.divisors, muPlus d * s.nu d
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.mk.injEq : ∀ {α : Sort u_1} (content : α) (location : Lean.Syntax) (seen : Bool) (content_1 : α) (location_1 : Lean.Syntax)
  (seen_1 : Bool),
  ({ content := content, location := location, seen := seen } =
      { content := content_1, location := location_1, seen := seen_1 }) =
    (content = content_1 ∧ location = location_1 ∧ seen = seen_1)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
/-- Let `L : C ⥤ D` be a localization functor with respect to a Serre class `P`
in the abelian category `C`. If `G : C ⥤ₑ E` is an exact functor to an abelian
category, it "factors" through `D` (i.e. it is in the essential image of
`whiskeringLeft L P E : (D ⥤ₑ E) ⥤ C ⥤ₑ E`) iff `G` inverts the class
of morphisms `P.isoModSerre`.  -/
CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] (E : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} E]
  [inst_5 : CategoryTheory.Abelian E] [inst_6 : L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : L.Additive],
  (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).essImage = fun G =>
    P.isoModSerre.IsInvertedBy G.obj
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
le_sigNeg_of_negDef : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] {V : Submodule R M},
  (QuadraticMap.restrict (-Q) V).PosDef → Module.finrank R ↥V ≤ sigNeg Q
-- Aesop.Index.Basic
Aesop.IndexingMode.or.sizeOf_spec : ∀ (imodes : Array Aesop.IndexingMode), sizeOf (Aesop.IndexingMode.or imodes) = 1 + sizeOf imodes
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationNatIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (X : CategoryTheory.Sheaf J D),
  ((CategoryTheory.sheafificationNatIso J D).inv.app X).hom =
    CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id X.obj) ⋯
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α},
  MeasureTheory.IsAddFundamentalDomain G t ν →
    ∀ {U : Set (Quotient (AddAction.orbitRel G α))},
      MeasurableSet U → μ U = ν (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ t)
-- Aesop.Util.Basic
Aesop.withExceptionTransform : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → (Lean.MessageData → Lean.MessageData) → m α → m α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Given `F : C ⥤ D` and `X : D`, to upgrade a functor `G : E ⥤ C` to a functor
`E ⥤ CostructuredArrow F X`, it suffices to provide maps `F.obj (G.obj Y) ⟶ X` for all `Y`
making the obvious triangles involving all `F.map (G.map g)` commute.

This is of course the same as providing a cocone over `F ⋙ G` with cocone point `X`, see
`Functor.toCostructuredArrowIsoToCostructuredArrow`.  -/
CategoryTheory.Functor.toCostructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (G : CategoryTheory.Functor E C) →
              (F : CategoryTheory.Functor C D) →
                (X : D) →
                  (f : (Y : E) → F.obj (G.obj Y) ⟶ X) →
                    (∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) →
                      CategoryTheory.Functor E (CategoryTheory.CostructuredArrow F X)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.eq_1 : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass M = Antisymmetrization (ArchimedeanOrder M) fun x1 x2 => x1 ≤ x2
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.ennrealRatEmbed_encode : ∀ (q : ℚ), MeasureTheory.SimpleFunc.ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal
-- Mathlib.Data.FP.Basic
FP.instInhabitedRMode : Inhabited FP.RMode
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- The submodule of `ModularForm Γ k` consisting of cusp forms, defined as the range of
the inclusion `CuspForm.toModularFormₗ`.  -/
ModularForm.cuspFormSubmodule : (Γ : Subgroup (GL (Fin 2) ℝ)) → (k : ℤ) → [inst : Γ.HasDetOne] → Submodule ℂ (ModularForm Γ k)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.noncommSum_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M)
  (comm : (↑t).Pairwise (Function.onFun AddCommute f)), (∀ c ∈ t, f c ∈ S) → t.noncommSum f comm ∈ S
-- Lean.Meta.Closure
Lean.Meta.Closure.State.toProcess : Lean.Meta.Closure.State → Array Lean.Meta.Closure.ToProcessElement
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.mapIncl.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (p : (i : ι) → Submodule R (s i)),
  PiTensorProduct.mapIncl p = PiTensorProduct.map fun i => (p i).subtype
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.parts.sizeOf_spec : ∀ (p : Array Lean.Elab.InlayHintLabelPart), sizeOf (Lean.Elab.InlayHintLabel.parts p) = 1 + sizeOf p
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_ofNat : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : NatCast M] (n : ℕ) [inst_1 : n.AtLeastTwo],
  ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.toSubring.congr_simp : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (p p_1 : MvPowerSeries σ R) (e_p : p = p_1) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T) (a a_1 : σ →₀ ℕ),
  a = a_1 → p.toSubring T hp a = p_1.toSubring T ⋯ a_1