mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
/-- Given a normed group hom `f : V → W` with `W` complete, this provides a lift of `f` to
the completion of `V`. The lemmas `lift_unique` and `lift_comp_incl` provide the api for the
universal property of the completion.  -/
SemiNormedGrp.completion.lift : {V W : SemiNormedGrp} → [CompleteSpace W.carrier] → [T0Space W.carrier] → (V ⟶ W) → (SemiNormedGrp.completion.obj V ⟶ W)
-- Std.Http.Data.Version
Std.Http.Version.v20.sizeOf_spec : sizeOf Std.Http.Version.v20 = 1
-- Lean.Elab.Tactic.Try
/-- Executes a tactic with heartbeat management:
- Restores the original maxHeartbeats limit (recorded at try? start)
- Gives the tactic a fresh heartbeat budget via withCurrHeartbeats
- Catches heartbeat exceptions and converts them to regular errors
 -/
Lean.Elab.Tactic.Try.withOriginalHeartbeats : {α : Type} → Lean.Elab.Tactic.Try.TryTacticM α → Lean.Elab.Tactic.Try.TryTacticM α
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_mk : ∀ (z : ℂ) (hz : ‖z‖ ≤ 1), ↑(Complex.UnitClosedDisc.mk z hz) = z
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.instEquivLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G},
  GroupExtension.Equiv.instEquivLike =
    { coe := fun equiv => ⇑equiv.toMulEquiv, inv := fun equiv => ⇑equiv.symm, left_inv := ⋯, right_inv := ⋯,
      coe_injective' := ⋯ }
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_self : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∨ P ⊣⊢ₛ P
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.instIsIsoHomFullSubcategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X ⟶ Y) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom
-- Mathlib.Algebra.Group.Basic
div_ne_one_of_ne : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a ≠ b → a / b ≠ 1
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_lt_encard_iff_dep_of_finite : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  X.Finite → autoParam (X ⊆ M.E) Matroid.eRk_lt_encard_iff_dep_of_finite._auto_1 → (M.eRk X < X.encard ↔ M.Dep X)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₀.X₂ =
    CategoryTheory.Limits.kernel (CategoryTheory.CategoryStruct.comp f g)
-- Batteries.Data.Stream
/-- Inner loop for `Stream.takeTR`.  -/
Std.Stream.takeTR.loop : {σ : Type u_1} → {α : Type u_2} → [Std.Stream σ α] → σ → List α → ℕ → List α × σ
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.opEquiv_apply : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), AddSubgroup.opEquiv H = H.op
-- Mathlib.NumberTheory.Dioph
Dioph.of_no_dummies : ∀ {α : Type u} (S : Set (α → ℕ)) (p : Poly α), (∀ (v : α → ℕ), v ∈ S ↔ p v = 0) → Dioph S
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (s : P.obj (Opposite.op X)) {Y : C} (f : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaEquiv.symm s).app (Opposite.op Y)))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f) =
    (CategoryTheory.ConcreteCategory.hom (P.map f.op)) s
-- Mathlib.RingTheory.PowerSeries.Basic
/-- `R⟦X⟧` is notation for `PowerSeries R`,
the semiring of formal power series in one variable over a semiring `R`.
 -/
PowerSeries.«term_⟦X⟧» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] →
                            (𝕜' : Type u_1) →
                              [inst_11 : Semiring 𝕜'] →
                                [inst_12 : Module 𝕜' F] →
                                  [ContinuousConstSMul 𝕜' F] →
                                    [SMulCommClass 𝕜 𝕜' F] → Module 𝕜' (FormalMultilinearSeries 𝕜 E F)
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.lintegral_condKernel_mem : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  {s : Set (β × Ω)}, MeasurableSet s → ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ρ s
-- Mathlib.SetTheory.ZFC.PSet
/-- The von Neumann ordinal ω  -/
PSet.omega : PSet.{u_1}
-- Std.Do.WP.SimpLemmas
OptionT.tryCatch.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : OptionT m α) (handle : PUnit.{u_1} → OptionT m α),
  x.tryCatch handle =
    OptionT.mk do
      let __x ← x
      match __x with
        | some a => pure (some a)
        | x => handle PUnit.unit
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.map : ∀ {m : Type u → Type v} {Pred EPred : Type 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] {α β : Type u}
  {post : β → Pred} {epost : EPred} (f : α → β) (x : m α),
  ⦃ Std.Internal.Do.wp x (fun a => post (f a)) epost ⦄ f <$> x ⦃ post; epost ⦄
-- Mathlib.RingTheory.Conductor
/-- This technical lemma tells us that if `C` is the conductor of `R<x>` and `I` is an ideal of `R`
then `p * (I * S) ⊆ I * R<x>` for any `p` in `C ∩ R`  -/
prod_mem_ideal_map_of_mem_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  {p : R} {z : S},
  p ∈ Ideal.comap (algebraMap R S) (conductor R x) →
    z ∈ Ideal.map (algebraMap R S) I →
      (algebraMap R S) p * z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
-- Init.Grind.Ring.Basic
Lean.Grind.CommRing.toCommSemiring : {α : Type u} → [self : Lean.Grind.CommRing α] → Lean.Grind.CommSemiring α
-- Mathlib.Data.NNRat.Defs
NNRat.natCast_eq_divNat : ∀ (n : ℕ), ↑n = NNRat.divNat n 1
-- Mathlib.Data.Rat.NatSqrt.Defs
Nat.lt_ratSqrt_add_inv_prec_sq : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
-- Mathlib.Algebra.BigOperators.Pi
/-- decomposing `x : ι → R` as a sum along the canonical basis  -/
pi_eq_sum_univ : ∀ {ι : Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι] {R : Type u_8} [inst_2 : NonAssocSemiring R] (x : ι → R),
  x = ∑ i, x i • fun j => if i = j then 1 else 0
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_induction_on : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {M N : Submodule R A} {C : A → Prop} {r : A},
  r ∈ M * N → (∀ m ∈ M, ∀ n ∈ N, C (m * n)) → (∀ (x y : A), C x → C y → C (x + y)) → C r
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))],
  (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit =
    {
      app := fun Y =>
        (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj Y
              (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)).symm
          (CategoryTheory.CategoryStruct.id
            (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)),
      naturality := ⋯ }
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly : BEq Lean.Grind.Linarith.Poly
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- `rpow` version of `Multiset.prod_map_pow` for `ℝ≥0`.  -/
NNReal.multiset_prod_map_rpow : ∀ {ι : Type u_1} (s : Multiset ι) (f : ι → NNReal) (r : ℝ),
  (Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `none` if the set is empty.
 -/
Std.ExtTreeSet.min? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Option α
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.Hom.hom.eq_1 : ∀ {X Y : AddMagmaCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- An alternative definition of the additive valuation, taking units into account  -/
IsDiscreteValuationRing.addVal_def' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (u : Rˣ) {ϖ : R},
  Irreducible ϖ → ∀ (n : ℕ), (IsDiscreteValuationRing.addVal R) (↑u * ϖ ^ n) = ↑n
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} {S : ι → AddSubgroup G}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Init.Data.Function
Function.RightInverse.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β), Function.RightInverse g f = Function.LeftInverse f g
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_map : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : Zero β] {f : α → β},
  f 0 = 0 → ∀ {d : n → α}, (Matrix.diagonal d).map f = Matrix.diagonal fun m => f (d m)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.connected_sup : ∀ {V : Type u} {G : SimpleGraph V} {H K : G.Subgraph},
  H.Preconnected → K.Preconnected → (H ⊓ K).verts.Nonempty → (H ⊔ K).Connected
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f)
    AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing S] → (I : Ideal R) → [Algebra S R] → Algebra S (AdicCompletion I R)
-- Mathlib.Data.Matrix.Block
/-- A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish  -/
Matrix.IsTwoBlockDiagonal : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → [Zero α] → Matrix (n ⊕ o) (l ⊕ m) α → Prop
-- Mathlib.Data.List.Basic
List.exists_mem_iff_getElem : ∀ {α : Type u} {l : List α} {p : α → Prop}, (∃ x ∈ l, p x) ↔ ∃ i, ∃ (x : i < l.length), p l[i]
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Commutative convolution semiring structure on linear maps from a cocommutative coalgebra to an
algebra.  -/
LinearMap.convCommSemiring : {R : Type u_1} →
  {A : Type u_3} →
    {C : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid C] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R C] →
                [inst_5 : Coalgebra R C] → [Coalgebra.IsCocomm R C] → CommSemiring (WithConv (C →ₗ[R] A))
-- Mathlib.Order.CompleteLattice.Lemmas
sup_iInf_le_iInf_sup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (a : α), a ⊔ ⨅ i, f i ≤ ⨅ i, a ⊔ f i
-- Mathlib.Data.NNReal.Basic
NNReal.coe_mulSingle : ∀ {α : Type u_2} [inst : DecidableEq α] (a : α) (b : NNReal) (c : α), ↑(Pi.mulSingle a b c) = Pi.mulSingle a (↑b) c
-- Mathlib.Data.PEquiv
/-- A `PEquiv` is a partial equivalence, a representation of a bijection between a subset
  of `α` and a subset of `β`. See also `PartialEquiv` for a version that requires `toFun` and
`invFun` to be globally defined functions and has `source` and `target` sets as extra fields.  -/
PEquiv : Type u → Type v → Type (max u v)
-- ProofWidgets.Component.FilterDetails
/-- The `FilterDetails` component is like a `<details>` HTML element,
but also has a filter button
that allows you to switch between filtered and unfiltered states.  -/
ProofWidgets.FilterDetails : ProofWidgets.Component ProofWidgets.FilterDetailsProps
-- Init.Data.String.Slice
String.Slice.SplitIterator.atEnd : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → String.Slice.SplitIterator pat s
-- Mathlib.Topology.UniformSpace.Completion
/-- Hausdorff completion of `α`  -/
UniformSpace.Completion : (α : Type u_1) → [UniformSpace α] → Type u_1
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curry_uncurryRight : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G),
  f.uncurryRight.curryRight = f
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.StrictMono.mk_comp_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f : (n : ℕ) → R →+* S ⧸ I ^ a n)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S] {n : ℕ},
  (Ideal.Quotient.mk (I ^ a n)).comp (IsAdicComplete.StrictMono.liftRingHom I ha f ⋯) = f n
-- Mathlib.MeasureTheory.PiSystem
/-- A nonempty finite intersection of sets in a π-system belongs to the π-system.  -/
IsPiSystem.biInter_mem : ∀ {α : Type u_1} {S : Set (Set α)},
  IsPiSystem S → ∀ {t : Finset (Set α)}, t.Nonempty → (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
-- Mathlib.Algebra.Group.Shrink
Shrink.instAdd.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α], Shrink.instAdd = (equivShrink α).symm.add
-- Lean.Data.Lsp.Basic
/-- Params for JSON-RPC method `$/progress` request.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#progress)  -/
Lean.Lsp.ProgressParams : Type → Type
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.mk'.congr_simp : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : DecidableEq ι] (f f_1 : ((i : ι) → M₁ i) → M₂) (e_f : f = f_1)
  (h₁ :
    ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
  (h₂ :
    ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c • x)) = c • f (Function.update m i x)),
  MultilinearMap.mk' f h₁ h₂ = MultilinearMap.mk' f_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.mono_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C] {ι : Type u_1} [Finite ι]
  {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (i : CategoryTheory.Discrete ι), CategoryTheory.Mono (c.ι.app i)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → UpperSet α),
  (⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`, then
`fun x ↦ f x * r` tends to negative infinity if and only if `0 < r`.  -/
Filter.tendsto_mul_const_atBot_iff_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ 0 < r)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result : Type
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_enorm_add_right : ∀ {α : Type u_1} {ε' : Type u_5} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε'] [inst_1 : TopologicalSpace ε''] [inst_2 : ESeminormedAddMonoid ε''] (f : α → ε') {g : α → ε''},
  MeasureTheory.AEStronglyMeasurable g μ →
    ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ
-- Std.Http.Data.Request
/-- Adds a header to the request being built only if the Option Header.Value is some.
 -/
Std.Http.Request.Builder.headerOpt : Std.Http.Request.Builder → Std.Http.Header.Name → Option Std.Http.Header.Value → Std.Http.Request.Builder
-- Mathlib.CategoryTheory.Shift.Localization
/-- The localization functor `W.Q : C ⥤ W.Localization` is compatible with the shift.  -/
CategoryTheory.MorphismProperty.commShift_Q : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] → [inst_3 : W.IsCompatibleWithShift A] → W.Q.CommShift A
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.kerLiftAlg_toRingHom : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (f : A →ₐ[R₁] B), ↑(Ideal.kerLiftAlg f) = (↑f).kerLift
-- Init.Data.List.Lemmas
List.getLast?_eq_head?_reverse : ∀ {α : Type u_1} {xs : List α}, xs.getLast? = xs.reverse.head?
-- Mathlib.Topology.EMetricSpace.Basic
/-- **Alias** of the forward direction of `EMetric.inseparable_iff`. -/
Inseparable.edist_eq_zero : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Inseparable x y → edist x y = 0
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.tsum_G2Term_eq_tsum : ∀ (z : UpperHalfPlane),
  ∑' (m : Fin 2 → ℤ), EisensteinSeries.G2Term✝ z m = ∑' (m : ℤ) (n : ℤ), EisensteinSeries.G2Term✝ z ![m, n]
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivWithinAt_iff_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x ↔ (fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhdsWithin x s] fun x' => x' - x
-- Mathlib.Order.Defs.PartialOrder
Preorder.toLE : {α : Type u_2} → [self : Preorder α] → LE α
-- Mathlib.Probability.Process.LocalProperty
/-- A pre-localizing sequence is a sequence of stopping times that tends almost surely to
infinity.  -/
ProbabilityTheory.IsPreLocalizingSequence : {ι : Type u_1} →
  {Ω : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        [inst_1 : TopologicalSpace ι] →
          [OrderTopology ι] →
            MeasureTheory.Filtration ι mΩ →
              (ℕ → Ω → WithTop ι) →
                autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreLocalizingSequence._auto_1 → Prop
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`, then
the function is `C`-Lipschitz. Version with `HasFDerivWithinAt`.  -/
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E}
  {f' : E → E →L[𝕜] G},
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    (∀ x ∈ s, ‖f' x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_all : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ}
  (φ : L.BoundedFormula α (k + 1)),
  FirstOrder.Language.BoundedFormula.relabel g φ.all = (FirstOrder.Language.BoundedFormula.relabel g φ).all
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_nat_iff_fintype : ∀ {α : Type u} {n : ℕ}, Cardinal.mk α = ↑n ↔ ∃ h, Fintype.card α = n
-- Mathlib.NumberTheory.AbelSummation
_private.Mathlib.NumberTheory.AbelSummation.0.summable_mul_of_bigO_atTop_aux : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (m : ℕ),
  ((fun n => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 0 n, ‖c k‖) =O[Filter.atTop] fun x => 1) →
    MeasureTheory.LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑m) MeasureTheory.volume →
      (∀ (n : ℕ),
          ∑ k ∈ Finset.Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
            ‖f ↑n‖ * ∑ k ∈ Finset.Icc 0 n, ‖c k‖ -
              ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, ‖c k‖) →
        ∀ {g : ℝ → ℝ},
          (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop] g →
            MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume → Summable fun n => f ↑n * c n
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.image_comap_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M),
  CategoryTheory.SubmonoidFunctor.image S.ι (CategoryTheory.SubmonoidFunctor.comap S.ι S) = S
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {J' : Type w'}
  [inst_5 : LinearOrder J'] [inst_6 : SuccOrder J'] [inst_7 : OrderBot J'] [inst_8 : WellFoundedLT J'] (e : J ≃o J'),
  W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J'
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.postponedSafeRule.inj : ∀ {r r_1 : Aesop.PostponedSafeRule},
  Aesop.UnsafeQueueEntry.postponedSafeRule r = Aesop.UnsafeQueueEntry.postponedSafeRule r_1 → r = r_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.min?.isSome = true
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat : Lean.Expr →
  ℕ →
    Lean.Meta.Grind.Arith.Linear.LinExpr →
      Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_mul_single_subset : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G] (r : k) (a : G),
  (f * SkewMonoidAlgebra.single a r).support ⊆ Finset.image (fun x => x * a) f.support