mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fin.Tuple.Basic
/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly.  -/
Fin.update_cons_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (z : α 0),
  Function.update (Fin.cons x p) 0 z = Fin.cons z p
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.adhesive_of_reflective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Adhesive C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.HasPushouts C]
  [H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g]
  {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan Gl], CategoryTheory.Adhesive D
-- Mathlib.Data.Nat.Fib.Zeckendorf
/-- A list of natural numbers is a Zeckendorf representation (of a natural number) if it is an
increasing sequence of non-consecutive numbers greater than or equal to `2`.

This is relevant for Zeckendorf's theorem, since if we write a natural `n` as a sum of Fibonacci
numbers `(l.map fib).sum`, `IsZeckendorfRep l` exactly means that we can't simplify any expression
of the form `fib n + fib (n + 1) = fib (n + 2)`, `fib 1 = fib 2` or `fib 0 = 0` in the sum.  -/
List.IsZeckendorfRep : List ℕ → Prop
-- Mathlib.Order.Monotone.Basic
strictMonoOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s ↔ StrictMonoOn f s
-- Lean.DocString.Extension
/-- Removes a builtin docstring from the compiler. This is used when translating between formats.
 -/
Lean.removeBuiltinDocString : Lean.Name → IO Unit
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofComp_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (i : ι' ⊕ ι),
  (Q.ofComp P).val i = Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange.eq_1 : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (p : Submodule R M),
  Submodule.baseChange A p = (LinearMap.baseChange A p.subtype).range
-- Aesop.Forward.Match.Types
Aesop.instHashableCompleteMatch.hash : Aesop.CompleteMatch → UInt64
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with subtraction.  -/
ContDiffAt.laplacianWithin_sub_nhdsWithin : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E},
  ContDiffWithinAt ℝ 2 f₁ s x →
    ContDiffWithinAt ℝ 2 f₂ s x →
      UniqueDiffOn ℝ s →
        x ∈ s →
          InnerProductSpace.laplacianWithin (f₁ - f₂) s =ᶠ[nhdsWithin x s]
            InnerProductSpace.laplacianWithin f₁ s - InnerProductSpace.laplacianWithin f₂ s
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_neg : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)), c +ᵥ -f = -(c +ᵥ f)
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- `rfl` is true if `proof` is by `Eq.refl`, `rfl` or a `@[defeq]` theorem.
 -/
Lean.Meta.SimpTheorem.rfl : Lean.Meta.SimpTheorem → Bool
-- Init.Data.SInt.Lemmas
Int8.ofIntLE.congr_simp : ∀ (i i_1 : ℤ) (e_i : i = i_1) (_hl : Int8.minValue.toInt ≤ i) (_hr : i ≤ Int8.maxValue.toInt),
  Int8.ofIntLE i _hl _hr = Int8.ofIntLE i_1 ⋯ ⋯
-- Init.Meta.Defs
/-- Filters an array of syntax, treating every other element as a separator rather than an element to
test with the monadic predicate `p`. The resulting array contains the tested elements for which `p`
returns `true`, separated by the corresponding separator elements.
 -/
Array.filterSepElemsM : {m : Type → Type} → [Monad m] → Array Lean.Syntax → (Lean.Syntax → m Bool) → m (Array Lean.Syntax)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntryD.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a), Std.DTreeMap.Internal.Impl.leaf.maxEntryD x = x
-- Mathlib.Tactic.SuccessIfFailWithMsg
/-- Evaluates `tacs` and succeeds only if `tacs` both fails and throws an error equal (as a string)
to `msg`.  -/
Mathlib.Tactic.successIfFailWithMessage : {s α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [MonadLiftT BaseIO m] →
        [MonadLiftT Lean.CoreM m] →
          [Lean.MonadBacktrack s m] →
            [Lean.MonadError m] →
              String → m α → optParam (Option Lean.Syntax) none → optParam (Option Lean.Syntax) none → m Unit
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.setOfPred_isNonloop_eq`. -/
Matroid.setOf_isNonloop_eq : ∀ {α : Type u_1} (M : Matroid α), {e | M.IsNonloop e} = M.E \ M.loops
-- Mathlib.Order.OrderIsoNat
/-- A stronger version of the **monotone chain** condition for partial orders.

See `wellFoundedGT_iff_monotone_chain_condition'` for a version on preorders.  -/
wellFoundedGT_iff_monotone_chain_condition : ∀ {α : Type u_1} [inst : PartialOrder α], WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitLeftOpIsoUnopColimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.limitLeftOpIsoUnopColimit F =
    CategoryTheory.Limits.limit.isoLimitCone
      { cone := CategoryTheory.Limits.coneLeftOpOfCocone (CategoryTheory.Limits.colimit.cocone F),
        isLimit := CategoryTheory.Limits.isLimitConeLeftOpOfCocone F (CategoryTheory.Limits.colimit.isColimit F) }
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₂_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] (x : E.I₀),
  (CategoryTheory.PreZeroHypercover.pullback₂ f E).f x = CategoryTheory.Limits.pullback.snd (E.f x) f
-- Mathlib.LinearAlgebra.InvariantBasisNumber
rankCondition_iff : ∀ (R : Type u) [inst : Semiring R],
  RankCondition R ↔ ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Surjective ⇑f → m ≤ n
-- Mathlib.Data.ENat.Pow
ENat.mul_epow : ∀ {x y z : ℕ∞}, (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction_rank : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (α : Type v) [inst : PartialOrder α] (f : P.RankFunction α) (a : ↑P.II),
  (SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction P α f).rank a = f.rank a
-- Init.Data.Vector.Lemmas
Vector.pop.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.pop = Vector.mk xs.toArray.pop ⋯
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_closure_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.eRk (M.closure X) = M.eRk X
-- Std.Data.TreeSet.Raw.Basic
/-- Computes the difference of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.TreeSet.Raw.diff : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp
-- Mathlib.Algebra.Algebra.TransferInstance
Equiv.algEquiv_symm_apply : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommSemiring R] (e : α ≃ β) [inst_1 : Semiring β]
  [inst_2 : Algebra R β] (b : β), (AlgEquiv.symm (Equiv.algEquiv R e)) b = e.symm b
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_interpolate_le : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  Set.InjOn v ↑s → ((Lagrange.interpolate s v) r).degree ≤ ↑(s.card - 1)
-- Mathlib.Algebra.Ring.Defs
/-- A commutative semiring is a semiring with commutative multiplication.  -/
CommSemiring : Type u → Type u
-- Mathlib.RingTheory.WittVector.Frobenius
/-- The polynomials that give the coefficients of `frobenius x`,
in terms of the coefficients of `x`.  -/
WittVector.frobeniusPoly : ℕ → ℕ → MvPolynomial ℕ ℤ
-- Init.Data.UInt.Basic
/-- The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
integer by another. Usually accessed via the `%` operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt8.mod 5 2 = 1`
* `UInt8.mod 4 2 = 0`
* `UInt8.mod 4 0 = 4`
 -/
UInt8.mod : UInt8 → UInt8 → UInt8
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly_eq_minpoly : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), FixedPoints.minpoly G F x = minpoly (↥(FixedPoints.subfield G F)) x
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The canonical morphism `K.truncLE' e ⟶ K.restriction e`.  -/
HomologicalComplex.truncLE'ToRestriction : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] → [inst_3 : ∀ (i' : ι'), K.HasHomology i'] → K.truncLE' e ⟶ K.restriction e
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_of_mem : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), s.indicator f a = f a
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instCompleteSpace : ∀ {A : Type u_3} {E : Type u_4} [inst : UniformSpace E] [CompleteSpace E], CompleteSpace (WithCStarModule A E)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_toEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑↑e = ⇑e
-- Mathlib.Data.PNat.Basic
PNat.add_sub_of_lt : ∀ {a b : ℕ+}, a < b → a + (b - a) = b
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.le_prod_of_submultiplicative_on_pred_of_nonneg : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {M : Type u_4}
  [inst_3 : CommMonoid M] (f : M → R) (p : M → Prop),
  (∀ (a : M), 0 ≤ f a) →
    f 1 ≤ 1 →
      (∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b) →
        (∀ (a b : M), p a → p b → p (a * b)) →
          ∀ (s : Finset ι) (g : ι → M), (∀ a ∈ s, p (g a)) → f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- An inverse function to `diracProba` (only really an inverse under hypotheses that
guarantee injectivity of `diracProba`).  -/
MeasureTheory.diracProbaInverse : {X : Type u_1} → [inst : MeasurableSpace X] → ↑(Set.range MeasureTheory.diracProba) → X
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_delete_contract_delete : ∀ {α : Type u_1} (M : Matroid α) (C D C' D' : Set α),
  Disjoint C' D → (((M.contract C).delete D).contract C').delete D' = (M.contract (C ∪ C')).delete (D ∪ D')
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₀.obj S = S.L₀
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) {F F' : CategoryTheory.Sheaf J (Type (max v v'))} (f : F ⟶ F')
  (x : F.obj.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f =
    J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) x)
-- Init.Data.Array.Zip
Array.unzip_replicate : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {a : α} {b : β},
  (Array.replicate n (a, b)).unzip = (Array.replicate n a, Array.replicate n b)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_dist_to_a_lt_deriv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 → ‖soln_gen✝ hnorm - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size =
      l.length
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.insertIdxIfInBounds.eq_1 : ∀ {α : Type u} (as : Array α) (i : ℕ) (a : α),
  as.insertIdxIfInBounds i a = if h : i ≤ as.size then as.insertIdx i a h else as
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.le_integral_rpowIntegrand₀₁_one : ∀ {p : ℝ}, p ∈ Set.Ioo 0 1 → -1 / (2 * (p - 1)) ≤ ∫ (t : ℝ) in Set.Ioi 0, p.rpowIntegrand₀₁ t 1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
MonotoneOn.sInf_image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {a b : α},
  a ≤ b → MonotoneOn f (Set.Icc a b) → sInf (f '' Set.Icc a b) = f a
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are subalgebras of `S / R`,
then `A` and `B` are linearly disjoint, if they are linearly disjoint as submodules of `S`.  -/
Subalgebra.LinearDisjoint : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → Subalgebra R S → Subalgebra R S → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKeyD_alter!_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).minKeyD fallback = k ↔
            (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Std.Data.TreeMap.Basic
Std.TreeMap.instMembership : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Membership α (Std.TreeMap α β cmp)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk_eq_bot : ∀ {M : Type u_1} [inst : MulOneClass M] (toSubsemigroup : Subsemigroup M) (one_mem' : 1 ∈ toSubsemigroup.carrier),
  { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊥ ↔ ↑toSubsemigroup = {1}
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.monotone_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F}, Monotone (AddSubmonoid.map f)
-- Mathlib.Analysis.Convex.Function
ConvexOn.comp_strictConvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConvexOn 𝕜 (f '' s) g → StrictConvexOn 𝕜 s f → StrictMonoOn g (f '' s) → StrictConvexOn 𝕜 s (g ∘ f)
-- Mathlib.MeasureTheory.Function.Jacobian
MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    MeasurableEmbedding f →
      ∀ {g : E → ℝ},
        (∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x) →
          MeasureTheory.IntegrableOn g (f '' s) μ →
            (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
              (MeasureTheory.Measure.comap f (μ.withDensity fun x => ENNReal.ofReal (g x))) s =
                ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- `MvPowerSeries.coeff` is continuous.  -/
MvPowerSeries.WithPiTopology.continuous_coeff : ∀ {σ : Type u_1} (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : Semiring R] (d : σ →₀ ℕ),
  Continuous ⇑(MvPowerSeries.coeff d)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyπ_naturality' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.π (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.π
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`.  -/
NonAssocSemiring.natCast_zero : ∀ {α : Type u} [self : NonAssocSemiring α], ↑0 = 0
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_le_card : ∀ {α : Type u_1} {f : α → α} {x : α} [inst : Fintype α], Function.minimalPeriod f x ≤ Fintype.card α
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of `Filter.tendsto_const_div_iff'`. -/
Filter.tendsto_const_div_iff : ∀ {G : Type w} {α : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun k => b / f k) l (nhds (b / c)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Data.Set.Opposite
Set.op_unop : ∀ {α : Type u_1} (s : Set α), s.op.unop = s
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- Given a presheaf of rings `R` on a cofiltered category, this is the
adjunction between `colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt`
and the constant functor.  -/
PresheafOfModules.colimitAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      [inst_2 : CategoryTheory.IsCofiltered C] →
        [inst_3 : CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              (hcR : CategoryTheory.Limits.IsColimit cR) →
                PresheafOfModules.colimitFunctor hcR ⊣ PresheafOfModules.constFunctor cR
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot_atBot_iff_of_monotone : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β}
  [inst_2 : Preorder β], Monotone f → (Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b)
-- Mathlib.Order.RelClasses
instIrreflGt : ∀ {α : Type u} [inst : Preorder α], Std.Irrefl fun x1 x2 => x2 < x1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X : C} {X₀ : C₀}
  (f : F.obj X₀ ⟶ X) {i : (data X).I₀} (p : F.obj X₀ ⟶ F.obj ((data X).X i)),
  CategoryTheory.CategoryStruct.comp p ((data X).f i) = f →
    CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p)
-- Init.SimpLemmas
iff_false : ∀ (p : Prop), (p ↔ False) = ¬p
-- Mathlib.Analysis.Convolution
/-- The convolution is continuous if one function is locally integrable and the other has compact
support and is continuous.  -/
HasCompactSupport.continuous_convolution_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G],
  HasCompactSupport g →
    MeasureTheory.LocallyIntegrable f μ → Continuous g → Continuous (MeasureTheory.convolution f g L μ)
-- Std.Time.Zoned.ZoneRules
/-- The abbreviation for this local time type (e.g., "EST", "PDT").
 -/
Std.Time.TimeZone.LocalTimeType.abbreviation : Std.Time.TimeZone.LocalTimeType → String
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instInhabited : {ι : Type u_1} → Inhabited (BoxIntegral.Box ι)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.suppPreservation_iff_isUniform : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F], MvQPF.SuppPreservation ↔ MvQPF.IsUniform
-- Aesop.Percent
Aesop.Percent.instLE : LE Aesop.Percent
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- Finds the strongly connected components of the graph `g`. Returns a hashmap where the value at
key `v` represents the SCC number containing vertex `v`. The numbering of SCCs is arbitrary.  -/
Mathlib.Tactic.Order.Graph.findSCCs : Mathlib.Tactic.Order.Graph → Std.HashMap ℕ ℕ
-- Lean.Parser.Extra
Lean.«termRegister_parser_alias(Kind:=_)______» : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `σₘ[A, B]` of two finsets `A` and `B` in a group is `|A / B| / |A|`.  -/
Combinatorics.Additive.«termδₘ[_,_]» : Lean.ParserDescr