mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- An upper estimate (in terms of `Asymptotics.IsBigO`)
on the difference between two compositions of Taylor series.

Let `p₁`, `p₂`, `q₁`, `q₂` be four families of formal multilinear series
depending on a parameter `a`.
Suppose that the norms of `(p₁ · k)`, `(q₁ · k)`, and `(q₂ · k)` are bounded along a filter `l`
for all `k ≤ n`.
Also, suppose that $p₁(a, k) - p₂(a, k) = O(f(a))$, $q₁(a, k) - q₂(a, k) = O(f(a))$
along `l` for all `k ≤ n`.
Then the difference between `n`th terms of `(p₁ a).taylorComp (q₁ a)` and `(p₂ a).taylorComp (q₂ a)`
is `O(f(a))` too.

This lemma can be used, e.g., to show that the composition of two $C^{k+α}$ functions
is a $C^{k+α}$ function.  -/
FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {α : Type u_5} {H : Type u_6}
  [inst_7 : NormedAddCommGroup H] {l : Filter α} {p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G}
  {q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F} {f : α → H} {n : ℕ},
  (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖p₁ x k‖) →
    (∀ k ≤ n, (fun a => p₁ a k - p₂ a k) =O[l] f) →
      (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₁ x k‖) →
        (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₂ x k‖) →
          (∀ k ≤ n, (fun a => q₁ a k - q₂ a k) =O[l] f) →
            (fun a => (p₁ a).taylorComp (q₁ a) n - (p₂ a).taylorComp (q₂ a) n) =O[l] f
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasStrictFDerivAt.mul` -/
HasStrictFDerivAt.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c d : E → 𝔸'} {c' d' : E →L[𝕜] 𝔸'},
  HasStrictFDerivAt c c' x → HasStrictFDerivAt d d' x → HasStrictFDerivAt (fun i => c i * d i) (c x • d' + d x • c') x
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_subtypePerm : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (f : Equiv.Perm α) (h : ∀ (x : α), f x ∈ s ↔ x ∈ s),
  (f.subtypePerm h).support = {x | f ↑x ≠ ↑x}
-- Mathlib.Algebra.Field.Basic
/-- See `inv_sub_inv` for the more convenient version when `K` is commutative.  -/
inv_sub_inv' : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, a ≠ 0 → b ≠ 0 → a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
-- Mathlib.Topology.NhdsKer
nhdsKer_minimal : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → IsOpen t → nhdsKer s ⊆ t
-- Mathlib.RingTheory.Flat.Localization
IsSMulRegular.of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [IsLocalization p S] {x : R}, IsSMulRegular R x → IsSMulRegular S ((algebraMap R S) x)
-- Init.Data.SInt.Lemmas
ISize.mul_succ : ∀ {a b : ISize}, a * (b + 1) = a * b + a
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.mk : {ρ : Type} →
  {pat : ρ} → {s : String.Slice} → s.Pos → String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instHasPropCarrierToTop : ∀ (P : TopCat → Prop) (X : CompHausLike P), CompHausLike.HasProp P ↑X.toTop
-- Mathlib.GroupTheory.Commensurable
/-- For `H` a subgroup of `G`, this is the subgroup of all elements `g : G`
such that `Commensurable (g H g⁻¹) H`  -/
Subgroup.Commensurable.commensurator : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instInhabitedTrie : {α : Type} → Inhabited (Lean.Meta.RefinedDiscrTree.Trie α)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.of_isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsPrenex
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_coe_dFinsupp : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (x : Π₀ (i : n), A i),
  CoalgebraStruct.comul ⇑x =
    (TensorProduct.map (DFinsupp.coeFnLinearMap R) (DFinsupp.coeFnLinearMap R)) (CoalgebraStruct.comul x)
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_apply : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  (Algebra.trace R S) x = (LinearMap.trace R S) ((Algebra.lmul R S) x)
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eq_cons_cons : ∀ {R : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : SMul R M] {r₁ r₂ : R} (m : M)
  {l₁ l₂ : Mathlib.Tactic.Module.NF R M}, r₁ = r₂ → l₁.eval = l₂.eval → ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAddMonoid : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → AddMonoid (E →ₛₗ.[σ] F)
-- Mathlib.Data.Finset.Option
Finset.eraseNone_inter : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] [inst_1 : DecidableEq α] (s t : Finset (Option α)),
  Finset.eraseNone (s ∩ t) = Finset.eraseNone s ∩ Finset.eraseNone t
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The one point compactification of a `T0Space` space is a `T0Space`.  -/
OnePoint.instT0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X], T0Space (OnePoint X)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_eq_intCast : ∀ {R : Type u_1} [inst : Ring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℤ), SkewPolynomial.C ↑n = ↑n
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app._auto_1)
  {Z : Cᵒᵖ} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)
      h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X).unop).op
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op
        h)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (promise : IO.Promise Bool) (waiter : Option (Std.Async.Waiter (Option α))),
  sizeOf { promise := promise, waiter := waiter } = 1 + sizeOf promise + sizeOf waiter
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- The inner dual of inner dual of a proper cone is itself.  -/
ProperCone.innerDual_innerDual : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
  (C : ProperCone ℝ E), ProperCone.innerDual ↑(ProperCone.innerDual ↑C) = C
-- Aesop.Stats.Report
_private.Aesop.Stats.Report.0.Aesop.StatsReport.default.fmtTime : Aesop.Nanos → ℕ → Std.Format
-- Mathlib.Probability.Independence.Basic
/-- A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a
measure `μ` (typically defined on a finer σ-algebra) if the family of sets of measurable sets they
define is independent. `m : ι → MeasurableSpace Ω` is independent with respect to measure `μ` if
for any finite set of indices `s = {i_1, ..., i_n}`, for any sets
`f i_1 ∈ m i_1, ..., f i_n ∈ m i_n`, then `μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i)`.  -/
ProbabilityTheory.iIndep : {Ω : Type u_1} →
  {ι : Type u_2} →
    (ι → MeasurableSpace Ω) →
      {_mΩ : MeasurableSpace Ω} → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndep._auto_1 → Prop
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.not_sOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder 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.WSameSide x y → ¬s.SOppSide x y
-- Std.Data.DTreeMap.Internal.Queries
/-- The smallest key of `t`. Returns the given fallback value if the map is empty.  -/
Std.DTreeMap.Internal.Impl.minKey! : {α : Type u} → {β : α → Type v} → [Inhabited α] → Std.DTreeMap.Internal.Impl α β → α
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool) (i : ℕ), (x.concat b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → t.maxKey?.isSome = true
-- Mathlib.RingTheory.Smooth.Pi
Algebra.FormallySmooth.of_pi : ∀ {R : Type u_1} {I : Type u_2} (A : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] [Algebra.FormallySmooth R ((i : I) → A i)] (i : I),
  Algebra.FormallySmooth R (A i)
-- Mathlib.Data.Num.Basic
/-- Converts an `Int` to a `ZNum`.  -/
ZNum.ofInt' : ℤ → ZNum
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_lt_ofReal_iff_of_nonneg : ∀ {p q : ℝ}, 0 ≤ p → (ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.infix_of_le : ∀ {p q : DyckWord}, p ≤ q → ↑p <:+: ↑q
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors.eq_1 : ArithmeticFunction.cardDistinctFactors =
  { toFun := fun n => n.primeFactorsList.dedup.length, map_zero' := ArithmeticFunction.cardDistinctFactors._proof_1 }
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.lt_iff_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a < f b ↔ a < b)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.toAssocList.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : List (α × β) → Sort u_3) →
      (x : List (α × β)) →
        (Unit → motive []) → ((a : α) → (b : β) → (es : List (α × β)) → motive ((a, b) :: es)) → motive x
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inclusion_mapId : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (x : CategoryTheory.Bicategory.Pith B),
  (CategoryTheory.Bicategory.Pith.inclusion B).mapId x = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id x).of
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_bitVecToNat : ∀ (n : BitVec System.Platform.numBits), USize.ofNatClamp n.toNat = { toBitVec := n }
-- Init.Data.BitVec.Lemmas
BitVec.slt_eq_decide : ∀ {w : ℕ} {x y : BitVec w}, x.slt y = decide (x.toInt < y.toInt)
-- Mathlib.Order.Interval.Finset.Defs
/-- Note we define `Icc (toDual a) (toDual b)` as `Icc α _ _ b a` (which has type `Finset α` not
`Finset αᵒᵈ`!) instead of `(Icc b a).map toDual.toEmbedding` as this means the
following is defeq:
```
lemma this : (Icc (toDual (toDual a)) (toDual (toDual b)) :) = (Icc a b :) := rfl
```
 -/
OrderDual.instLocallyFiniteOrder : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → LocallyFiniteOrder αᵒᵈ
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_mono : ∀ {G : Type u_1} [inst : Group G] (n : ℕ), Monotone fun S => S.lowerCentralSeries n
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
/-- The L2 norm of the cross product of two real vectors (of type `Fin 3 → R`) equals the product
of their individual L2 norms times the sine of the angle between them.  -/
InnerProductGeometry.norm_toLp_symm_crossProduct : ∀ (a b : Fin 3 → ℝ),
  ‖WithLp.toLp 2 ((crossProduct a) b)‖ =
    ‖WithLp.toLp 2 a‖ * ‖WithLp.toLp 2 b‖ * Real.sin (InnerProductGeometry.angle (WithLp.toLp 2 a) (WithLp.toLp 2 b))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) → [addMon : CategoryTheory.AddMonObj X] → CategoryTheory.AddMon C
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instLawfulOrderLTNat : Std.LawfulOrderLT ℕ
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.exp (f x)) x
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopEquivalence_unitIso : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.unopEquivalence V c).unitIso = HomologicalComplex.unopUnitIso V c
-- Mathlib.RingTheory.Trace.Basic
algHomEquivSigma.eq_1 : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [inst : CommSemiring A] [inst_1 : CommSemiring C]
  [inst_2 : CommSemiring D] [inst_3 : Algebra A C] [inst_4 : Algebra A D] [inst_5 : CommSemiring B]
  [inst_6 : Algebra A B] [inst_7 : Algebra B C] [inst_8 : IsScalarTower A B C],
  algHomEquivSigma =
    { toFun := fun f => ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩,
      invFun := fun fg =>
        have x := fg.fst.toAlgebra;
        AlgHom.restrictScalars A fg.snd,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_addXYZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_lt_of_forall_not_threeAPFree : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {n : ℕ},
  (∀ t ∈ Finset.powersetCard n s, ¬ThreeAPFree ↑t) → addRothNumber s < n
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.varName : {α : Type} → Lean.ParserCompiler.Context α → Lean.Name
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_19 : HAdd Std.Time.Minute.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_sub : ∀ {a b : ISize} (h : System.Platform.numBits = 32), (a - b).toBitVec32 h = a.toBitVec32 h - b.toBitVec32 h
-- Mathlib.CategoryTheory.Action.Limits
Action.res_additive : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {H : Type u_4} [inst_3 : Monoid H] (f : G →* H), (Action.res V f).Additive
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricSMul.to_continuousConstSMul : ∀ (M : Type u) (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X],
  ContinuousConstSMul M X
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
OrderDual.borelSpace : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [h : BorelSpace α], BorelSpace αᵒᵈ
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.mk.sizeOf_spec : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1} [inst : SizeOf α]
  (inner : Std.TreeMap.Raw α Unit cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
`∑ b ∈ s, f b`.  -/
hasSum_sum_support_of_ne_finset_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {s : Finset β},
  (∀ b ∈ L.support, b ∉ s → f b = 0) →
    ∀ [L.HasSupport] [inst_3 : DecidablePred fun x => x ∈ L.support], HasSum f (∑ b ∈ (↑s ∩ L.support).toFinset, f b) L
-- Init.SimpLemmas
let_congr : ∀ {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β},
  a = a' →
    (∀ (x : α), b x = b' x) →
      (have x := a;
        b x) =
        have x := a';
        b' x
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_3.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) → ((x : ℕ) → motive 0 x) → ((a : ℕ) → motive 1 a) → ((n a : ℕ) → motive n.succ.succ a) → motive x x_1
-- Mathlib.MeasureTheory.Measure.Restrict
ae_restrict_iff_subtype : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂MeasureTheory.Measure.comap Subtype.val μ, p ↑x
-- Mathlib.RingTheory.Perfection
PreTilt.coeff_pow_p : ∀ {O : Type u₂} [inst : CommRing O] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (x : PreTilt O p)
  (n : ℕ), (PreTilt.coeff (n + 1)) x ^ p = (PreTilt.coeff n) x
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_mul_Iic : ∀ {a : ℝ}, 0 < a → ∀ (c : ℝ), ∫ (x : ℝ) in Set.Iic c, Real.exp (a * x) = Real.exp (a * c) / a
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Inhabited M], ArchimedeanOrder.instInhabited = { default := ArchimedeanOrder.of default }
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_inter_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  Finset.Ioc a b ∩ Finset.Ioc c d = Finset.Ioc (max a c) (min b d)
-- Mathlib.Algebra.Order.Quantale
Quantale.leftMulResiduation_le_iff_mul_le : ∀ {α : Type u_1} {x y z : α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  x ≤ Quantale.leftMulResiduation y z ↔ x * y ≤ z
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.ae_mem_imp_eq_mk : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {s : Set α} (h : AEMeasurable f (μ.restrict s)),
  ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEMeasurable.mk f h x
-- Mathlib.CategoryTheory.Action.Monoidal
Action.rightDual_v : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {H : Type u_3} [inst_2 : Group H] (X : Action V H) [inst_3 : CategoryTheory.RightRigidCategory V], Xᘁ.V = X.Vᘁ
-- Mathlib.GroupTheory.Submonoid.Center
AddOpposite.op_mem_center_iff : ∀ {M : Type u_2} [inst : Add M] {x : M}, AddOpposite.op x ∈ Set.addCenter Mᵃᵒᵖ ↔ x ∈ Set.addCenter M
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_iff_contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, s ∈ nhds x → (ContDiffWithinAt 𝕜 n f s x ↔ ContDiffAt 𝕜 n f x)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.threeShortAddLongRoot_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2],
  RootPairing.EmbeddedG2.threeShortAddLongRoot P =
    3 • RootPairing.EmbeddedG2.shortRoot P + RootPairing.EmbeddedG2.longRoot P
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_of : ∀ {α : Type u} (a : α), ↑(FreeRing.of a) = FreeCommRing.of a
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = 0
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqHost.beq : Std.Http.Header.Host → Std.Http.Header.Host → Bool
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_add_Ici_eq : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] [AddRightMono α] {a b : α},
  Set.Ici a + Set.Ici b = Set.Ici (a + b)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.polynomial : ∀ (ι : Type u) (R : Type u_1) [inst : CommRing R] [Nonempty ι] [Subsingleton ι],
  IsTranscendenceBasis R fun x => Polynomial.X
-- Mathlib.Topology.Order.IntermediateValue
/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if `f(a) ≤ f(b)`.  -/
ContinuousOn.strictMonoOn_of_injOn_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a ≤ b → f a ≤ f b → ContinuousOn f (Set.Icc a b) → Set.InjOn f (Set.Icc a b) → StrictMonoOn f (Set.Icc a b)
-- Aesop.Script.CtorNames
/-- Whether the constructor has at least one implicit argument.  -/
Aesop.CtorNames.hasImplicitArg : Aesop.CtorNames → Bool
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppImplicitCore.mkNamedArg : Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Lean.Elab.DocString
/-- In module mode, docstring extensions are invoked at elaboration time, so the underlying definition
must be marked `meta`.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.checkDocExtMeta : Lean.Name → String → Lean.CoreM Unit
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.exists_ne_zero_of_setIntegral_ne_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X) in t, f x ∂[B; μ] ≠ 0 → ∃ x ∈ t, f x ≠ 0
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableOn_proj : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  {s : Set (Bundle.TotalSpace F E)}, MDiff[s] Bundle.TotalSpace.proj
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLT! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α → α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.step_append : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] {it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  (it₁.append it₂).step = do
    let __do_lift ← it₁.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it₁' out, h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (it₁'.append it₂) out ⋯))
      | ⟨Std.IterStep.skip it₁', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (it₁'.append it₂) ⋯))
      | ⟨Std.IterStep.done, h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.appendSnd α₁ it₂) ⋯))