mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.ofOption.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.RingTheory.Derivation.ToSquareZero
/-- If `f₁ f₂ : A →ₐ[R] B` are two lifts of the same `A →ₐ[R] B ⧸ I`,
we may define a map `f₁ - f₂ : A →ₗ[R] I`.  -/
diffToIdealOfQuotientCompEq : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal B) →
                  (f₁ f₂ : A →ₐ[R] B) → (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂ → A →ₗ[R] ↥I
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.plaintext : String → Lean.Lsp.InlayHintTooltip
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
AddMonCat.forget_isCorepresentable : (CategoryTheory.forget AddMonCat).IsCorepresentable
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_expect : ∀ {K : Type u_1} [inst : RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ),
  ↑(s.expect fun i => f i) = s.expect fun i => ↑(f i)
-- Init.Data.Vector.Count
Vector.count_empty : ∀ {α : Type u_1} [inst : BEq α] {a : α}, Vector.count a #v[] = 0
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.mk.injEq : ∀ (unfolds : Lean.NameMap Lean.Meta.SimpTheorem) (casts : Lean.NameMap (Lean.Name × Lean.Name))
  (insertionFuns : Lean.NameSet) (unfolds_1 : Lean.NameMap Lean.Meta.SimpTheorem)
  (casts_1 : Lean.NameMap (Lean.Name × Lean.Name)) (insertionFuns_1 : Lean.NameSet),
  ({ unfolds := unfolds, casts := casts, insertionFuns := insertionFuns } =
      { unfolds := unfolds_1, casts := casts_1, insertionFuns := insertionFuns_1 }) =
    (unfolds = unfolds_1 ∧ casts = casts_1 ∧ insertionFuns = insertionFuns_1)
-- Mathlib.Logic.Equiv.Defs
EquivLike.self_comp_coe_symm : ∀ {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (e : F), ⇑e ∘ ⇑(↑e).symm = id
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Roo α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Roo α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.MapLinearEquiv.isAddHaarMeasure : ∀ {𝕜 : Type u_1} {G : Type u_2} {H : Type u_3} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace H]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : TopologicalSpace G] [inst_4 : TopologicalSpace H]
  [inst_5 : AddCommGroup G] [inst_6 : AddCommGroup H] [IsTopologicalAddGroup G] [IsTopologicalAddGroup H]
  [inst_9 : Module 𝕜 G] [inst_10 : Module 𝕜 H] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G]
  [BorelSpace H] [CompleteSpace 𝕜] [T2Space G] [FiniteDimensional 𝕜 G] [ContinuousSMul 𝕜 G] [ContinuousSMul 𝕜 H]
  [T2Space H] (e : G ≃ₗ[𝕜] H), (MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- A functor preserves identity morphisms.  -/
CategoryTheory.ReflPrefunctor.map_id : ∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  (self : V ⥤rq W) (X : V), self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)
-- Mathlib.Control.Monad.Cont
ContT.run_contT_map_contT : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : ContT r m α), (ContT.map f x).run = f ∘ x.run
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_odd : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  preNormEDS b c d (2 * m + 1) =
    (preNormEDS b c d (m + 2) * preNormEDS b c d m ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (m - 1) * preNormEDS b c d (m + 1) ^ 3 * if Even m then 1 else b
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : X.OpenCover),
  (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_iff_tendsto : ∀ {𝕜 : 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} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x ↔
    Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (nhdsWithin x s) (nhds 0)
-- Lean.Level
Lean.Level.PP.Result.brecOn_1.go : {motive_1 : Lean.Level.PP.Result → Sort u} →
  {motive_2 : List Lean.Level.PP.Result → Sort u} →
    (t : List Lean.Level.PP.Result) →
      ((t : Lean.Level.PP.Result) → t.below → motive_1 t) →
        ((t : List Lean.Level.PP.Result) → Lean.Level.PP.Result.below_1 t → motive_2 t) →
          motive_2 t ×' Lean.Level.PP.Result.below_1 t
-- Mathlib.Topology.Constructions
isOpenMap_toAdd : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑Multiplicative.toAdd
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.support 0 = ∅
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_eq_empty : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C : ConvexCone R M}, ↑C = ∅ ↔ C = ⊥
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.hasStrictDerivAt_log_of_pos : ∀ {x : ℝ}, 0 < x → HasStrictDerivAt Real.log x⁻¹ x
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedGroup.disjoint_nhds : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E) (f : Filter E),
  Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖
-- Mathlib.Analysis.Normed.Module.Bases
/-- The vector `e_n` lies in the range of the operator `succSub P n = P (n+1) - P n`.  -/
SchauderBasis.RankOneDecomposition.e_mem_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X) (n : ℕ),
  self.e n ∈ (↑(SchauderBasis.succSub self.P n)).range
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grindSeq1Indented : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toHomeomorph_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, f.toHomeomorph = g.toHomeomorph ↔ f = g
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ext_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt)
  (h :
    autoParam (∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i)
      CategoryTheory.Limits.Multifork.ext._auto_1),
  (CategoryTheory.Limits.Multifork.ext e h).inv.hom = e.inv
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_union_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∩ (t ∪ s) = s
-- Mathlib.Data.Multiset.Defs
Multiset.card_strictMono : ∀ {α : Type u_1}, StrictMono Multiset.card
-- Lean.Expr
Lean.Expr.updateFVar! : Lean.Expr → Lean.FVarId → Lean.Expr
-- Mathlib.Data.Set.Sups
Set.infs_inter_subset_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s₁ s₂ t : Set α}, (s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.instGroup : {X : Type u_1} → [inst : PseudoEMetricSpace X] → Group (X ≃ᵈ X)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.coe_mulActionHom_of_embedding : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  (f : Fin n ↪ α), ↑((Set.powersetCard.mulActionHom_of_embedding G α n).toFun f) = Finset.map f Finset.univ
-- Mathlib.Order.Shrink
instOrderTopShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [inst_1 : Preorder α] → [OrderTop α] → OrderTop (Shrink.{u, u_1} α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_string_empty : ∀ {s : String.Slice}, s.endsWith "" = true
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
/-- **Gauss' lemma**. The Legendre symbol can be computed by considering the number of naturals less
than `p/2` such that `(a * x) % p > p / 2`.  -/
ZMod.gauss_lemma : ∀ {p : ℕ} [h : Fact (Nat.Prime p)] {a : ℤ},
  p ≠ 2 → ↑a ≠ 0 → legendreSym p a = (-1) ^ {x ∈ Finset.Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}.card
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.IsLocalizationMap.surj : ∀ {M : Type u_1} [inst : AddCommMonoid M] {N : Type u_2} [inst_1 : AddCommMonoid N] {S : AddSubmonoid M} {f : M → N},
  S.IsLocalizationMap f → ∀ (z : N), ∃ x, z + f ↑x.2 = f x.1
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mk.sizeOf_spec : ∀ {R : Type u_3} [inst : CommSemiring R] {A : Type u_4} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_5} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toAlgHom : A →ₐ[R] B)
  (cont : autoParam (Continuous (↑↑toAlgHom.toRingHom).toFun) ContinuousAlgHom.cont._autoParam),
  sizeOf { toAlgHom := toAlgHom, cont := cont } = 1 + sizeOf toAlgHom + sizeOf cont
-- Init.Data.UInt.Lemmas
UInt32.mul_neg : ∀ (a b : UInt32), a * -b = -(a * b)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_lt_rpow : ∀ {x z : ℝ}, 1 < x → 0 < z → 1 < x ^ z
-- Mathlib.Algebra.Polynomial.Roots
/-- A monic polynomial `p` that has as many roots as its degree
can be written `p = ∏(X - a)`, for `a` in `p.roots`.  -/
Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p.Monic → p.roots.card = p.natDegree → (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
-- Init.Data.Array.Basic
/-- Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no
such element is found.

Examples:
* `#[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
* `#[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
Array.findRev? : {α : Type} → (α → Bool) → Array α → Option α
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_of_forall_one_lt_le_mul : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α]
  {a b : α}, (∀ (ε : α), 1 < ε → a ≤ b * ε) → a ≤ b
-- Mathlib.Order.Filter.Pointwise
Filter.inv_le_inv : ∀ {α : Type u_2} [inst : Inv α] {f g : Filter α}, f ≤ g → f⁻¹ ≤ g⁻¹
-- Mathlib.Algebra.Lie.Basic
/-- Lie module equivalences are transitive.  -/
LieModuleEquiv.trans : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        {P : Type w₂} →
          [inst : CommRing R] →
            [inst_1 : LieRing L] →
              [inst_2 : AddCommGroup M] →
                [inst_3 : AddCommGroup N] →
                  [inst_4 : AddCommGroup P] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R P] →
                          [inst_8 : LieRingModule L M] →
                            [inst_9 : LieRingModule L N] →
                              [inst_10 : LieRingModule L P] → (M ≃ₗ⁅R,L⁆ N) → (N ≃ₗ⁅R,L⁆ P) → M ≃ₗ⁅R,L⁆ P
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'.wf.congr_simp : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift lift_1 : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ),
  lift = lift_1 →
    ∀ (γ : Type x) (PlausibleForInStep : β → γ → ForInStep γ → Prop)
      (wf : Std.IteratorLoop.WellFounded α m PlausibleForInStep) (it it_1 : Std.IterM m β) (e_it : it = it_1)
      (init init_1 : γ),
      init = init_1 →
        ∀ (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
          (f f_1 : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
          f = f_1 →
            Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it init P hP f =
              Std.IterM.DefaultConsumers.forIn'.wf lift_1 γ PlausibleForInStep wf it_1 init_1 P ⋯ f_1
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub_nf : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ - o₂).NF
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.mk.injEq : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [inst_2 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (vec : aig.RefVec w) (aig_1 : Std.Sat.AIG α) (vec_1 : aig_1.RefVec w),
  ({ aig := aig, vec := vec } = { aig := aig_1, vec := vec_1 }) = (aig = aig_1 ∧ vec ≍ vec_1)
-- Init.Internal.Order.Basic
Lean.Order.instCCPOReaderT : {m : Type u_1 → Type u_2} → {ρ α : Type u_1} → [inst : Lean.Order.CCPO (m α)] → Lean.Order.CCPO (ReaderT ρ m α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey ⋯ =
    t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k'
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Induction principle for weighted homogeneous polynomials.  -/
MvPolynomial.IsWeightedHomogeneous.induction_on : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M}
  {motive : (p : MvPolynomial σ R) → MvPolynomial.IsWeightedHomogeneous w p m → Prop},
  motive 0 ⋯ →
    (∀ (p q : MvPolynomial σ R) (hp : MvPolynomial.IsWeightedHomogeneous w p m)
        (hq : MvPolynomial.IsWeightedHomogeneous w q m), motive p hp → motive q hq → motive (p + q) ⋯) →
      (∀ (d : σ →₀ ℕ) (r : R) (hr : (Finsupp.weight w) d = m), motive ((MvPolynomial.monomial d) r) ⋯) →
        ∀ {p : MvPolynomial σ R} (hp : MvPolynomial.IsWeightedHomogeneous w p m), motive p hp
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNonUnitalNormedCommRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : NonUnitalNormedCommRing R] → NonUnitalNormedCommRing (BoundedContinuousFunction α R)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- An equalizer of an idempotent morphism and the identity is split mono.  -/
CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {f : X ⟶ X} →
        CategoryTheory.CategoryStruct.comp f f = f →
          {c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f} →
            CategoryTheory.Limits.IsLimit c → CategoryTheory.SplitMono c.ι
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_neg_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Neg Z] [inst_4 : ContinuousNeg Z] (f : C(X × Y, Z)) (x : X),
  (-f).curry x = -f.curry x
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.mk.sizeOf_spec : ∀ (id method : String) (registerOptions : Option Lean.Json),
  sizeOf { id := id, method := method, registerOptions := registerOptions } =
    1 + sizeOf id + sizeOf method + sizeOf registerOptions
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup = inferInstance
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {s t : T}, ProbabilityTheory.HasGaussianLaw (fun ω => (X s ω, X t ω)) P
-- Std.Http.Data.Body.Any
Std.Http.Body.Any.mk.sizeOf_spec : ∀ (recv : Std.Async.Async (Option Std.Http.Chunk)) (close : Std.Async.Async Unit) (isClosed : Std.Async.Async Bool)
  (recvSelector : Std.Async.Selector (Option Std.Http.Chunk))
  (tryRecv : Std.Async.Async (Option (Option Std.Http.Chunk)))
  (getKnownSize : Std.Async.Async (Option Std.Http.Body.Length))
  (setKnownSize : Option Std.Http.Body.Length → Std.Async.Async Unit),
  sizeOf
      { recv := recv, close := close, isClosed := isClosed, recvSelector := recvSelector, tryRecv := tryRecv,
        getKnownSize := getKnownSize, setKnownSize := setKnownSize } =
    1 + sizeOf recvSelector
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [Lean.Grind.NoNatZeroDivisors α] (ctx : Lean.Grind.Linarith.Context α)
  (k₁ k₂ : ℤ) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_diseq_subst_cert k₁ k₂ p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ ≠ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ ≠ 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inl_XIsoBiprod_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) h
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_iff_infinite_of_neg : ∀ {x : ℝ*}, x < 0 → (x.InfiniteNeg ↔ x.Infinite)
-- Mathlib.Algebra.Category.Grp.Zero
AddGrpCat.isZero_of_iff_subsingleton : ∀ {G : Type u_1} [inst : AddGroup G], CategoryTheory.Limits.IsZero (AddGrpCat.of G) ↔ Subsingleton G
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.refl : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] (f : α → E) (l : Filter α), f =Θ[𝕜; l] f
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.ae_isMeasurablyGenerated : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, (MeasureTheory.ae μ).IsMeasurablyGenerated
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Let `S` be an `S₀`-algebra. Then the category of `S`-modules is `S₀`-linear.
 -/
ModuleCat.Algebra.instLinear : {S₀ : Type u₀} →
  [inst : CommSemiring S₀] → {S : Type u} → [inst_1 : Ring S] → [Algebra S₀ S] → CategoryTheory.Linear S₀ (ModuleCat S)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.alter m k f) k' fallback =
    if (k == k') = true then (f (Std.DHashMap.Const.get? m k)).getD fallback else Std.DHashMap.Const.getD m k' fallback
-- Init.Meta.Defs
Lean.Name.isInaccessibleUserName : Lean.Name → Bool
-- Init.Data.List.Lemmas
/-- Variant of `append_inj` instead requiring equality of the lengths of the second lists.  -/
List.append_inj' : ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂ ∧ t₁ = t₂
-- Mathlib.CategoryTheory.Countable
CategoryTheory.instCountableCategoryNat : CategoryTheory.CountableCategory ℕ
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
jacobiTheta_eq_jacobiTheta₂ : ∀ (τ : ℂ), jacobiTheta τ = jacobiTheta₂ 0 τ
-- Std.Http.Data.Status
Std.Http.Status.imUsed.sizeOf_spec : sizeOf Std.Http.Status.imUsed = 1
-- Lean.Elab.Tactic.Grind.Annotated
/-- Check if a module has been marked as grind-annotated.  -/
Lean.Elab.Tactic.Grind.isGrindAnnotatedModule : Lean.Environment → Lean.ModuleIdx → Bool
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.map_swap_antidiagonal : ∀ {A : Type u_1} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A},
  Finset.map { toFun := Prod.swap, inj' := ⋯ } (Finset.HasAntidiagonal.antidiagonal n) =
    Finset.HasAntidiagonal.antidiagonal n
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_coeff : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : PolynomialModule R M), { coeff := x.coeff } = x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsEquivOfQuotEquiv_symm`. -/
idealFactorsEquivOfQuotEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J),
  (IsDedekindDomain.idealFactorsEquivOfQuotEquiv f).symm = IsDedekindDomain.idealFactorsEquivOfQuotEquiv f.symm
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousOn_iff_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} [inst_1 : TopologicalSpace β],
  UpperHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `Kᗮ` can be characterized as the intersection of the kernels of the operations of
inner product with each of the elements of `K`.  -/
ClosedSubmodule.orthogonal_eq_inter : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), ↑Kᗮ = ⨅ v, (↑((innerSL 𝕜) ↑v)).ker
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_mul_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R), (x * y).cardSupp ≤ x.cardSupp * y.cardSupp
-- Mathlib.CategoryTheory.Join.Basic
/-- A natural isomorphism `Fᵣ ≅ Gᵣ` induces a natural isomorphism
`mapPair H Fᵣ ≅ mapPair H Gᵣ` for every `H : C ⥤ E`.  -/
CategoryTheory.Join.mapIsoWhiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (H : CategoryTheory.Functor C E) →
                  {Fᵣ Gᵣ : CategoryTheory.Functor D E'} →
                    (Fᵣ ≅ Gᵣ) → (CategoryTheory.Join.mapPair H Fᵣ ≅ CategoryTheory.Join.mapPair H Gᵣ)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.split.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] (s : String.Slice) (pat : ρ)
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ],
  s.split pat = Std.Iter.map String.Slice.Subslice.toSlice (s.splitToSubslice pat)
-- Mathlib.Data.Finset.Range
/-- `range n` is the set of natural numbers less than `n`.  -/
Finset.range : ℕ → Finset ℕ