mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.Do.Syntax
/-- After `mvcgen [...]`, there can be an optional `invariants` followed by either
* a bulleted list of invariants `· term; · term`.
* a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
  inaccessibles.
The tracing variant ` invariants? ` will suggest a skeleton for missing invariants; see the
docstring for `mvcgen`.
 -/
Lean.Parser.Tactic.invariantAlts : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_obj : ∀ (x : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.obj x =
    CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero
      CategoryTheory.Limits.WalkingParallelPair.one x
-- Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
/-- The isometry between a weighted sum of squares on an algebraically closed field and the
sum of squares, i.e. `weightedSumSquares` with weight `fun (i : ι) => 1`.  -/
QuadraticForm.isometryEquivSumSquaresUnits : {ι : Type u_1} →
  [inst : Fintype ι] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [IsAlgClosed K] →
          [DecidableEq K] →
            (w : ι → Kˣ) → (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K 1)
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated additive submonoids is finitely generated.  -/
AddSubmonoid.FG.prod : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] {P : AddSubmonoid M} {Q : AddSubmonoid N},
  P.FG → Q.FG → (P.prod Q).FG
-- Init.Data.Rat.Lemmas
Rat.le_ceil : ∀ {x : ℚ}, x ≤ ↑x.ceil
-- Init.Data.List.Sort.Basic
List.nil_merge : ∀ {α : Type u_1} {le : α → α → Bool} (ys : List α), [].merge ys le = ys
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Measurable.infEDist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α}, Measurable f → ∀ {s : Set α}, Measurable fun x => Metric.infEDist (f x) s
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withInDSimpWithCache : {α : Type} → (Lean.ExprStructMap Lean.Expr → Lean.Meta.SimpM (α × Lean.ExprStructMap Lean.Expr)) → Lean.Meta.SimpM α
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.induce_connectedComponent_isMatching : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph},
  M.IsPerfectMatching → ∀ (c : G.ConnectedComponent), (M.induce c.supp).IsMatching
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.map_add : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] [inst_2 : AddMonoid S]
  (f : R →+ S) {x y : HahnSeries Γ R}, (x + y).map f = x.map f + y.map f
-- Mathlib.Algebra.Group.Defs
mul_right_cancel_iff : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] {a b c : G}, b * a = c * a ↔ b = c
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map_δ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_4 : CategoryTheory.Preadditive D]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproducts D] {K L : CochainComplex C ℤ} (φ : K ⟶ L)
  (G : CategoryTheory.Functor C D) [inst_6 : G.Additive],
  CategoryTheory.CategoryStruct.comp
      ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
      ((CategoryTheory.Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app K) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapHomologicalComplexIso φ G).hom
      (CochainComplex.mappingCone.triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.mk'_eq_zero_iff_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] {x : R} {y : ↥(nonZeroDivisors R)}, IsLocalization.mk' K x y = 0 ↔ x = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
instIsRegularCardinalOrderNat : IsRegularCardinalOrder ℕ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.IsoLift.e : Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Algebra.Category.Grp.Ulift
CommGrpCat.uliftFunctor_preservesLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J CommGrpCat.uliftFunctor
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.functorIsoDiscreteAux₂.eq_1 : ∀ (R : Type (u + 1)) [inst : Ring R] (M : ModuleCat R),
  CondensedMod.LocallyConstant.functorIsoDiscreteAux₂ R M =
    (Condensed.discrete (ModuleCat R)).mapIso (CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ R M)
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Subset.decidable.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lists' α true → Lists' α true → Sort u_2) (b : Bool) (a : Lists' α b) (l₁ l₂ : Lists' α true)
  (h_1 : (x : Lists' α true) → motive Lists'.nil x)
  (h_2 : (b : Bool) → (a : Lists' α b) → (l₁ l₂ : Lists' α true) → motive (a.cons' l₁) l₂),
  (match a.cons' l₁, l₂ with
    | Lists'.nil, x => h_1 x
    | a.cons' l₁, l₂ => h_2 b a l₁ l₂) =
    h_2 b a l₁ l₂
-- Mathlib.Order.ModularLattice
inf_covBy_of_covBy_sup_of_covBy_sup_left : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ a
-- Mathlib.Probability.Kernel.Basic
/-- `ProbabilityTheory.Kernel.piecewise hs κ η` is the kernel equal to `κ` on the measurable set `s`
and to `η` on its complement.  -/
ProbabilityTheory.Kernel.piecewise : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {s : Set α} →
          [DecidablePred fun x => x ∈ s] →
            MeasurableSet s → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α β
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_eq_append : ∀ {n : ℕ}, 0 < n → (*...=n).toList = (*...=n - 1).toList ++ [n]
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_eq_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ Q 1 * P 2 → P 1 * Q 2 = W'.negY Q * P 2
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCOneHomOfOneHomClass.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [inst_3 : OneHomClass F M N], instCoeTCOneHomOfOneHomClass = { coe := OneHomClass.toOneHom }
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_add_right_eq_map : ∀ {m n : ℤ}, (m...m + n).toArray = Array.map (fun x => x + m) (0...n).toArray
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.stateful.injEq : ∀ (h h_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MCasesPat.stateful h = Lean.Parser.Tactic.MCasesPat.stateful h_1) = (h = h_1)
-- Mathlib.Probability.CondVar
/-- The integral of the conditional variance `Var[X | m]` over an `m`-measurable set is equal to
the integral of `(X - μ[X | m]) ^ 2` on that set.  -/
ProbabilityTheory.setIntegral_condVar : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {s : Set Ω}
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable ((X - μ[X | m]) ^ 2) μ →
    MeasurableSet s → ∫ (ω : Ω) in s, ProbabilityTheory.condVar m X μ ω ∂μ = ∫ (ω : Ω) in s, (X ω - μ[X | m] ω) ^ 2 ∂μ
-- Mathlib.Algebra.Star.Module
starLinearEquiv.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A], starLinearEquiv R = starLinearEquiv R
-- Mathlib.Data.PEquiv
PEquiv.self_trans_symm : ∀ {α : Type u} {β : Type v} (f : α ≃. β), f.trans f.symm = PEquiv.ofSet {a | (f a).isSome = true}
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_pow : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f : F →WOT[𝕜₂] F) (n : ℕ), (f ^ n).toCLM = f.toCLM ^ n
-- Lean.Declaration
Lean.ReducibilityHints.opaque : Lean.ReducibilityHints
-- Mathlib.Combinatorics.Graph.Basic
Graph.vertexSet_bouquet : ∀ {α : Type u_1} {β : Type u_2} (v : α) (edgeSet : Set β), (Graph.bouquet v edgeSet).vertexSet = {v}
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_pow_le : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x : S) (n : ℕ), ‖x ^ n‖₊ ≤ ‖x‖₊
-- Mathlib.Data.Multiset.Count
Multiset.count_eq_card : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, Multiset.count a s = s.card ↔ ∀ x ∈ s, a = x
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'.wf.induct_unfolding : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x)
  (PlausibleForInStep : β → γ → ForInStep γ → Prop) (wf : Std.IteratorLoop.WellFounded α m PlausibleForInStep)
  (P : β → Prop) (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c)))
  (motive : (it : Std.IterM m β) → γ → (∀ (b : β), it.IsPlausibleIndirectOutput b → P b) → n γ → Prop),
  (∀ (it : Std.IterM m β) (init : γ) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b),
      (∀ (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) (c : γ),
          PlausibleForInStep out init (ForInStep.yield c) →
            motive it' c ⋯ (Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' c P ⋯ f)) →
        (∀ (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it')),
            motive it' init ⋯ (Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' init P ⋯ f)) →
          motive it init hP
            (lift (Std.Shrink it.Step) γ
              (fun s =>
                match s.inflate with
                | ⟨Std.IterStep.yield it' out, h⟩ => do
                  let __do_lift ← f out ⋯ init
                  match __do_lift with
                    | ⟨ForInStep.yield c, property⟩ =>
                      Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' c P ⋯ f
                    | ⟨ForInStep.done c, property⟩ => pure c
                | ⟨Std.IterStep.skip it', h⟩ =>
                  Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' init P ⋯ f
                | ⟨Std.IterStep.done, property⟩ => pure init)
              it.step)) →
    ∀ (it : Std.IterM m β) (init : γ) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b),
      motive it init hP (Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it init P hP f)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_totalDegree_le : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂), (LinearMap.toMvPolynomial b₁ b₂ f i).totalDegree ≤ 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ1728_Δ : ∀ (R : Type u_1) [inst : CommRing R], (WeierstrassCurve.ofJ1728 R).Δ = -64
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRicSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRicSlice._auto_1) →
    Std.Ric.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RicSlice α)
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring module bracket is additive in its second component.  -/
LieRingModule.lie_add : ∀ {L : Type v} {M : Type w} {inst : LieRing L} {inst_1 : AddCommGroup M} [self : LieRingModule L M] (x : L) (m n : M),
  ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosStrictMono_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  MulPosStrictMono α ↔ ∀ ⦃c : α⦄, 0 < c → ∀ ⦃a b : α⦄, a < b → a * c < b * c
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.Quot
Quotient.eq_mk_iff_out : ∀ {α : Sort u_1} {s : Setoid α} {x : Quotient s} {y : α}, x = ⟦y⟧ ↔ x.out ≈ y
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- **Alias** of `CompHausLike.LocallyConstant.functor_obj_obj_obj`. -/
CompHausLike.LocallyConstant.functor_obj_obj : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : Type (max u w)) (x : (CompHausLike P)ᵒᵖ),
  ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.obj x = LocallyConstant (↑(Opposite.unop x).toTop) X
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.algebraMap_extendRightEquiv_symm : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (a : ↥(F.extendRight M)), (algebraMap (↥F) M) ((F.extendRightEquiv M).symm a) = ↑a
-- Mathlib.Tactic.Linarith.Lemmas
/-- Finds the name of a multiplicative lemma corresponding to an inequality strength.  -/
Mathlib.Ineq.toConstMulName : Mathlib.Ineq → Lean.Name
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.hasProjectiveDimensionLT_of_ge : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n m : ℕ),
  n ≤ m → ∀ [CategoryTheory.HasProjectiveDimensionLT X n], CategoryTheory.HasProjectiveDimensionLT X m
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.IsPrincipal.mk : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Submodule R M}, (∃ a, S = R ∙ a) → S.IsPrincipal
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.compactSet_ae : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.compactSet K =ᵐ[MeasureTheory.volume]
    ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
      closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K)
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.Irreducible.eq_minpoly : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B]
  {p : Polynomial A}, Irreducible p → (Polynomial.aeval x) p = 0 → p = Polynomial.C p.leadingCoeff * minpoly A x
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.compl₂_comp_linearEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} [inst_7 : AddCommMonoid N₁]
  [inst_8 : AddCommMonoid N₂] [inst_9 : Module R N₁] [inst_10 : Module R N₂],
  IsTensorProduct f → ∀ (e₁ : N₁ ≃ₗ[R] M₁) (e₂ : N₂ ≃ₗ[R] M₂), IsTensorProduct ((f ∘ₗ ↑e₁).compl₂ ↑e₂)
-- Mathlib.AlgebraicGeometry.Restrict
/-- `f.resLE U V` induces `f.appLE U V` on global sections.  -/
AlgebraicGeometry.arrowResLEAppIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (V : X.Opens) →
        (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) →
          CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Scheme.Hom.resLE f U V e)) ≅
            CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.appLE f U V e)
-- Mathlib.Order.Category.LinOrd
LinOrd.Hom.ext : ∀ {X Y : LinOrd} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Data.List.InsertIdx
List.insertIdx_eraseIdx_getElem : ∀ {α : Type u} {l : List α} {n : ℕ} (hn : n < l.length), (l.eraseIdx n).insertIdx n l[n] = l
-- Mathlib.Probability.Martingale.Centering
/-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
process. This is the martingale. See `predictablePart` for the predictable process.  -/
MeasureTheory.martingalePart : {Ω : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        {m0 : MeasurableSpace Ω} → (ℕ → Ω → E) → MeasureTheory.Filtration ℕ m0 → MeasureTheory.Measure Ω → ℕ → Ω → E
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciInf_set_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α} {a : α},
  s.Nonempty → BddBelow (f '' s) → (a ≤ ⨅ i, f ↑i ↔ ∀ i ∈ s, a ≤ f i)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.tendsto_atTop_iff : ∀ {x : ℝ*}, Filter.Germ.Tendsto x Filter.atTop ↔ 0 < x ∧ ArchimedeanClass.mk x < 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_def : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α},
  s.inf f = (Multiset.map f s.val).inf
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.aestronglyMeasurable : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  [SecondCountableTopology X], MeasureTheory.LocallyIntegrable f μ → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.ModelTheory.FinitelyGenerated
/-- A substructure of `M` is countably generated if it is the closure of a countable subset of `M`.
 -/
FirstOrder.Language.Substructure.CG : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → L.Substructure M → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.functorExt_hom_app : ∀ {J : CategoryTheory.Limits.MultispanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C}
  (left :
    (i : J.L) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.left i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.left i))
  (right :
    (i : J.R) →
      F.obj (CategoryTheory.Limits.WalkingMultispan.right i) ≅ G.obj (CategoryTheory.Limits.WalkingMultispan.right i))
  (wl :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i))
            (right (J.fst i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_1)
  (wr :
    autoParam
      (∀ (i : J.L),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i))
            (right (J.snd i)).hom =
          CategoryTheory.CategoryStruct.comp (left i).hom (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i)))
      CategoryTheory.Limits.WalkingMultispan.functorExt._auto_3)
  (X : CategoryTheory.Limits.WalkingMultispan J),
  (CategoryTheory.Limits.WalkingMultispan.functorExt left right wl wr).hom.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left i => left i
      | CategoryTheory.Limits.WalkingMultispan.right i => right i).hom
-- Mathlib.Algebra.DirectSum.Module
/-- Every linear map from a direct sum agrees with the one obtained by applying
the universal property to each of its components.  -/
DirectSum.toModule.unique : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {N : Type u₁} [inst_4 : AddCommMonoid N]
  [inst_5 : Module R N] (ψ : (DirectSum ι fun i => M i) →ₗ[R] N) (f : DirectSum ι fun i => M i),
  ψ f = (DirectSum.toModule R ι N fun i => ψ ∘ₗ DirectSum.lof R ι M i) f
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Every polynomial is the sum of its weighted homogeneous components.  -/
MvPolynomial.sum_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  (φ : MvPolynomial σ R), ∑ᶠ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) φ = φ
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_eq_zero_iff_notMem_support : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], G.degree v = 0 ↔ v ∉ G.support
-- Init.Data.Nat.Fold
/-- Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f`
is applied to the current value and to the next natural number less than `n`, in increasing order.

Examples:
* `Nat.fold 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))`
* `Nat.fold 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]`
* `Nat.fold 0 (fun i _ xs => xs.push i) #[] = #[]`
 -/
Nat.fold : {α : Type u} → (n : ℕ) → ((i : ℕ) → i < n → α → α) → α → α
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Various statements equivalent to the fact that `f n` grows exponentially slower than `R ^ n`.

* 0: $f n = o(a ^ n)$ for some $-R < a < R$;
* 1: $f n = o(a ^ n)$ for some $0 < a < R$;
* 2: $f n = O(a ^ n)$ for some $-R < a < R$;
* 3: $f n = O(a ^ n)$ for some $0 < a < R$;
* 4: there exist `a < R` and `C` such that one of `C` and `R` is positive and $|f n| ≤ Ca^n$
  for all `n`;
* 5: there exists `0 < a < R` and a positive `C` such that $|f n| ≤ Ca^n$ for all `n`;
* 6: there exists `a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`;
* 7: there exists `0 < a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`.

NB: For backwards compatibility, if you add more items to the list, please append them at the end of
the list.  -/
TFAE_exists_lt_isLittleO_pow : ∀ (f : ℕ → ℝ) (R : ℝ),
  [∃ a ∈ Set.Ioo (-R) R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[Filter.atTop] fun x => a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[Filter.atTop] fun x => a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n].TFAE
-- Init.Data.List.Lemmas
List.ext_getElem_iff : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.uvars : Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.VarSet
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
AlgHom.fieldRange_eq_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] {f : E →ₐ[F] K}, f.fieldRange = ⊤ ↔ Function.Surjective ⇑f
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `... ⊣⊢ₛ ...⌝` syntax from applications of `SPred.entails`.
 -/
Std.Do.SPred.Notation.unexpandBientails : Lean.PrettyPrinter.Unexpander
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_clog_zero_left : ∀ (b n : ℕ), b.ble 1 = true → Nat.clog b n = 0