mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.addSnippet : Lean.VersoModuleDocs.DocContext✝ → Lean.VersoModuleDocs.Snippet → Except String Lean.VersoModuleDocs.DocContext✝
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F =
    { obj := fun X => { base := X.base, fiber := CategoryTheory.AsSmall.up.obj X.fiber },
      map := fun {X Y} f => { base := f.base, fiber := CategoryTheory.AsSmall.up.map f.fiber }, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_insert` that requires `s ∩ support f` rather
than `s` to be finite.  -/
finsum_mem_insert' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {a : α} {s : Set α} (f : α → M),
  a ∉ s → (s ∩ Function.support f).Finite → ∑ᶠ (i : α) (_ : i ∈ insert a s), f i = f a + ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.CategoryTheory.Monoidal.Conv
CategoryTheory.Conv.mul_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.MonObj N] (f g : CategoryTheory.Conv M N),
  f * g =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f M)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft N g)
          CategoryTheory.MonObj.mul))
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- The value of `χ₄ n`, for `n : ℕ`, depends only on `n % 4`.  -/
ZMod.χ₄_nat_mod_four : ∀ (n : ℕ), ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.FreeCoequalizer.π_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.FreeCoequalizer.π X).f = X.a
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_sub_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R), ⌈a - 1⌉₊ = ⌈a⌉₊ - 1
-- Std.Time.Format.Modifier
Std.Time.Modifier.a.injEq : ∀ (presentation presentation_1 : Std.Time.Text),
  (Std.Time.Modifier.a presentation = Std.Time.Modifier.a presentation_1) = (presentation = presentation_1)
-- Lean.Server.GoTo
Lean.Server.instBEqGoToKind.beq : Lean.Server.GoToKind → Lean.Server.GoToKind → Bool
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
RingEquiv.map_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type w}
  [inst_3 : CommRing S] (f : R ≃+* S) (M : Matrix n n R), f M.det = (f.mapMatrix M).det
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_nat_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ n, x ≤ ↑n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid of an n-simplex can be obtained from a vertex by adding
`n` times the vector from the centroid to the `faceOppositeCentroid`.  -/
Affine.Simplex.centroid_eq_smul_vsub_vadd_point : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.centroid = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.points i
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntryD.eq_3 : ∀ {α : Type u} {β : Type v} (x : α × β) (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 => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntryD
      (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) x =
    Std.DTreeMap.Internal.Impl.Const.maxEntryD (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) x
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.instOrdApplyKey : Ord Mathlib.Tactic.ClickSuggestions.ApplyKey
-- Mathlib.Data.Vector.Basic
List.Vector.get_tail : ∀ {α : Type u_1} {n : ℕ} (x : List.Vector α n) (i : Fin (n - 1)), x.tail.get i = x.get ⟨↑i + 1, ⋯⟩
-- Mathlib.Order.Heyting.Basic
sdiff_le_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, b \ a ≤ ￢a
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `NormedAddGroup.tendsto_nhds_zero`. -/
NormedAddCommGroup.tendsto_nhds_zero : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedAddGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
-- Mathlib.Order.Defs.PartialOrder
le_iff_lt_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Icc_eq_empty_of_lt : ∀ {m n : ℤ}, n < m → Finset.Icc m n = ∅
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- General version of `preimage_vadd_setₛₗ`.
This version assumes that the vector addition of `c` is surjective
while the vector addition of `σ c` is injective.  -/
preimage_vadd_setₛₗ' : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : VAdd M α]
  [inst_1 : VAdd N β] [inst_2 : FunLike F α β] [AddActionSemiHomClass F σ α β] {f : F} {t : Set β} {c : M},
  (Function.Surjective fun m => c +ᵥ m) → (Function.Injective fun n => σ c +ᵥ n) → ⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {X' : C} (g : X' ⟶ X) {p q : ℤ}
  (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q')
  (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0),
  CochainComplex.HomComplex.Cocycle.fromSingleMk (CategoryTheory.CategoryStruct.comp g f) h q' hq' ⋯ =
    (CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf).precomp ((CochainComplex.singleFunctor C p).map g)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_subtype : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : AddSubmonoid M), AddMonoidHom.mrange s.subtype = s
-- Init.Data.UInt.Lemmas
UInt16.mod_eq_of_lt : ∀ {a b : UInt16}, a < b → a % b = a
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_def : ∀ (x : GaussianInt), GaussianInt.toComplex x = ↑x.re + ↑x.im * Complex.I
-- Mathlib.Data.List.Sigma
List.notMem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)}, a ∉ l.keys ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
-- Mathlib.RingTheory.Ideal.Operations
/-- Prime avoidance. Atiyah-Macdonald 1.11, Eisenbud 3.3, Matsumura Ex.1.6.  -/
Ideal.subset_union_prime : ∀ {ι : Type u_1} {R : Type u} [inst : CommRing R] {s : Finset ι} {f : ι → Ideal R} (a b : ι),
  (∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) → ∀ {I : Ideal R}, ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_smul : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul S R] (s : S) (r : R), WithVal.toVal v (s • r) = s • WithVal.toVal v r
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g),
  rTensor.inverse Q hfg hg = rTensor.inverse_of_rightInverse Q hfg ⋯
-- Batteries.Classes.Order
compareOfLessAndEq.congr_simp : ∀ {α : Type u_1} (x x_1 : α),
  x = x_1 →
    ∀ (y y_1 : α),
      y = y_1 →
        ∀ [inst : LT α] {inst_1 : Decidable (x < y)} [inst_2 : Decidable (x_1 < y_1)] {inst_3 : DecidableEq α}
          [inst_4 : DecidableEq α], compareOfLessAndEq x y = compareOfLessAndEq x_1 y_1
-- Lean.Meta.Tactic.Grind.Proof
/-- Given `lhsEqCommon : lhs = common`, returns a proof for `lhs = rhs`.  -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkProofFrom : Lean.Expr → Lean.Expr → Option Lean.Expr → Bool → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.le_connectivity_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K ≤ 1 →
    S.Nonempty → ∀ {r : ℝ}, r ≤ Finset.connectivity✝ K S ↔ ∀ ⦃A : Finset G⦄, A.Nonempty → r ≤ Finset.expansion✝ K S A
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- A continuous multilinear function `f` admits a Taylor series, whose successive terms are given
by `f.iteratedFDeriv n`. This is the point of the definition of `f.iteratedFDeriv`.  -/
ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F),
  HasFTaylorSeriesUpTo ⊤ ⇑f fun v n => f.iteratedFDeriv n v
-- Mathlib.Topology.Continuous
continuous_iff_image_closure_subset_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f ↔ ∀ (s : Set X), f '' closure s ⊆ closure (f '' s)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.symm_A : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H), b.symm.A = b.A
-- Mathlib.Data.ENat.Lattice
ENat.le_iInf₂_add_iInf₂ : ∀ {ι : Sort u_2} {a : ℕ∞} {κ : Sort u_4} {q₁ : ι → Sort u_5} {q₂ : κ → Sort u_6} {f : (i : ι) → q₁ i → ℕ∞}
  {g : (k : κ) → q₂ k → ℕ∞},
  (∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk) → a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.differentiableAt_smoothingFn : ∀ {x : ℝ}, 1 < x → DifferentiableAt ℝ AkraBazziRecurrence.smoothingFn x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The localization of a torsion-free monoid is torsion-free.  -/
Localization.instIsMulTorsionFree : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} [IsMulTorsionFree M], IsMulTorsionFree (Localization S)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.commute_of_mem_adjoin_of_forall_mem_commute : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {a b : A} {s : Set A},
  b ∈ NonUnitalStarAlgebra.adjoin R s → (∀ b ∈ s, Commute a b) → (∀ b ∈ s, Commute a (star b)) → Commute a b
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_zero_linearMap : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M], ↑0 = 0
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_prime_le_iff_dvd : ∀ {d n : ℕ}, d ≠ 0 → n ≠ 0 → ((∀ (p : ℕ), Nat.Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n)
-- Lean.Meta.LazyDiscrTree
/-- Map from discriminator trie roots to the index.  -/
Lean.Meta.LazyDiscrTree.roots : {α : Type} → Lean.Meta.LazyDiscrTree α → Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Construct a `NonUnitalSubsemiring R` from a set `s`, a subsemigroup `sg`, and an additive
submonoid `sa` such that `x ∈ s ↔ x ∈ sg ↔ x ∈ sa`.  -/
NonUnitalSubsemiring.mk' : {R : Type u} →
  [inst : NonUnitalNonAssocSemiring R] →
    (s : Set R) → (sg : Subsemigroup R) → ↑sg = s → (sa : AddSubmonoid R) → ↑sa = s → NonUnitalSubsemiring R
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- The reflection in `Kᗮ` of an element of `K` is its negation.  -/
Submodule.reflection_mem_subspace_orthogonal_precomplement_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, v ∈ K → Kᗮ.reflection v = -v
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSlice_eq_dropSliceTR.go : ∀ (α : Type u_1) (l : List α) (m : ℕ) (acc : Array α) (xs : List α) (n : ℕ),
  l = acc.toList ++ xs → List.dropSliceTR.go l m xs n acc = acc.toList ++ List.dropSlice n (m + 1) xs
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_pow : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (n : ℕ) (a : M) (b : ↥S),
  Localization.mk a b ^ n = Localization.mk (a ^ n) (b ^ n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Power)
  (m_1 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denoteAsIntModule ctx (Lean.Grind.CommRing.Mon.mult p m_1) =
    Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m_1 (Lean.Grind.CommRing.Power.denote ctx p)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_X : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x Polynomial.X = x
-- Mathlib.Logic.Nonempty
nonempty_psum : ∀ {α : Sort u_3} {β : Sort u_4}, Nonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β
-- Mathlib.InformationTheory.Hamming
Hamming.instNontrivialOfNonemptyOfDefault : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Inhabited ι] [∀ (i : ι), Nonempty (β i)] [Nontrivial (β default)],
  Nontrivial (Hamming β)
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.result : Qq.SortLocalDecls.State → Array Lean.LocalDecl
-- Mathlib.Order.CompleteLattice.Basic
sSup_empty : ∀ {α : Type u_1} [inst : CompleteLattice α], sSup ∅ = ⊥
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (p : C) [projective : CategoryTheory.Projective p]
  (f : p ⟶ X) [epi : CategoryTheory.Epi f] (p_1 : C) (projective_1 : CategoryTheory.Projective p_1) (f_1 : p_1 ⟶ X)
  (epi_1 : CategoryTheory.Epi f_1),
  ({ p := p, projective := projective, f := f, epi := epi } =
      { p := p_1, projective := projective_1, f := f_1, epi := epi_1 }) =
    (p = p_1 ∧ f ≍ f_1)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coeff_uniqueAlgEquiv_symm : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [inst_4 : Subsingleton M] (a : A) (m : M),
  ((AddMonoidAlgebra.uniqueAlgEquiv R M).symm a).coeff m = a
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Char
-- Init.Control.Except
/-- Returns `true` if the value is `Except.ok`, `false` otherwise.  -/
Except.isOk : {ε : Type u} → {α : Type u_1} → Except ε α → Bool
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mem_affineSpan_image_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Affine.Simplex k P n) {fs : Set (Fin (n + 1))} {i : Fin (n + 1)},
  s.points i ∈ affineSpan k (s.points '' fs) ↔ i ∈ fs
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_inj : ∀ {M : Type u_2} [inst : Mul M] {S T : Subsemigroup M}, S.op = T.op ↔ S = T
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_eq_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (r : ENNReal), ∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}
-- Init.Data.SInt.Basic
/-- Constructs an `Int16` from an `Int` that is known to be in bounds.  -/
Int16.ofIntLE : (i : ℤ) → Int16.minValue.toInt ≤ i → i ≤ Int16.maxValue.toInt → Int16
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M N : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N),
  Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f) (Φ.skyscraperPresheafFunctor.map g)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isLittleO_pow_pow_atTop_of_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {p q : ℕ},
  p < q → (fun x => x ^ p) =o[Filter.atTop] fun x => x ^ q
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.sub_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : α) (v₁ v₂ v : ℚ),
  (v == v₁ - v₂) = true →
    a = Lean.Grind.Field.NormNum.ofRat v₁ →
      b = Lean.Grind.Field.NormNum.ofRat v₂ → a - b = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_mem_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {n : ℕ}, 1 ∈ s → 1 ∈ s ^ n
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.FunctorCategory.whiskerLeft_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F' G' : CategoryTheory.Functor C D} (F : CategoryTheory.Functor C D)
  (β : F' ⟶ G') (X : C),
  (CategoryTheory.Monoidal.FunctorCategory.whiskerLeft F β).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (β.app X)
-- Init.Data.String.FindPos
/-- Obtains the smallest valid position that is greater than or equal to the given byte position.
 -/
String.posGE : (s : String) → (offset : String.Pos.Raw) → offset ≤ s.rawEndPos → s.Pos
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_contains_field_as_subfield : ∀ {E : Type u_2} [inst : Field E] (S : Set E) (F : Subfield E), ↑F ⊆ ↑(IntermediateField.adjoin (↥F) S)
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_map_lt_prod_map : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R]
  [NeZero 1] {ι : Type u_3} {s : Multiset ι},
  s ≠ 0 → ∀ (f g : ι → R), (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i < g i) → (Multiset.map f s).prod < (Multiset.map g s).prod
-- Init.Data.Array.Nat
Array.sum_div_length_le_max_of_max?_eq_some_nat : ∀ {x : ℕ} {xs : Array ℕ}, xs.max? = some x → xs.sum / xs.size ≤ x
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
and `L` has no zero smul divisors by `A`, the `A`-rank of the integral closure `C` of `A` in `L`
is equal to the `K`-rank of `L`.  -/
IsIntegralClosure.rank : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsPrincipalIdealRing A] [Module.IsTorsionFree A L],
  Module.finrank A C = Module.finrank K L
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.isUnit_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommGroup Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : CommRing R] [IsDomain R] {x : HahnSeries Γ R}, IsUnit x ↔ IsUnit x.leadingCoeff
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_pow_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] (x : HahnSeries Γ R) (n : ℕ), (x ^ n).cardSupp ≤ x.cardSupp ^ n
-- Mathlib.Data.ENat.Basic
ENat.mul_left_strictMono : ∀ {a : ℕ∞}, a ≠ 0 → a ≠ ⊤ → StrictMono fun x => x * a
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_inv_of_invertible : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [Invertible A], A⁻¹⁻¹ = A
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.le_one_iff : ∀ {α : Type u_2} [inst : One α] {f : Filter α}, f.NeBot → (f ≤ 1 ↔ f = 1)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWindowClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.WindowClientCapabilities
-- Mathlib.Analysis.Complex.Basic
Complex.continuous_im : Continuous Complex.im
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {a : α} {n : ℕ},
  a ∈ n • s ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
-- Mathlib.Algebra.Group.TypeTags.Finite
instFiniteMultiplicative : ∀ {α : Type u} [Finite α], Finite (Multiplicative α)
-- Mathlib.RingTheory.WittVector.Frobenius
/-- `frobeniusFun` is the function underlying the ring endomorphism
`frobenius : 𝕎 R →+* frobenius 𝕎 R`.  -/
WittVector.frobeniusFun : {p : ℕ} → {R : Type u_1} → [CommRing R] → WittVector p R → WittVector p R
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_bot : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L), Subfield.map f ⊥ = ⊥
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true ↔ k ∈ t
-- Mathlib.Algebra.Order.Module.Defs
smul_max_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β]
  [inst_3 : Zero α] [PosSMulMono α β], 0 ≤ a → ∀ (b₁ b₂ : β), a • max b₁ b₂ = max (a • b₁) (a • b₂)
-- Init.Data.Order.Ord
Std.instLawfulBEqOrd : ∀ {α : Type u} {x : Ord α}, Std.LawfulBEqOrd α
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.single_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toLex fun₀ | b => 1) < toLex fun₀ | a => 1) ↔ a < b
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.M.map_mk : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat) {j k : J} (f : j ⟶ k)
  (x : ↑(F.obj j)),
  AddMonCat.FilteredColimits.M.mk F ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x⟩ =
    AddMonCat.FilteredColimits.M.mk F ⟨j, x⟩
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instInhabited : {α : Type u_2} → [inst : BooleanAlgebra α] → Inhabited (BooleanSubalgebra α)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_bot : ∀ {M : Type u_1} [inst : MulOneClass M] {x : M}, x ∈ ⊥ ↔ x = 1
-- Aesop.Script.TacticState
Aesop.Script.TacticState.visibleGoalsHaveMVars : Aesop.Script.TacticState → Bool
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.LaxTrans.Hom η θ}, x = y ↔ x.as = y.as