mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.maxKey? = some km → Std.DTreeMap.Internal.Impl.contains km t = true
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassDiv.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f g : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A],
  f /ʷ g =
    if hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 then PowerSeries.IsWeierstrassDivisorAt.div ⋯ f else 0
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (values : Std.Queue α) (consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α))
  (closed : Bool),
  sizeOf { values := values, consumers := consumers, closed := closed } =
    1 + sizeOf values + sizeOf consumers + sizeOf closed
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.homologyFunctor.congr_simp : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology V] (i i_1 : ι),
  i = i_1 → HomotopyCategory.homologyFunctor V c i = HomotopyCategory.homologyFunctor V c i_1
-- Mathlib.Algebra.Quaternion
Quaternion.star_eq_self : ∀ {R : Type u_3} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R}, star a = a ↔ a = ↑a.re
-- Mathlib.Order.Fin.Basic
/-- `Fin.succAbove p` as an `OrderEmbedding`.  -/
Fin.succAboveOrderEmb : {n : ℕ} → Fin (n + 1) → Fin n ↪o Fin (n + 1)
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of the forward direction of `AffineSubspace.wOppSide_comm`. -/
AffineSubspace.WOppSide.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y → s.WOppSide y x
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.lift.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (f : R →+* S) (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)),
  Ideal.ResidueField.lift I f hf₁ hf₂ = IsLocalization.lift ⋯
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- See Note [custom simps projection]  -/
CoalgEquiv.Simps.apply : {R : Type u_5} →
  [inst : CommSemiring R] →
    {α : Type u_6} →
      {β : Type u_7} →
        [inst_1 : AddCommMonoid α] →
          [inst_2 : AddCommMonoid β] →
            [inst_3 : Module R α] →
              [inst_4 : Module R β] →
                [inst_5 : CoalgebraStruct R α] → [inst_6 : CoalgebraStruct R β] → (α ≃ₗc[R] β) → α → β
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- Addition in `WeakBilin B` is continuous.  -/
WeakBilin.instContinuousAdd : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜], ContinuousAdd (WeakBilin B)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cot_inv_eq_tan : ∀ (x : ℂ), x.cot⁻¹ = Complex.tan x
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) =
    (Std.Internal.List.containsKey k l₁ && !l₂.contains k)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv4.inj : ∀ {ipv4 ipv4_1 : Std.Net.IPv4Addr}, Std.Http.URI.Host.ipv4 ipv4 = Std.Http.URI.Host.ipv4 ipv4_1 → ipv4 = ipv4_1
-- Mathlib.Algebra.Group.Defs
nsmulRec'.eq_3 : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : Add M] (x : M) (k : ℕ), nsmulRec' k.succ.succ x = nsmulRec' (k + 1) x + x
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.classifier_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Sheaf.classifier J).Ω₀ = CategoryTheory.Sheaf.terminal J CategoryTheory.Limits.Types.isTerminalPUnit
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.Cache.insert.match_1.eq_1 : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (motive : Std.Tactic.BVDecide.BVExpr.Cache aig → Sort u_1)
  (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size)
  (h_1 :
    (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w) →
      (hbound :
          ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
            (map.get k h1)[i].gate < aig.decls.size) →
        motive { map := map, hbound := hbound }),
  (match { map := map, hbound := hbound } with
    | { map := map, hbound := hbound } => h_1 map hbound) =
    h_1 map hbound
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β]
  [inst_3 : Top β] [inst_4 : Min γ] [inst_5 : Top γ] [inst_6 : Min δ] [inst_7 : Top δ] (f : InfTopHom γ δ)
  (g : InfTopHom β γ) (h : InfTopHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.RingTheory.Localization.Defs
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →+* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` sending `z : S` to `g x * (g y)⁻¹`, where `(x, y) : R × M` are such that
`z = f x * (f y)⁻¹`.  -/
IsLocalization.lift : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Submonoid R} →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            {P : Type u_3} →
              [inst_3 : CommSemiring P] → [IsLocalization M S] → {g : R →+* P} → (∀ (y : ↥M), IsUnit (g ↑y)) → S →+* P
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : Π₀ (_a : α), ℕ}, DFinsupp.toMultiset f = DFinsupp.toMultiset g ↔ f = g
-- Std.Sat.AIG.CNF
/-- Connect SAT results about the AIG to SAT results about the CNF.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.denote_as_go : ∀ {aig : Std.Sat.AIG ℕ} {start : ℕ} {inv : Bool} {h1 : start < aig.decls.size} {assign : ℕ → Bool},
  ⟦Std.Sat.AIG.toCNF.projectLeftAssign✝ aig assign,
        { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ =
      false →
    Std.Sat.CNF.eval assign
        (Std.Sat.CNF.add [(start, !inv)]
          (Std.Sat.AIG.toCNF.State.cnf✝ ↑(Std.Sat.AIG.toCNF.go✝ aig start h1 (Std.Sat.AIG.toCNF.State.empty✝ aig)))) =
      false
-- Init.GetElem
GetElem?.mk : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} →
        [toGetElem : GetElem coll idx elem valid] →
          (coll → idx → Option elem) → ([Inhabited elem] → coll → idx → elem) → GetElem? coll idx elem valid
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.instEssentiallySmallColimitsClosureOfSmallOfLocallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C]
  [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), CategoryTheory.LocallySmall.{w, v', u'} (J a)],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure J)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_ofNat_eq_lift : ∀ {o : Ordinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Ordinal.omega (OfNat.ofNat n) = Ordinal.lift.{v, u} o ↔ Ordinal.omega (OfNat.ofNat n) = o
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The `AddHom` underlying a `LinearMap`.  -/
LinearMap.toAddHom : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_16} →
            {M₂ : Type u_17} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] → [inst_4 : Module R M] → [inst_5 : Module S M₂] → (M →ₛₗ[σ] M₂) → M →ₙ+ M₂
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) left whiskering for R-modules  -/
SemimoduleCat.MonoidalCategory.whiskerLeft : {R : Type u} →
  [inst : CommSemiring R] →
    (M : SemimoduleCat R) →
      {N₁ N₂ : SemimoduleCat R} →
        (N₁ ⟶ N₂) → (SemimoduleCat.MonoidalCategory.tensorObj M N₁ ⟶ SemimoduleCat.MonoidalCategory.tensorObj M N₂)
-- Lean.Meta.TryThis
/-- Style as a success.  -/
Lean.Meta.Tactic.TryThis.SuggestionStyle.success : Lean.Meta.Tactic.TryThis.SuggestionStyle
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} [inst_2 : SizeOf C] [inst_3 : SizeOf κ]
  (page : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r))
  (iso :
    (r r' : ℤ) →
      (pq : κ) →
        (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
          (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
            (page r ⋯).homology pq ≅ (page r' ⋯).X pq),
  sizeOf { page := page, iso := iso } = 1
-- Mathlib.Data.Sym.Sym2
Sym2.Rel.symm : ∀ {α : Type u_1} {x y : α × α}, Sym2.Rel α x y → Sym2.Rel α y x
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mul.eq_def : ∀ {v : Lean.Level} {M : Q(Type v)} (x x_1 : Mathlib.Tactic.FieldSimp.qNF q(«$M»)),
  x.mul x_1 =
    match x, x_1 with
    | [], l => l
    | l, [] => l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ > k₂ then ((a₁, x₁), k₁) :: Mathlib.Tactic.FieldSimp.qNF.mul t₁ (((a₂, x₂), k₂) :: t₂)
      else
        if k₁ = k₂ then ((a₁ + a₂, x₁), k₁) :: Mathlib.Tactic.FieldSimp.qNF.mul t₁ t₂
        else ((a₂, x₂), k₂) :: Mathlib.Tactic.FieldSimp.qNF.mul (((a₁, x₁), k₁) :: t₁) t₂
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenQuotientMap id
-- Init.Data.UInt.Lemmas
UInt8.toNat_zero : UInt8.toNat 0 = 0
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendIsometry_symm_apply : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ) (f : Fin (m + n) → α),
  (Fin.appendIsometry m n).symm f = (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i))
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addLeftMono : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : PartialOrder M] [inst_2 : AddLeftStrictMono M],
  AddLeftMono { x // 0 < x }
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.isoMk_hom_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : Q.RespectsIso] {A B : P.Over Q X} (f : A.left ≅ B.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom B.hom = A.hom)
      CategoryTheory.MorphismProperty.Over.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Over.isoMk f w).hom.left = f.hom
-- Mathlib.GroupTheory.Perm.ConjAct
Equiv.Perm.support_conj_eq_smul_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (k : ConjAct (Equiv.Perm α)) (g : Equiv.Perm α),
  (k • g).support = ConjAct.ofConjAct k • g.support
-- Mathlib.Data.FunLike.Module
FunLike.smulCommClass : ∀ {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [inst : SMul M β]
  [inst_1 : SMul M' β] [inst_2 : SMul M F] [inst_3 : SMul M' F] [IsSMulApply M F α β] [IsSMulApply M' F α β]
  [SMulCommClass M M' β], SMulCommClass M M' F
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.mk.inj : ∀ {curr top curr_1 top_1 : ℕ},
  { curr := curr, top := top } = { curr := curr_1, top := top_1 } → curr = curr_1 ∧ top = top_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context.mk.inj : ∀ {toIntId toIntId_1 : ℕ}, { toIntId := toIntId } = { toIntId := toIntId_1 } → toIntId = toIntId_1
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_sup : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring R) (f : F),
  NonUnitalSubsemiring.map f (s ⊔ t) = NonUnitalSubsemiring.map f s ⊔ NonUnitalSubsemiring.map f t
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_top : ∀ {M : Type u_2} [inst : AddZeroClass M], ⊤.op = ⊤
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_ediv : ∀ {x y z : ℤ}, x / y / z = x / (y * z) - if y < 0 ∧ ¬z ∣ x / y then z.sign else 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instCompleteLattice : {R : Type u} → {M : Type v} → [inst : VAdd R M] → CompleteLattice (SubAddAction R M)
-- Init.Data.Float.Model.Float
/-- Negate a `Float.Model`.
 -/
Float.Model.neg : Float.Model → Float.Model
-- Mathlib.Data.Set.Subset
Set.image_val_mono : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, D ⊆ E → Subtype.val '' D ⊆ Subtype.val '' E
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.υ_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.υ hF).hom.app X =
    CategoryTheory.CategoryStruct.comp (e'.unitIso.hom.app (eA.functor.obj X)) (e'.inverse.map (hF.hom.app X))
-- Mathlib.Dynamics.Flow
Flow.toHomeomorph_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddGroup τ]
  (ϕ : Flow τ α) (t : τ) (x : α), (ϕ.toHomeomorph t) x = ϕ.toFun t x
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o] [LawfulMonad m] [LawfulMonad n]
  [LawfulMonad o] [inst_8 : Std.IteratorLoop α m n] [inst_9 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n]
  [Std.LawfulIteratorLoop α m o] [inst_12 : MonadLiftT m n] [inst_13 : MonadLiftT n o] [LawfulMonadLiftT m n]
  [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.mapWithPostcondition f it) =
    Std.IterM.foldM
      (fun d b => do
        let c ← liftM (f b).run
        g d c)
      init it
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0.sizeOf_spec : ∀ (k : ℕ) (c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.numEq0 k c₁ c₂) = 1 + sizeOf k + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_one : Complex.sqrt 1 = 1
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive
semigroup homomorphism `AddHom Mᵃᵒᵖ Nᵃᵒᵖ`. This is the action of the (fully faithful)`ᵃᵒᵖ`-functor
on morphisms.  -/
AddHom.op : {M : Type u_3} → {N : Type u_4} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) ≃ (Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ)
-- Init.Data.List.Impl
/-- Removes the first element of a list for which `p` returns `true`. If no element satisfies `p`, then
the list is returned unchanged.

This is a tail-recursive version of `eraseP`, used at runtime.

Examples:
  * `[2, 1, 2, 1, 3, 4].erasePTR (· < 2) = [2, 2, 1, 3, 4]`
  * `[2, 1, 2, 1, 3, 4].erasePTR (· > 2) = [2, 1, 2, 1, 4]`
  * `[2, 1, 2, 1, 3, 4].erasePTR (· > 8) = [2, 1, 2, 1, 3, 4]`
 -/
List.erasePTR : {α : Type u_1} → (α → Bool) → List α → List α
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X)
  (s : CategoryTheory.Limits.Cocone S.arrows.diagram), (S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp_mul : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : CommMonoid β]
  [inst_3 : Preorder β] [inst_4 : CommMonoid γ] [inst_5 : Preorder γ] [inst_6 : IsOrderedMonoid β]
  [inst_7 : IsOrderedMonoid γ] (g : β →*o γ) (f₁ f₂ : α →*o β), g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
-- Mathlib.Algebra.Group.Equiv.Defs
Monoid.End.equiv_symm_apply : ∀ {M : Type u_9} [inst : MulOne M] (f : M →* M) (x : M), ((Monoid.End.equiv M).symm f) x = f x
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall g pg x r → HasFPowerSeriesOnBall (f - g) (pf - pg) x r
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.smul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y → ∀ (c : ℝ), BoxIntegral.HasIntegral I l (c • f) vol (c • y)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- A crude lemma estimating the difference between `log (1-x)` and its Taylor series at `0`,
where the main point of the bound is that it tends to `0`. The goal is to deduce the series
expansion of the logarithm, in `hasSum_pow_div_log_of_abs_lt_1`.

TODO: use one of generic theorems about Taylor's series to prove this estimate.
 -/
Real.abs_log_sub_add_sum_range_le : ∀ {x : ℝ},
  |x| < 1 → ∀ (n : ℕ), |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + Real.log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
-- Lean.Elab.Do.Basic
/-- Maps mutable variable names to their `MutVar` record. Kept in sync with `mutVars`.  -/
Lean.Elab.Do.Context.mutVarDefs : Lean.Elab.Do.Context → Std.HashMap Lean.Name Lean.Elab.Do.MutVar
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar_eq_of_measure_smul_eq_mul : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] {g : G} [inst_7 : MeasurableSpace A] [BorelSpace A] {μ : MeasureTheory.Measure A}
  [μ.IsAddHaarMeasure] [μ.Regular] {s : Set A},
  μ s ≠ 0 → μ s ≠ ⊤ → ∀ {r : NNReal}, μ (g • s) = ↑r * μ s → (MeasureTheory.distribHaarChar A) g = r
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Auxiliary definition for `OuterMeasure.mkMetric'`: given a function on sets
`m : Set X → ℝ≥0∞`, returns the maximal outer measure `μ` such that `μ s ≤ m s`
for any set `s` of diameter at most `r`.  -/
MeasureTheory.OuterMeasure.mkMetric'.pre : {X : Type u_2} → [EMetricSpace X] → (Set X → ENNReal) → ENNReal → MeasureTheory.OuterMeasure X
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassUnit_smul : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {a : A} {g : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) (a • g) ≠ 0),
  (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Graph.DFSState.mk.inj : ∀ {visited visited_1 : Std.HashSet ℕ}, { visited := visited } = { visited := visited_1 } → visited = visited_1
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The opposite of a factorization.  -/
CategoryTheory.MorphismProperty.MapFactorizationData.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W₁ W₂ : CategoryTheory.MorphismProperty C) →
      {X Y : C} → {f : X ⟶ Y} → W₁.MapFactorizationData W₂ f → W₂.op.MapFactorizationData W₁.op f.op
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
assumes `0≤K`.  -/
LipschitzOnWith.of_le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : NNReal),
  (∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y) → LipschitzOnWith K f s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- Map a quaternion into the clifford algebra.  -/
CliffordAlgebraQuaternion.ofQuaternion : {R : Type u_1} →
  [inst : CommRing R] →
    {c₁ c₂ : R} → QuaternionAlgebra R c₁ 0 c₂ →ₐ[R] CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instHomIsOverInv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] {f : X ⟶ Y} [inst_3 : CategoryTheory.IsIso f] [CategoryTheory.HomIsOver f S],
  CategoryTheory.HomIsOver (CategoryTheory.inv f) S
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.volume_sum_rpow_lt_one : ∀ (ι : Type u_1) [inst : Fintype ι] {p : ℝ},
  1 ≤ p →
    MeasureTheory.volume {x | ∑ i, |x i| ^ p < 1} =
      ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
-- Mathlib.Algebra.Group.Units.Basic
add_ne_zero : ∀ {α : Type u} [inst : AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
/-- The function `sinc` is continuous.  -/
Real.continuous_sinc : Continuous Real.sinc
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ),
  PowerSeries.trunc n = { toFun := PowerSeries.truncAux✝ n, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Ring.Opposite
/-- A non-unital ring homomorphism `f : R →ₙ+* S` such that `f x` commutes with `f y` for all `x, y`
defines a non-unital ring homomorphism to `Sᵐᵒᵖ`.  -/
NonUnitalRingHom.toOpposite : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] → (f : R →ₙ+* S) → (∀ (x y : R), Commute (f x) (f y)) → R →ₙ+* Sᵐᵒᵖ
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.reindex.eq_1 : ∀ {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] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  s.reindex e = { points := s.points ∘ ⇑e.symm, independent := ⋯ }