mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setIntegral_setAverage_sub : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {s : Set α} {f : α → E} [CompleteSpace E],
  μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → ∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ - f x ∂μ = 0
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_sub_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y z : F), inner 𝕜 (x - y) z = inner 𝕜 x z - inner 𝕜 y z
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)],
  (∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
      R ∈ K.coverings X → ∀ {U : C} (g : U ⟶ X), R g → P f → P (CategoryTheory.CategoryStruct.comp g f)) →
    (∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
        R ∈ K.coverings X → (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f) →
      P.IsLocalAtSource K
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.hereditarily_iff : ∀ {p : ZFSet.{u} → Prop} {x : ZFSet.{u}}, ZFSet.Hereditarily p x ↔ p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.Quotient.vadd_coe : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] (H : AddSubgroup G)
  [inst_3 : AddAction.QuotientAction X H] (b : X) (g : G), b +ᵥ ↑g = ↑(b +ᵥ g)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasDerivWithinAt.arsinh : ∀ {f : ℝ → ℝ} {s : Set ℝ} {a f' : ℝ},
  HasDerivWithinAt f f' s a → HasDerivWithinAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') s a
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Opens.isoOfLE hUV).hom U.ι =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι V.ι
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.instModule : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → (ρ : Representation k G V) → Module k ρ.Coinvariants
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Given manifolds `M`, `N` and an open neighbourhood `U` of a point `x : M`, the evaluation-at-`x`
map to `N` from smooth functions from  `U` to `N`.  -/
smoothSheaf.evalAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (N : Type u) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H N] →
                                        (x : ↑(TopCat.of M)) →
                                          (U : TopologicalSpace.OpenNhds x) →
                                            (smoothSheaf IM I M N).presheaf.obj (Opposite.op ↑U) → N
-- Mathlib.Topology.Closure
isOpen_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen (interior s)
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_symm_apply_castAdd : ∀ {m n : ℕ} (x : Fin m), finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.orderIsoOfIso_apply : ∀ {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e : X ≅ Y) (hA : B.preimage e.hom = A) (x : A.N),
  (SSet.Subcomplex.N.orderIsoOfIso e hA) x = { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ }
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Composition of the inverse of a partial equivalence and this partial equivalence is equivalent
to the restriction of the identity to the target.  -/
PartialEquiv.symm_trans_self : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.symm.trans e ≈ PartialEquiv.ofSet e.target
-- Mathlib.Dynamics.Ergodic.Action.Basic
MeasureTheory.ergodicSMul_iterateMulAct : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → α},
  Measurable f → (ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.mem_smul_pointwise_iff_exists : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Subring R), r ∈ m • S ↔ ∃ s ∈ S, m • s = r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The first projection of the pullback of `f` and `g`.  -/
CategoryTheory.Limits.pullback.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasPullback f g] → CategoryTheory.Limits.pullback f g ⟶ X
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft_mul_factorizationLCMRight : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
-- Init.Data.SInt.Lemmas
Int16.le_of_eq : ∀ {a b : Int16}, a = b → a ≤ b
-- Lean.Data.SSet
/-- Staged set. It is just a simple wrapper on top of Staged maps.  -/
Lean.SSet : (α : Type u) → [BEq α] → [Hashable α] → Type (max u 0)
-- Mathlib.RingTheory.Valuation.Archimedean
Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered : ∀ {F : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O F] {v : Valuation F Γ₀} [MulArchimedean ↥(MonoidHom.mrange v)],
  v.Integers O → (IsPrincipalIdealRing O ↔ ¬DenselyOrdered ↑(Set.range ⇑v))
-- Mathlib.Data.Set.Monotone
/-- **Alias** of `strictMono_domRestrict`. -/
strictMono_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMono (s.domRestrict f) ↔ StrictMonoOn f s
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.precomposing_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) (f : a ⟶ b),
  (CategoryTheory.Bicategory.precomposing a b c).obj f = CategoryTheory.Bicategory.precomp c f
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_comp_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R),
  (MvPolynomial.aeval f).comp (MvPolynomial.bind₁ g) = MvPolynomial.aeval fun i => (MvPolynomial.aeval f) (g i)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.mem_saturation_iff' : ∀ {M : Type u_1} [inst : CommMonoid M] {s : Submonoid M} {x : M}, x ∈ s.saturation ↔ ∃ y, y * x ∈ s
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.mkQL_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (S : Submodule R M) (x : M), S.mkQL x = S.mkQ x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]? = m[k]?
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.induction_on : ∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : PerfectClosure K p)
  {q : PerfectClosure K p → Prop}, (∀ (x : ℕ × K), q (PerfectClosure.mk K p x)) → q x
-- Mathlib.Probability.StrongLaw
MeasureTheory.AEStronglyMeasurable.memLp_truncation : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ} {p : ENNReal}, MeasureTheory.MemLp (ProbabilityTheory.truncation f A) p μ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.product_mul_product_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Mul α] [inst_2 : Mul β] [inst_3 : DecidableEq β]
  (s₁ s₂ : Finset α) (t₁ t₂ : Finset β), s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_hom_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (i : Opposite.op U ⟶ Opposite.op V),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).map i.unop).op)
      (AlgebraicGeometry.Scheme.Hom.appIso f V).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).hom (X.presheaf.map i)
-- Init.Data.List.Nat.Range
/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
List.mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {x : α × ℕ} {l : List α}, x ∈ l.zipIdx ↔ l[x.2]? = some x.1
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_iff_isRightRegular : ∀ {R : Type u_1} [inst : Semiring R] [IsArtinianRing R] {x : R}, IsUnit x ↔ IsRightRegular x
-- Mathlib.Data.List.SplitLengths
List.length_splitLengths : ∀ {α : Type u_1} (l : List α) (sz : List ℕ), (sz.splitLengths l).length = sz.length
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_insert_of_notMem : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (f : α → β)
  (comm : (↑(insert a s)).Pairwise (Function.onFun Commute f)),
  a ∉ s → (insert a s).noncommProd f comm = f a * s.noncommProd f ⋯
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The hypotheses are symmetric in `f` and `g`, with the constant `ε` replaced by `ε⁻¹`.  -/
WeakFEPair.symm : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → WeakFEPair E
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
Topology.IsOpenEmbedding.compatiblePreserving : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑Y) hf.functor
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_toArray : ∀ {α : Type u_1} {xs : ListSlice α}, (Std.Slice.toArray xs).toList = Std.Slice.toList xs
-- Init.Data.UInt.Lemmas
UInt64.toFin_toBitVec : ∀ (x : UInt64), x.toBitVec.toFin = x.toFin
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.Hom.ext_iff : ∀ {A B : AddMagmaCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_obj : ∀ (X : AlgebraicGeometry.LocallyRingedSpace),
  AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.obj X = X.toSheafedSpace
-- Mathlib.Order.CountableSupClosed
countableInfClosure_min : ∀ {α : Type u_2} {s t : Set α} [inst : Preorder α], s ⊆ t → CountableInfClosed t → countableInfClosure s ⊆ t
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- Assume that `E` is a normed vector space over semirings `𝕜 ⊆ 𝕜'` and that `x ∈ s` is a point
of unique differentiability with respect to the set `s` and the smaller semiring `𝕜`,
then `x` is also a point of unique differentiability with respect to the set `s`
and the larger semiring `𝕜'`.
 -/
UniqueDiffWithinAt.mono_field : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} {𝕜' : Type u_3} [inst_4 : Semiring 𝕜'] [inst_5 : SMul 𝕜 𝕜']
  [inst_6 : Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E], UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜' s x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₀_desc_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₀
      (CategoryTheory.CategoryStruct.comp (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) =
    CategoryTheory.CategoryStruct.comp f₀ h
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj Z₁₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp w₁₂
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.m₁) h) =
    CategoryTheory.CategoryStruct.comp u₂₃ (CategoryTheory.CategoryStruct.comp w₁₃ h)
-- Batteries.Data.Vector.Basic
Vector.scanrM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → β → m β) (as : Vector α n)
  (cur : β) (i : ℕ) (hi : i ≤ n) (acc : Vector β (n - i)),
  Vector.scanrM.loop f as cur i hi acc =
    if h_gt : 0 < i then do
      let next ← f as[i - 1] cur
      Vector.scanrM.loop f as next (i - 1) ⋯ (Vector.cast ⋯ (acc.push cur))
    else pure (Vector.cast ⋯ (acc.push cur).reverse)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.normal_ker : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M), f.ker.Normal
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.mem_centralizer_iff : ∀ {M : Type u_1} {S : Set M} [inst : Monoid M] {z : M}, z ∈ Submonoid.centralizer S ↔ ∀ g ∈ S, g * z = z * g
-- Init.GrindInstances.Ring.UInt
UInt16.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_eq_toList_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toList = it.toIterM.toList.run
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_congr : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → (ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
lipschitzOnWith_closure_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α}
  {K : NNReal}, ContinuousOn f (closure s) → (LipschitzOnWith K f (closure s) ↔ LipschitzOnWith K f s)
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instOne : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → One ↑(Set.Ioc 0 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.c₂ : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Lean.Meta.Grind.Arith.Cutsat.LeCnstr
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given a representation `A` of a commutative monoid `G`, the map `ρ_A(g)` is a representation
morphism `A ⟶ A` for any `g : G`.  -/
Rep.applyAsHom : {k : Type u} → [inst : Semiring k] → {G : Type v} → [inst_1 : CommMonoid G] → (A : Rep.{u_1, u, v} k G) → G → (A ⟶ A)
-- Init.Data.BitVec.Basic
/-- Returns the `i`th most significant bit.
 -/
BitVec.getMsb : {w : ℕ} → BitVec w → Fin w → Bool
-- Mathlib.Data.Int.Lemmas
/-- A specialization of `abs_sub_lt_of_nonneg_of_lt` for working with the signed subtraction
of natural numbers.  -/
Int.natAbs_coe_sub_coe_lt_of_lt : ∀ {a b n : ℕ}, a < n → b < n → (↑a - ↑b).natAbs < n
-- Aesop.Forward.PremiseIndex
Aesop.instBEqPremiseIndex.beq : Aesop.PremiseIndex → Aesop.PremiseIndex → Bool
-- Lean.Elab.SyntheticMVars
/-- Any kind of pending synthetic metavariable can be postponed.
Universe constrains may also be postponed.
 -/
Lean.Elab.Term.PostponeBehavior.yes : Lean.Elab.Term.PostponeBehavior
-- Init.Data.Nat.Basic
Nat.eq_zero_or_eq_sub_one_add_one : ∀ {n : ℕ}, n = 0 ∨ n = n - 1 + 1
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocSemiring R⦄,
  HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
the period chain complex
`... ⟶ (A ⊗ₖ k[G])_G --⟦Id ⊗ N⟧--> (A ⊗ₖ k[G])_G --⟦Id ⊗ (ρ(g⁻¹) - 𝟙)⟧--> (A ⊗ₖ k[G])_G ⟶ 0`
is isomorphic as a complex in `ModuleCat k` to
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`.  -/
Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) →
              HomologicalComplex.coinvariantsTensorObj A (Rep.FiniteCyclicGroup.resolution k g⁻¹ ⋯).complex ≅
                Rep.FiniteCyclicGroup.moduleCatChainComplex A g
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.ciSup_add : ∀ {ι : Type u} (f : ι → Cardinal.{v}) [Nonempty ι],
  BddAbove (Set.range f) → ∀ (c : Cardinal.{v}), (⨆ i, f i) + c = ⨆ i, f i + c
-- Init.Data.Range.Polymorphic.UInt
USize.instLeast? : Std.PRange.Least? USize
-- Std.Async.Basic
Std.Async.MaybeTask.ofTask.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Task α), sizeOf (Std.Async.MaybeTask.ofTask a) = 1 + sizeOf a
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- ContextInfo for running MetaM  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.ci : Mathlib.Linter.Flexible.TacticData✝ → Lean.Elab.ContextInfo
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The inclusion to the coproduct as a bundled continuous map.  -/
TopCat.sigmaι : {ι : Type v} → (α : ι → TopCat) → (i : ι) → α i ⟶ TopCat.of ((i : ι) × ↑(α i))
-- Mathlib.RingTheory.WittVector.WittPolynomial
/-- `wittPolynomial p R n` is the `n`-th Witt polynomial
with respect to a prime `p` with coefficients in a commutative ring `R`.
It is defined as:

`∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`.  -/
Witt.termW_ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The (diagonal) entries of the matrix.  -/
Module.Basis.SmithNormalForm.a : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} → {ι : Type u_4} → {n : ℕ} → Module.Basis.SmithNormalForm N ι n → Fin n → R
-- Mathlib.Algebra.Lie.Nilpotent
/-- The upper (aka ascending) central series.

See also `LieSubmodule.lcs`.  -/
LieSubmodule.ucs : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → ℕ → LieSubmodule R L M → LieSubmodule R L M
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psum_isSymmetric : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  (MvPolynomial.psum σ R n).IsSymmetric
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] (T T' : Set α → E →L[ℝ] G''),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : MeasureTheory.SimpleFunc α E),
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T' f
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C}, Nonempty (CategoryTheory.PreOneHypercover S)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangleIso.hom.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₁
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Probability measures are defined as the subtype of measures that have the property of being
probability measures (i.e., their total mass is one).  -/
MeasureTheory.ProbabilityMeasure : (Ω : Type u_1) → [MeasurableSpace Ω] → Type u_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β] {f : Option β → Option β}, (t.alter k f)[k]! = (f t[k]?).get!
-- Mathlib.Dynamics.FixedPoints.Support
/-- The fixed support of a self-map `f : X → X` is the closure of the set of non-fixed points, often
called the support of `f`, but we use the term "fixed support" to disamiguate from other notions.  -/
Function.fixedSupport : {X : Type u_1} → [TopologicalSpace X] → (X → X) → Set X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Z`-coordinate of a representative of `P + Q` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Jacobian.addZ : {R : Type r} → [CommRing R] → (Fin 3 → R) → (Fin 3 → R) → R
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.preDefault : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc