mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Basic
/-- The closure of a compact set in an R₁ space is a compact set.  -/
IsCompact.closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {K : Set X}, IsCompact K → IsCompact (closure K)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The set of points for which a measurable sequence of functions converges is measurable.  -/
MeasureTheory.measurableSet_exists_tendsto : ∀ {ι : Type u_2} {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : TopologicalSpace γ]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace γ] [SecondCountableTopology γ] [inst_4 : MeasurableSpace γ]
  [hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → β → γ},
  (∀ (i : ι), Measurable (f i)) → MeasurableSet {x | ∃ c, Filter.Tendsto (fun n => f n x) l (nhds c)}
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.foldlM_array : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ 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] {xs : Array α} {init : β} {f : β → α → m β}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun b' =>
        inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'; epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ Array.foldlM f init xs ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toAlternatingMap_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], ContinuousAlternatingMap.toAlternatingMap 0 = 0
-- Mathlib.MeasureTheory.Measure.AddContent
/-- For an `m : addContent C` on a `SetSemiring C` and `s t : Set α` with `s ⊆ t`, we can write
`m t = m s + ∑ i in hC.disjointOfDiff ht hs, m i`.  -/
MeasureTheory.eq_add_disjointOfDiff_of_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  s ⊆ t → m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termα_mod_G_2 : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.kind? : Lean.Lsp.FoldingRange → Option Lean.Lsp.FoldingRangeKind
-- Lean.Environment
Lean.writeModule : Lean.Environment → System.FilePath → optParam Bool true → IO Unit
-- Lean.Parser.Basic
/-- The `colEq` parser ensures that the next token starts at exactly the column of the saved
position (see `withPosition`). This can be used to do whitespace sensitive syntax like
a `by` block or `do` block, where all the lines have to line up.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.checkColEq : optParam String "checkColEq" → Lean.Parser.Parser
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H) (q : G ⧸ H),
  Quotient.mk'' ↑(hS.leftQuotientEquiv q) = q
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.hqhom : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (self : Algebra.Smooth.DescentAux✝ A B) (i : Algebra.Smooth.DescentAux.vars✝ self),
  (Algebra.Smooth.DescentAux.q✝ self i).IsHomogeneous 1
-- Lean.PrettyPrinter.Delaborator.Basic
/-- See `SubExpr.nextExtraPos`.  -/
Lean.PrettyPrinter.Delaborator.State.holeIter : Lean.PrettyPrinter.Delaborator.State → Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousAt.zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f x → ∀ (z : ℤ), ContinuousAt (f ^ z) x
-- Mathlib.Data.Set.Prod
/-- A product set is included in a product set if and only factors are included, or a factor of the
first set is empty.  -/
Set.prod_subset_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β}, s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
-- Mathlib.Data.Part
Part.some_mul_some : ∀ {α : Type u_1} [inst : Mul α] (a b : α), Part.some a * Part.some b = Part.some (a * b)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.mem_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ Finset.nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s
-- Mathlib.Topology.EMetricSpace.Diam
Metric.edist_le_of_ediam_le : ∀ {X : Type u_2} {s : Set X} {x y : X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  x ∈ s → y ∈ s → Metric.ediam s ≤ d → edist x y ≤ d
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.structuredArrowDownwards_initial_iff_of_iso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₂ X₂' : C₂} (e : X₂ ≅ X₂'), (w.structuredArrowDownwards X₂).Initial ↔ (w.structuredArrowDownwards X₂').Initial
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isIso_fromTildeΓ_iff : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules},
  CategoryTheory.IsIso M.fromTildeΓ ↔ (AlgebraicGeometry.tilde.functor R).essImage M
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) {Z_1 : C}
  (h : I.cocomplex.X 1 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (CategoryTheory.CategoryStruct.comp (I.cocomplex.d 0 1) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.userPostDSimprocs : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_signSet_apply_isComplex : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : { w // w.IsComplex }),
  ((NumberField.mixedEmbedding.negAt (NumberField.mixedEmbedding.signSet x)) x).2 w = x.2 w
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Non-commutative version of `fderiv_inv`  -/
fderiv_inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {x : R}, x ≠ 0 → fderiv 𝕜 Inv.inv x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The naturality condition.  -/
CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (CategoryTheory.CategoryStruct.comp (θ.naturality f).hom h) =
    CategoryTheory.CategoryStruct.comp (η.naturality f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) h)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- The inclusion of left exact functors into functors is fully faithful.  -/
CategoryTheory.LeftExactFunctor.fullyFaithful : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.LeftExactFunctor.forget C D).FullyFaithful
-- Init.WF
Prod.RProdSubLex : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a b : α × β),
  Prod.RProd ra rb a b → Prod.Lex ra rb a b
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.add_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a + b).toProd.1 = a.toProd.1 + b.toProd.1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forM_eq_forM : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : α → m PUnit.{w + 1}}, Std.TreeSet.forM f t = forM t f
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_4}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'}
  {x : E} {y : E'},
  ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n g t y → ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y)
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings for a semicolon preceded by a space.  -/
Mathlib.Linter.TextBased.linter.whitespaceBeforeSemicolon : Lean.Option Bool
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k).minD fallback = k
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw : ∀ {Ω : Type u_1} {E : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} [inst : MeasurableSpace E]
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E] {X : T → Ω → E}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsGaussianProcess._auto_1},
  ProbabilityTheory.IsGaussianProcess X P →
    ∀ (I : Finset T), ProbabilityTheory.HasGaussianLaw (fun ω => I.restrict fun x => X x ω) P
-- Mathlib.Algebra.Group.Action.Basic
/-- Embedding of `α` into functions `M → α` induced by a multiplicative action of `M` on `α`.  -/
MulAction.toFun : (M : Type u_2) → (α : Type u_5) → [inst : Monoid M] → [MulAction M α] → α ↪ M → α
-- Init.Data.Range.Polymorphic.Map
Std.Rxi.LawfulHasSize.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.Rxi.HasSize α] [inst_3 : Std.Rxi.HasSize β] [Std.Rxi.LawfulHasSize β]
  (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesRxiSize], Std.Rxi.LawfulHasSize α
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are flat `R`-algebras, both of them are transcendental, then `A ⊗[R] B` cannot
be a field.  -/
Algebra.TensorProduct.not_isField_of_transcendental : ∀ (R : Type u) [inst : CommRing R] (A : Type v) [inst_1 : CommRing A] (B : Type w) [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Module.Flat R A] [Module.Flat R B] [Algebra.Transcendental R A]
  [Algebra.Transcendental R B], ¬IsField (TensorProduct R A B)
-- Lean.Message
Lean.instReprTraceResult : Repr Lean.TraceResult
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β), ↑(RelIso.ofOnFun r f) = f
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.dvd_pow_iff_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [DecompositionMonoid R] {x y : R} {n : ℕ},
  Squarefree x → n ≠ 0 → (x ∣ y ^ n ↔ x ∣ y)
-- Init.Omega.Constraint
Lean.Omega.positivize.eq_1 : ∀ (p : Lean.Omega.Constraint × Lean.Omega.Coeffs), Lean.Omega.positivize p = (Lean.Omega.positivize? p).getD p
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.productEquiv_apply_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  (F : J → C) [inst_3 : CategoryTheory.Limits.HasProduct F]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (∏ᶜ F)) (j : J),
  (CategoryTheory.Limits.Concrete.productEquiv F) x j =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a x acc => f a ⋯ acc
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.disjoint_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → ∀ {H K : Subgroup G}, Disjoint H K → Disjoint (Subgroup.map f H) (Subgroup.map f K)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.map_trim_comap : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : Measurable f), MeasureTheory.Measure.map f (μ.trim ⋯) = MeasureTheory.Measure.map f μ
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coe_liftNCAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : Semiring B] [inst_5 : Algebra R B] (f : A →ₐ[R] B)
  (g : Multiplicative M →* B) (h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)),
  ⇑(AddMonoidAlgebra.liftNCAlgHom f g h_comm) = ⇑(AddMonoidAlgebra.liftNC ↑f ⇑g)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.normedSpaceAux : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_3} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : NonUnitalCStarAlgebra A] →
            [inst_3 : PartialOrder A] → [inst_4 : StarOrderedRing A] → NormedSpace ℂ (CStarMatrix m n A)
-- Lean.Expr
/-- Given `a b : Nat`, returns `a * b`  -/
Lean.mkNatMul : Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.SInt.Lemmas
ISize.zero_add : ∀ (a : ISize), 0 + a = a
-- Init.Data.List.Basic
/-- Drops the first element of a nonempty list, returning the tail. Returns `none` when the argument is
empty.

Alternatives include `List.tail`, which returns the empty list on failure, `List.tail?`, which
returns an `Option`, and `List.tail!`, which panics on the empty list.

Examples:
 * `["apple", "banana", "grape"].tailD ["orange"] = ["banana", "grape"]`
 * `["apple"].tailD ["orange"] = []`
 * `[].tailD ["orange"] = ["orange"]`
 -/
List.tailD : {α : Type u} → List α → List α → List α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
StrictMono.const_nsmul : ∀ {β : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : Preorder β] [AddLeftStrictMono M]
  [AddRightStrictMono M] {f : β → M}, StrictMono f → ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => n • f x
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.eventually_lt_const : ∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {l : Filter γ}
  {f : γ → α} {u v : α}, v < u → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, f a < u
-- Lean.Data.NameMap.Basic
/-- `filter f m` returns the `NameMap` consisting of all
"`key`/`val`"-pairs in `m` where `f key val` returns `true`.  -/
Lean.NameMap.filter : {α : Type} → (Lean.Name → α → Bool) → Lean.NameMap α → Lean.NameMap α
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.one_of : ∀ {A : Type u_1} [inst : Monoid A], 1 = 1
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.strictAntiOn_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ}, StrictConcaveOn ℝ S f → DifferentiableOn ℝ f S → StrictAntiOn (derivWithin f S) S
-- Batteries.Data.String.Legacy
/-- Checks whether a string contains the specified character.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
* `"green".contains 'e' = true`
* `"green".contains 'x' = false`
* `"".contains 'x' = false`
 -/
String.Legacy.contains : String → Char → Bool
-- Mathlib.Order.Directed
isDirected_onFun : ∀ {α : Type u_1} {ι : Sort u_3} {r : α → α → Prop} {f : ι → α}, IsDirected ι (Function.onFun r f) ↔ Directed r f
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.CommGrp C),
  (CategoryTheory.Preadditive.commGrpEquivalence.counitIso.hom.app X).hom.hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Data.Fin.SuccPred
Fin.exists_succ_eq_of_ne_zero : ∀ {n : ℕ} {x : Fin (n + 1)}, x ≠ 0 → ∃ y, y.succ = x
-- Mathlib.GroupTheory.Perm.ViaEmbedding
Equiv.Perm.viaEmbedding_apply : ∀ {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (ι : α ↪ β) (x : α), (e.viaEmbedding ι) (ι x) = ι (e x)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.all_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m β'} {p : β' → Bool},
  Std.IterM.all p (Std.Iter.mapM f it) =
    Std.IterM.allM (fun x => (fun x => { down := p x }) <$> f x) (Std.Iter.mapM pure it)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_ofNat_zero : ∀ {R : Type u} [inst : Semiring R] (a : ℕ) [inst_1 : a.AtLeastTwo], (OfNat.ofNat a).coeff 0 = OfNat.ofNat a
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_le_eq`. -/
gauge_le_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {a : ℝ},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → 0 ≤ a → {x | gauge s x ≤ a} = ⋂ r, ⋂ (_ : a < r), r • s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_8 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftLeft rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_8 w n lhs rhs
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_findIdxNth_iff_of_left_lt_countP : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {m : ℕ} {xs : List α},
  n < List.countP p xs → (List.findIdxNth p xs n = List.findIdxNth p xs m ↔ n = m)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.skipPrefix?_prop_eq_skipPrefix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.skipPrefix? p = s.skipPrefix? fun x => decide (p x)
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Coreflective R]
  (X : (CategoryTheory.coreflectorAdjunction R).toComonad.Coalgebra),
  CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction R).counit.app X.A)
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toFun : M → N) (map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y),
  sizeOf { toFun := toFun, map_mul' := map_mul' } = 1
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_ofDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : αᵒᵈ}, IsAddRightRegular (OrderDual.ofDual a) ↔ IsAddRightRegular a
-- Mathlib.Logic.Function.OfArity
/-- The type of `n`-ary functions `α → α → ... → β`.

Note that this is not universe polymorphic, as this would require that when `n=0` we produce either
`Unit → β` or `ULift β`.  -/
Function.OfArity : Type u → Type u → ℕ → Type u
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.map_inf : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I J : Ideal R),
  Ideal.map (algebraMap R S) (I ⊓ J) = Ideal.map (algebraMap R S) I ⊓ Ideal.map (algebraMap R S) J
-- Lean.Elab.MutualInductive
Lean.Elab.Command.CtorView.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) (declName : Lean.Name) (declId binders : Lean.Syntax)
  (type? : Option Lean.Syntax),
  sizeOf
      { ref := ref, modifiers := modifiers, declName := declName, declId := declId, binders := binders,
        type? := type? } =
    1 + sizeOf ref + sizeOf modifiers + sizeOf declName + sizeOf declId + sizeOf binders + sizeOf type?
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.ext : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p q : Submodule R M},
  (∀ (x : M), x ∈ p ↔ x ∈ q) → p = q