mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- The natural `R`-linear equivalence between the two ways to represent an invariant submodule.  -/
Module.AEval.equiv_mapSubmodule : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [inst_6 : IsScalarTower R A M] →
                      (p : Submodule R M) →
                        (hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule) →
                          ↥p ≃ₗ[R] ↥((Module.AEval.mapSubmodule R M a) ⟨p, hp⟩)
-- Mathlib.Topology.Algebra.FilterBasis
/-- The topological space structure coming from a group filter basis.  -/
GroupFilterBasis.topology : {G : Type u} → [inst : Group G] → GroupFilterBasis G → TopologicalSpace G
-- Aesop.Rule.Name
Aesop.BuilderName.unfold : Aesop.BuilderName
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_isLoop_iff_mem_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, (M.contract C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.normal.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a a_1 : Λ),
  (Turing.TM2to1.Λ'.normal a = Turing.TM2to1.Λ'.normal a_1) = (a = a_1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.mk.injEq : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type w) (X : I → C)
  (coversTop : J.CoversTop X) (generators : (i : I) → (M.over (X i)).GeneratingSections) (I_1 : Type w) (X_1 : I_1 → C)
  (coversTop_1 : J.CoversTop X_1) (generators_1 : (i : I_1) → (M.over (X_1 i)).GeneratingSections),
  ({ I := I, X := X, coversTop := coversTop, generators := generators } =
      { I := I_1, X := X_1, coversTop := coversTop_1, generators := generators_1 }) =
    (I = I_1 ∧ X ≍ X_1 ∧ generators ≍ generators_1)
-- Std.Time.Zoned.Database.TzIf
/-- The data for version 1 of the TZif file.
 -/
Std.Time.TimeZone.TZif.TZif.v1 : Std.Time.TimeZone.TZif.TZif → Std.Time.TimeZone.TZif.TZifV1
-- Mathlib.Order.Minimal
minimal_mem_iff : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {s : Set α},
  Minimal (fun x => x ∈ s) x ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → y ≤ x → x = y
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.cast_skipPrefixWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy), (s.skipPrefixWhile pat).cast hst = t.skipPrefixWhile pat
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAtFilter_add_const_iff`. -/
HasFDerivAtFilter.add_const : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} (c : F), HasFDerivAtFilter f f' L → HasFDerivAtFilter (fun x => f x + c) f' L
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.isIrreducible_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} (φ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α),
  ProbabilityTheory.Kernel.IsIrreducible φ κ ↔
    ∀ ⦃A : Set α⦄, MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ n, ((κ ^ n) a) A > 0
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNatClamp_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.commutes : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} {inst : Group G} {inst_1 : CommSemiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra A B} {inst_4 : MulSemiringAction G B} [self : IsGaloisGroup G A B], SMulCommClass G A B
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_symm : ∀ {α : Type u_1}, FreeAddMonoid.ofList.symm = FreeAddMonoid.toList
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instPreservesEpimorphismsKaroubiToKaroubi : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.toKaroubi C).PreservesEpimorphisms
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- Avoid using this and use the induction principle on `M ⊗[R] N` instead.  -/
TensorProduct.exists_sum_tmul_eq : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  ∃ k m n, x = ∑ j, m j ⊗ₜ[R] n j
-- Mathlib.Analysis.Matrix.PosDef
Matrix.PosDef.det_pos : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  A.PosDef → 0 < A.det
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.embedding.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] (𝒜 : ι → σ) (x : Submonoid A)
  (p : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x p = Localization.mk ↑p.num ⟨↑p.den, ⋯⟩
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
affineSpan_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P} {Q : AffineSubspace k P}, affineSpan k s ≤ Q ↔ s ⊆ ↑Q
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan_inj_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D) (j : J) {Z : D}
  (h : (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Cofan.inj (CategoryTheory.GradedObject.mapBifunctorRightUnitorCofan F Y e p hp X j)
        ⟨(j, 0), ⋯⟩)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
        (e.hom.app (X j)))
      h
-- Lean.Expr
Lean.Expr.mvarId! : Lean.Expr → Lean.MVarId
-- Mathlib.Analysis.Convex.Topology
closedConvexHull_min : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s t : Set E},
  s ⊆ t → Convex 𝕜 t → IsClosed t → (closedConvexHull 𝕜) s ⊆ t
-- Lean.Elab.DeclNameGen
/-- Core algorithm for generating a name. The provided expression should be a winnowed expression.

- `omitTopForall` if true causes "Forall" to not be included if the binding type results in an empty string.
 -/
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore : Lean.Expr → optParam Bool false → Lean.Elab.Command.NameGen.MkNameM✝ String
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C},
  h.homEquiv =
    { toFun := fun f => (t.extend f).π, invFun := fun π => h.lift { pt := W, π := π }, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Array.Lemmas
/-- Variant of `filterMap_reverse` with a hypothesis giving the stop condition.  -/
Array.filterMap_reverse' : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {stop : ℕ},
  stop = xs.size → Array.filterMap f xs.reverse 0 stop = (Array.filterMap f xs).reverse
-- Mathlib.CategoryTheory.GlueData
/-- The map `D.U i ⟶ D.glued` for each `i`.  -/
CategoryTheory.GlueData.ι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] → (i : D.J) → D.U i ⟶ D.glued
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
/-- A set of `finrank R M` vectors forms a basis if they span the whole space,
provided `R` satisfies the Orzech property.  -/
setBasisOfTopLeSpanOfCardEqFinrank : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [OrzechProperty R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {s : Set M} →
              [inst_4 : Fintype ↑s] →
                ⊤ ≤ Submodule.span R s → s.toFinset.card = Module.finrank R M → Module.Basis (↑s) R M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar : ℕ → Type
-- Mathlib.ModelTheory.Definability
Set.Definable.sdiff : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s t : Set (α → M)},
  A.Definable L s → A.Definable L t → A.Definable L (s \ t)
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps.mk : Lean.Name → GoToModuleLinkProps
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X), p.yonedaEquivFst = CategoryTheory.yonedaEquiv p.fst
-- Init.Data.Nat.Lemmas
Nat.pow_eq_zero : ∀ {a n : ℕ}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Transversal.mk.sizeOf_spec : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} [inst_2 : SizeOf ι] [inst_3 : (a : ι) → SizeOf (G a)] [inst_4 : SizeOf H]
  (injective : ∀ (i : ι), Function.Injective ⇑(φ i)) (set : (i : ι) → Set (G i)) (one_mem : ∀ (i : ι), 1 ∈ set i)
  (compl : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set i)),
  sizeOf { injective := injective, set := set, one_mem := one_mem, compl := compl } = 1
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- Two Gaussian measures are equal if they have same mean and same covariance.  -/
ProbabilityTheory.IsGaussian.ext_covarianceBilinDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : NormedSpace ℝ E]
  {ν : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [ProbabilityTheory.IsGaussian ν],
  ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν →
    ProbabilityTheory.covarianceBilinDual μ = ProbabilityTheory.covarianceBilinDual ν → μ = ν
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
/-- The natural homeomorphism between nonzero elements of a normed space `E`
and `Metric.sphere (0 : E) r × Set.Ioi (0 : ℝ)`, `0 < r`.

The forward map sends `⟨x, hx⟩` to `⟨r • ‖x‖⁻¹ • x, ‖x‖ / r⟩`,
the inverse map sends `(x, r)` to `r • x`.

In the case of the unit sphere `r = `,
one may think about it as generalization of polar coordinates to any normed space.  -/
homeomorphSphereProd : (E : Type u_2) →
  [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (r : ℝ) → 0 < r → ↑{0}ᶜ ≃ₜ ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.cosZeta_zero : HurwitzZeta.cosZeta 0 = riemannZeta
-- Mathlib.Analysis.Fourier.FourierTransform
/-- For any `w`, the Fourier integral is convergent iff `f` is integrable.  -/
VectorFourier.fourierIntegral_convergent_iff : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] [inst_8 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
  [inst_10 : TopologicalSpace V] [BorelSpace V] [inst_12 : TopologicalSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜},
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      ∀ {f : V → E} (w : W), MeasureTheory.Integrable (fun v => e (-(L v) w) • f v) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.Data.ENat.Basic
ENat.mul_le_mul_of_le_right : ∀ {a x y : ℕ∞}, x ≤ y → a ≠ 0 → a ≠ ⊤ → x * a ≤ y * a
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.analyticOn : ∀ {𝕜 : 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}, ContDiffWithinAt 𝕜 ⊤ f s x → ∃ u ∈ nhdsWithin x (insert x s), AnalyticOn 𝕜 f u
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve ((F.comp G).obj X)),
  CategoryTheory.Sieve.functorPullback (F.comp G) R =
    CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPullback G R)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.condExp_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] {a b : ℕ},
  a ≤ b →
    ∀ {x₀ : (i : ↥(Finset.Iic a)) → X ↑i} {f : ((n : ℕ) → X n) → E},
      MeasureTheory.Integrable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
        ((ProbabilityTheory.Kernel.traj κ a) x₀)[f |
            ↑MeasureTheory.Filtration.piLE b] =ᵐ[(ProbabilityTheory.Kernel.traj κ a) x₀]
          fun x => ∫ (y : (n : ℕ) → X n), f y ∂(ProbabilityTheory.Kernel.traj κ b) (Preorder.frestrictLe b x)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filterMapWithPostcondition : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1}
  {o : Type w → Type u_2} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o]
  [inst_5 : Std.Do.WPMonad o ps] [inst_6 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_9 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterMapWithPostcondition f it) init g ⦃Q⦄
-- Mathlib.Data.ULift
ULift.rec_update : ∀ {α : Type u} {β : ULift.{u_2, u} α → Type u_1} [inst : DecidableEq α] (f : (a : α) → β { down := a }) (a : α)
  (x : β { down := a }),
  (fun t => ULift.rec (Function.update f a x) t) = Function.update (fun t => ULift.rec f t) { down := a } x
-- Mathlib.Data.Finset.Insert
Finset.toList_cons : ∀ {α : Type u_1} {a : α} {s : Finset α} (h : a ∉ s), (Finset.cons a s h).toList.Perm (a :: s.toList)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict derivative in both limits for a locally finite
measure.

Let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of
`intervalIntegral.FTCFilter`s around `a`; let `(lb, lb')` be a pair of `intervalIntegral.FTCFilter`s
around `b`. Suppose that `f` has finite limits `ca` and `cb` at `la' ⊓ ae μ` and `lb' ⊓ ae μ`,
respectively.
Then `∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ =
  ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ +
    o(‖∫ x in ua..va, (1:ℝ) ∂μ‖ + ‖∫ x in ub..vb, (1:ℝ) ∂μ‖)`
as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`.
 -/
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ}
  {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {ua va ub vb : ι → ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f μ a b →
    StronglyMeasurableAtFilter f la' μ →
      StronglyMeasurableAtFilter f lb' μ →
        Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (nhds ca) →
          Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (nhds cb) →
            Filter.Tendsto ua lt la →
              Filter.Tendsto va lt la →
                Filter.Tendsto ub lt lb →
                  Filter.Tendsto vb lt lb →
                    (fun t =>
                        ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
                          (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
                      fun t => ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanIntNorm_localization : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I : Ideal S),
  ∀ M ≤ nonZeroDivisors R,
    ∀ {Rₘ : Type u_4} (Sₘ : Type u_5) [inst_9 : CommRing Rₘ] [inst_10 : Algebra R Rₘ] [inst_11 : CommRing Sₘ]
      [inst_12 : Algebra S Sₘ] [inst_13 : Algebra Rₘ Sₘ] [inst_14 : Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ]
      [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
      [inst_19 : IsIntegrallyClosed Rₘ] [inst_20 : IsDomain Rₘ] [inst_21 : IsDomain Sₘ]
      [inst_22 : Module.IsTorsionFree Rₘ Sₘ] [inst_23 : Module.Finite Rₘ Sₘ] [inst_24 : IsIntegrallyClosed Sₘ],
      Ideal.spanNorm Rₘ (Ideal.map (algebraMap S Sₘ) I) = Ideal.map (algebraMap R Rₘ) (Ideal.spanNorm R I)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.inhabited : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                [inst_3 : Inhabited (CategoryTheory.Comma L R)] →
                  Inhabited (CategoryTheory.CommaMorphism default default)
-- Mathlib.Data.ZMod.Defs
ZMod.commRing : (n : ℕ) → CommRing (ZMod n)
-- Mathlib.Algebra.DirectSum.Ring
/-- The `NonUnitalNonAssocRing` derived from `GNonUnitalNonAssocSemiring A`.  -/
DirectSum.instNonUnitalNonAssocRingOfNat : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommGroup (A i)] →
        [inst_1 : AddZeroClass ι] → [DirectSum.GNonUnitalNonAssocSemiring A] → NonUnitalNonAssocRing (A 0)
-- Std.Time.Zoned.Database.TzIf
/-- Represents version 1 of the TZif format.
 -/
Std.Time.TimeZone.TZif.TZifV1 : Type
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instRing : {d : ℤ} → Ring (ℤ√d)
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.pnatCast : {R : Type u_1} → [inst : CommRing R] → [Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] → ℕ+ → Rˣ
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.mapNeighborSet_symm_apply_coe : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (v : V)
  (w : ↑(G'.neighborSet (f v))), ↑((f.mapNeighborSet v).symm w) = f.symm ↑w
-- Lean.CoreM
Lean.Core.getMaxHeartbeats : Lean.Options → ℕ
-- Mathlib.AlgebraicGeometry.Spec
/-- Spec, as a contravariant functor from commutative rings to presheafed spaces.
 -/
AlgebraicGeometry.Spec.toPresheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (AlgebraicGeometry.PresheafedSpace CommRingCat)
-- Mathlib.Algebra.Group.Even
isSquare_inv : ∀ {α : Type u_2} [inst : DivisionMonoid α] {a : α}, IsSquare a⁻¹ ↔ IsSquare a
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsDeterministicDeterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f),
  ProbabilityTheory.IsDeterministic (ProbabilityTheory.Kernel.deterministic f hf)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Legendre's Theorem**

The `p`-adic valuation of `n!` is the sum of the quotients `n / p ^ i`. This sum is expressed
over the finset `Ico 1 b` where `b` is any bound greater than `log p n`.  -/
padicValNat_factorial : ∀ {p n b : ℕ} [hp : Fact (Nat.Prime p)], Nat.log p n < b → padicValNat p n.factorial = ∑ i ∈ Finset.Ico 1 b, n / p ^ i
-- Init.Data.Rat.Lemmas
Rat.pow_succ : ∀ (q : ℚ) (n : ℕ), q ^ (n + 1) = q ^ n * q
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_smul_set_inv : ∀ {α : Type u_2} [inst : Group α] {a b : α} {s : Set α}, a ∈ b • s⁻¹ ↔ b ∈ a • s
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instEmptyCollection : EmptyCollection AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_hom_leftUnitor : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = ↑(TensorProduct.lid R ↑M)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.post : Lean.Meta.Simp.Methods → Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function is 'meromorphic in normal form' on `U` if has normal form at every
point of `U`.
 -/
MeromorphicNFOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → Set 𝕜 → Prop
-- Mathlib.Data.Sum.Basic
Sum.inl_injective : ∀ {α : Type u} {β : Type v}, Function.Injective Sum.inl
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_base_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : B),
  φ.leftUnitor.hom.base.app X = CategoryTheory.CategoryStruct.id (φ.base.obj X)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.Quotient.mk_smul_out : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] (H : Subgroup G)
  [inst_3 : MulAction.QuotientAction X H] (b : X) (q : G ⧸ H), ↑(b • Quotient.out q) = b • q
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_iff_tendsto : ∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
  (∀ (x : α), g x = 0 → f x = 0) → (f =o[l] g ↔ Filter.Tendsto (fun x => f x / g x) l (nhds 0))