mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f z))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f z))
-- Lean.Attributes
/-- A `TagAttribute` variant where we can attach parameters to attributes.
It is slightly more expensive and consumes a little bit more memory than `TagAttribute`.

They provide the function `pAttr.getParam env decl` which returns `some p` iff declaration `decl`
contains the attribute `pAttr` with parameter `p`.  -/
Lean.ParametricAttribute : Type → Type
-- Init.PropLemmas
and_congr : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.regular : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : M →ₗ[R] M →ₗ[R] R} {x : M}, B.IsReflective x → IsRegular ((B x) x)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_sum : ∀ {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w}),
  Ordinal.lsub f = max (Ordinal.lsub fun a => f (Sum.inl a)) (Ordinal.lsub fun b => f (Sum.inr b))
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common arrows will agree with those of the original path `f`. In particular,
an arrow `i` with `i + 1 < j` can be identified with the same arrow in `f`.  -/
SSet.StrictSegal.spine_δ_arrow_lt : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)},
  i.succ.castSucc < j →
    (X.spine n
            ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X j)) (sx.spineToSimplex f))).arrow
        i =
      f.arrow i.castSucc
-- Mathlib.CategoryTheory.Whiskering
/-- The isomorphism between left-whiskering on the composition of functors and the composition
of two left-whiskering applications.  -/
CategoryTheory.Functor.whiskeringLeftObjCompIso : {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] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D D') →
                    (CategoryTheory.Functor.whiskeringLeft C D' E).obj (F.comp G) ≅
                      ((CategoryTheory.Functor.whiskeringLeft D D' E).obj G).comp
                        ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The Hausdorffification of a module with respect to an ideal.  -/
Hausdorffification : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_4
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H`, the induction functor `Rep k G ⥤ Rep k H` is left
adjoint to the restriction functor along `φ`.  -/
Rep.indResAdjunction : (k : Type u) →
  {G : Type v} →
    {H : Type v'} →
      [inst : CommRing k] →
        [inst_1 : Group G] → [inst_2 : Group H] → (φ : G →* H) → Rep.indFunctor k φ ⊣ Rep.resFunctor φ
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_nhds_top_iff_real : ∀ {α : Type u_2} {m : α → EReal} {f : Filter α}, Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
-- Mathlib.Order.Irreducible
SupPrime.ne_bot : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α} [inst_1 : OrderBot α], SupPrime a → a ≠ ⊥
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.w₀.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.dirichletUnitTheorem.w₀ = NumberField.Units.dirichletUnitTheorem.w₀
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.symmetric : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (self : ContDiffBumpBase E) (R : ℝ) (x : E),
  self.toFun R (-x) = self.toFun R x
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZifV1.default : Std.Time.TimeZone.TZif.TZifV1
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_trans : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → a ∣ c
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.constantBaseRingEquiv.eq_1 : ∀ (ι : Type u_1) (R : Type u_3) [inst : CommSemiring R] [inst_1 : Fintype ι],
  PiTensorProduct.constantBaseRingEquiv ι R =
    AlgEquiv.ofAlgHom (AlgHom.ofLinearMap (PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R ι R)) ⋯ ⋯)
      (Algebra.ofId R (PiTensorProduct R fun x => R)) ⋯ ⋯
-- Lean.Expr
/-- `mkAppN f #[a₀, ..., aₙ]` constructs the application `f a₀ a₁ ... aₙ`.
 -/
Lean.mkAppN : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.mk.inj : ∀ {α : Type u_6} {inst : MeasurableSpace α} {toOuterMeasure : MeasureTheory.OuterMeasure α}
  {m_iUnion :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure (f i)}
  {trim_le : toOuterMeasure.trim ≤ toOuterMeasure} {toOuterMeasure_1 : MeasureTheory.OuterMeasure α}
  {m_iUnion_1 :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure_1 (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure_1 (f i)}
  {trim_le_1 : toOuterMeasure_1.trim ≤ toOuterMeasure_1},
  { toOuterMeasure := toOuterMeasure, m_iUnion := m_iUnion, trim_le := trim_le } =
      { toOuterMeasure := toOuterMeasure_1, m_iUnion := m_iUnion_1, trim_le := trim_le_1 } →
    toOuterMeasure = toOuterMeasure_1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.instDecidableEqWalkingParallelFamily : {J : Type w} → DecidableEq (CategoryTheory.Limits.WalkingParallelFamily J)
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_zero : IsCyclic (ZMod 0)ˣ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.isIso_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupHomology X.X₂ (n + 1)) →
    CategoryTheory.Limits.IsZero (groupHomology X.X₂ n) → CategoryTheory.IsIso (groupHomology.δ hX (n + 1) n ⋯)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.TensorSigns.mk : {I : Type u_7} →
  [inst : AddMonoid I] →
    {c : ComplexShape I} →
      (ε' : Multiplicative I →* ℤˣ) →
        (∀ (p q r : I), c.Rel p q → c.Rel (p + r) (q + r)) →
          (∀ (p q r : I), c.Rel p q → c.Rel (r + p) (r + q)) → (∀ (p q : I), c.Rel p q → ε' q = -ε' p) → c.TensorSigns
-- Init.Tactics
/-- `specialize h a₁ ... aₙ` is equivalent to `replace h := h a₁ ... aₙ`.
It specializes the local hypothesis `h` by instantiating
universal quantifications and implications using the concrete terms `a₁` ... `aₙ`.
The tactic adds a new hypothesis with the same name and tries to remove
the original `h` if possible.

Example: given `h : ∀ (n : Nat), p n → q n` and `h' : p 2`,
then `specialize h 2 h'` replaces `h` with `h : q 2`.

The tactic also supports instantiating particular universal quantifiers
using named argument syntax. Example: given `h : ∀ (m n : Nat), p m n`,
then `specialize h (n := 2)` replaces `h` with `h : ∀ (m : Nat), p m 2`.
 -/
Lean.Parser.Tactic.specialize : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZSMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β],
  ContinuousMap.instZSMul = { smul := fun z f => { toFun := z • ⇑f, continuous_toFun := ⋯ } }
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.schwartzSeminormFamily_apply_zero : ∀ (𝕜 : Type u_2) (E : Type u_5) (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F], schwartzSeminormFamily 𝕜 E F 0 = SchwartzMap.seminorm 𝕜 0 0
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.toString : Lean.PersistentArray.Stats → String
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleRing.ext : ∀ {L : Type u_1} {x y : LieAdmissibleRing L},
  Add.add = Add.add →
    Zero.zero = Zero.zero →
      NSMul.nsmul = NSMul.nsmul →
        Neg.neg = Neg.neg → Sub.sub = Sub.sub → ZSMul.zsmul = ZSMul.zsmul → Mul.mul = Mul.mul → x = y
-- Init.Data.UInt.Bitwise
USize.toUInt32_and : ∀ (a b : USize), (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.rev : Turing.PartrecToTM2.K'
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.false_of_mem_of_not_mem : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsSatisfiable → ∀ {φ : L.Sentence}, φ ∈ T → FirstOrder.Language.BoundedFormula.not φ ∈ T → False
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instCharP : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  CharP (PerfectClosure K p) p
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.shrink.loop : {α : Type u} → ℕ → Array α → Array α
-- Mathlib.Algebra.Quaternion
Quaternion.coe_injective : ∀ {R : Type u_3} [inst : CommRing R], Function.Injective Quaternion.coe
-- Mathlib.Order.Interval.Finset.Defs
Subtype.instLocallyFiniteOrderBot : {α : Type u_1} →
  [inst : Preorder α] →
    (p : α → Prop) → [DecidablePred p] → [LocallyFiniteOrderBot α] → LocallyFiniteOrderBot (Subtype p)
-- Lean.Elab.DocString
Lean.Doc.DocArg.ident.inj : ∀ {val val_1 : Lean.Ident}, Lean.Doc.DocArg.ident val = Lean.Doc.DocArg.ident val_1 → val = val_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The `𝕜`-subring of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,
with extra structure.  -/
lpInftySubring : {I : Type u_5} →
  (B : I → Type u_6) → [inst : (i : I) → NormedRing (B i)] → [∀ (i : I), NormOneClass (B i)] → Subring (PreLp B)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Poly → α
-- Init.Data.UInt.Lemmas
UInt16.neg_add : ∀ {a b : UInt16}, -(a + b) = -a - b
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- `Hom_S(-, X)` sends a cofiltered limit of qcqs `S`-schemes with affine transition maps
to a filtered colimit if `X` is locally of finite presentation over `X`.  -/
AlgebraicGeometry.Scheme.preservesColimit_yoneda : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S : AlgebraicGeometry.Scheme}
  (D : CategoryTheory.Functor I (CategoryTheory.Over S)) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (CategoryTheory.Over.Hom.left (D.map f))]
  [∀ (i : I), CompactSpace ↥(D.obj i).left] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left] (X : CategoryTheory.Over S)
  [AlgebraicGeometry.LocallyOfFinitePresentation X.hom],
  CategoryTheory.Limits.PreservesColimit D.op (CategoryTheory.yoneda.obj X)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsClosedImmersion f],
  CategoryTheory.IsIso f ↔ AlgebraicGeometry.Scheme.Hom.ker f = ⊥
-- Mathlib.Tactic.Linter.GlobalAttributeIn
/-- Lint on any occurrence of `attribute [...] name in` which is not `local` or `scoped`:
these are a footgun, as the attribute is applied *globally* (despite the `in`).  -/
Mathlib.Linter.linter.globalAttributeIn : Lean.Option Bool
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.ext_of_toZModPow : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x y : ℤ_[p]},
  (∀ (n : ℕ), (PadicInt.toZModPow n) x = (PadicInt.toZModPow n) y) ↔ x = y
-- Mathlib.LinearAlgebra.Ray
/-- Negating a ray.  -/
instNegRay : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → Neg (Module.Ray R M)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
exists_lt_of_lt_ciSup' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α} {a : α},
  a < ⨆ i, f i → ∃ i, a < f i
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_add_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g₁ g₂ : (i : ι) → E i), ⟪f, g₁ + g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] + ⟪f, g₂⟫_[𝕜, w]
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instInhabited : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [S : AddTorsor V P] → Inhabited (AffineSubspace k P)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.isFintype : (self : FinBoolAlg) → Fintype ↑self.toBoolAlg
-- Mathlib.Topology.Compactness.CountablyCompact
/-- In a `T₁` space, a set is countably compact if and only if every infinite subset has an
accumulation point in the set.  -/
isCountablyCompact_iff_infinite_subset_has_accPt : ∀ {E : Type u_2} [inst : TopologicalSpace E] [T1Space E] {A : Set E},
  IsCountablyCompact A ↔ ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (Filter.principal B)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.optional.sizeOf_spec : sizeOf Std.Time.Reason.optional✝ = 1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkCongrArg : Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.mk.sizeOf_spec : ∀ (d : ℤ) (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof),
  sizeOf { d := d, p := p, h := h } = 1 + sizeOf d + sizeOf p + sizeOf h
-- Mathlib.Algebra.GradedMonoid
/-- `1 : A 0` is the value provided in `GOne.one`.  -/
GradedMonoid.GradeZero.one : {ι : Type u_1} → (A : ι → Type u_2) → [inst : Zero ι] → [GradedMonoid.GOne A] → One (A 0)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_inv_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (e : A ≅ B) (x : ↑B),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- The natural `R[X]`-linear equivalence between the two ways to represent an invariant submodule.
 -/
Module.AEval.restrict_equiv_mapSubmodule : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [inst_6 : IsScalarTower R A M] →
                      (p : Submodule R M) →
                        (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule) →
                          Module.AEval R (↥p) (LinearMap.restrict ((Algebra.lsmul R R M) a) hp) ≃ₗ[Polynomial R]
                            ↥((Module.AEval.mapSubmodule R M a) ⟨p, hp⟩)
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {R : Type u_2}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal], Ergodic f μ → ∀ (c : R), Ergodic f (c • μ)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.le_order_pow_of_constantCoeff_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (n : ℕ), PowerSeries.constantCoeff φ = 0 → ↑n ≤ (φ ^ n).order
-- Lean.Parser.Types
Lean.Parser.Error.mk.injEq : ∀ (unexpectedTk : Lean.Syntax) (unexpected : String) (expected : List String) (unexpectedTk_1 : Lean.Syntax)
  (unexpected_1 : String) (expected_1 : List String),
  ({ unexpectedTk := unexpectedTk, unexpected := unexpected, expected := expected } =
      { unexpectedTk := unexpectedTk_1, unexpected := unexpected_1, expected := expected_1 }) =
    (unexpectedTk = unexpectedTk_1 ∧ unexpected = unexpected_1 ∧ expected = expected_1)
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {z : Set β}, HasOpenLowerSections fun _x => z
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadLift_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ε : Type u} (x : m α)
  (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp x post epost.tail ⦄ MonadLift.monadLift x ⦃ post; epost ⦄
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_symm_X : ∀ {R : Type u_1} [inst : Semiring R], (Polynomial.opRingEquiv R).symm Polynomial.X = MulOpposite.op Polynomial.X
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousOn.neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn (-f) s
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.instIsCountablyGeneratedAtBotProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Filter.atBot.IsCountablyGenerated] [inst_2 : Preorder β]
  [Filter.atBot.IsCountablyGenerated], Filter.atBot.IsCountablyGenerated
-- Init.Data.List.Basic
List.sum_nil : ∀ {α : Type u} [inst : Add α] [inst_1 : Zero α], [].sum = 0
-- Mathlib.Computability.Partrec
Computable₂.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [inst : Primcodable α]
  [inst_1 : Primcodable β] [inst_2 : Primcodable γ] [inst_3 : Primcodable δ] [inst_4 : Primcodable σ] {f : γ → δ → σ}
  {g : α → β → γ} {h : α → β → δ},
  Computable₂ f → Computable₂ g → Computable₂ h → Computable₂ fun a b => f (g a b) (h a b)
-- Aesop.Builder.Basic
Aesop.PhaseSpec.unsafe : Aesop.UnsafeRuleInfo → Aesop.PhaseSpec
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.sup_edge_of_not_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → (G ⊔ SimpleGraph.edge u v).IsBridge s(u, v)
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_mul_left : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul M M] (a : M), Isometry fun x => a * x
-- Mathlib.Order.Defs.PartialOrder
/-- **Alias** of `le_antisymm`. -/
eq_of_le_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
-- Mathlib.MeasureTheory.Function.SimpleFunc
_private.Mathlib.MeasureTheory.Function.SimpleFunc.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a continuous function `c` realizes its maximum at a unique point `x₀` in a compact set `s`,
then the sequence of functions `(c x) ^ n / ∫ (c x) ^ n` is a sequence of peak functions
concentrating around `x₀`. Therefore, `∫ (c x) ^ n * g / ∫ (c x) ^ n` converges to `g x₀` if `g` is
integrable on `s` and continuous at `x₀`.

Version assuming that `μ` gives positive mass to all neighborhoods of `x₀` within `s`.
For a less precise but more usable version, see
`tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn`.
 -/
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos : ∀ {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α}
  [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ],
  IsCompact s →
    (∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)) →
      ∀ {c : α → ℝ},
        ContinuousOn c s →
          (∀ y ∈ s, y ≠ x₀ → c y < c x₀) →
            (∀ x ∈ s, 0 ≤ c x) →
              0 < c x₀ →
                x₀ ∈ s →
                  MeasureTheory.IntegrableOn g s μ →
                    ContinuousWithinAt g s x₀ →
                      Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ)
                        Filter.atTop (nhds (g x₀))
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.homMk.congr_simp : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X}
  (f f_1 : ↑Y → ↑Z) (e_f : f = f_1) (hf : Topology.ContinuousGeneratedBy X f),
  ContinuousGeneratedByCat.homMk f hf = ContinuousGeneratedByCat.homMk f_1 ⋯
-- Lean.Expr
Lean.BinderInfo.default.sizeOf_spec : sizeOf Lean.BinderInfo.default = 1
-- Mathlib.Algebra.Order.Module.Field
/-- Positivity extension for scalar multiplication.  -/
Mathlib.Meta.Positivity.evalSMul : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Set.Restrict
Set.MapsTo.coe_iterate_restrict : ∀ {α : Type u_1} {s : Set α} {f : α → α} (h : Set.MapsTo f s s) (x : ↑s) (k : ℕ),
  ↑((Set.MapsTo.restrict f s s h)^[k] x) = f^[k] ↑x
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_irrelevant : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜],
  (HomogeneousIdeal.irrelevant 𝒜).toIdeal = RingHom.ker (GradedRing.projZeroRingHom 𝒜)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.mk : ∀ {G : Type u} [inst : Group G], (∃ ι, Nonempty (FreeGroupBasis ι G)) → IsFreeGroup G
-- Mathlib.RingTheory.Valuation.Quotient
AddValuation.comap_supp : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀) {S : Type u_3} [inst_2 : CommRing S] (f : S →+* R),
  (AddValuation.comap f v).supp = Ideal.comap f v.supp
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.inv₀ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : GroupWithZero β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable f⁻¹
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → ⨍⁻ (x : α) in s, f x ∂μ < ⊤
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.coeff_zero_mem_comap_of_root_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I : Ideal S} {r : S},
  r ∈ I → ∀ {p : Polynomial R}, Polynomial.eval₂ f r p = 0 → p.coeff 0 ∈ Ideal.comap f I
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_toAddMonoidHom_injective : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], Function.Injective AddMonoidHomClass.toAddMonoidHom
-- Mathlib.Data.Finset.Sym
Finset.sym2_cons : ∀ {α : Type u_1} (a : α) (s : Finset α) (ha : a ∉ s),
  (Finset.cons a s ha).sym2 = (Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha)).disjUnion s.sym2 ⋯
-- Batteries.Data.Fin.Coding
/-- Decode `Ordering` from `Fin 3`.  -/
Fin.decodeOrdering : Fin 3 → Ordering
-- Mathlib.Data.PFun
/-- Turns a partial function into a function out of its domain.  -/
PFun.asSubtype : {α : Type u_1} → {β : Type u_2} → (f : α →. β) → ↑f.Dom → β