mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- **Alias** of `AddSubmonoid.nsmulSaturated_iff_nsmul`. -/
AddSubgroup.saturated_iff_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {H : AddSubmonoid G},
  H.NSMulSaturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
-- Mathlib.Order.IsNormal
Order.IsNormal.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LinearOrder α] [WellFoundedLT α] [inst_2 : SuccOrder α]
  [inst_3 : LinearOrder β] [inst_4 : OrderBot α] {g : α → β},
  Order.IsNormal f → Order.IsNormal g → (f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (Order.succ a) = g (Order.succ a))
-- Mathlib.Order.SupClosed
infClosure_supClosure : ∀ {α : Type u_3} [inst : DistribLattice α] (s : Set α), infClosure (supClosure s) = latticeClosure s
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the largest element in the tree that is `≤ x`.

```
findLe 2 {1, 2, 4} = some 2
findLe 3 {1, 2, 4} = some 2
findLe 0 {1, 2, 4} = none
```  -/
Ordnode.findLe : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option α
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.forget_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.CommRingObjCat C),
  (CategoryTheory.CommRingObjCat.forget C).obj R = R.X
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.instCommSemiring : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → CommSemiring (SymmetricAlgebra R M)
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.structuralArg : Lean.Elab.TerminationMeasure → Lean.MetaM ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Preorder.measurable_restrictLe : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (a : α) → MeasurableSpace (X a)] (a : α),
  Measurable (Preorder.restrictLe a)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} → {S : C} → J.ZeroHypercover S → CategoryTheory.PreZeroHypercover S
-- Mathlib.CategoryTheory.Grothendieck
/-- The fiber inclusion `ι F c` composed with `map α` is isomorphic to `α.app c ⋙ ι F' c`.  -/
CategoryTheory.Grothendieck.ιCompMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F' : CategoryTheory.Functor C CategoryTheory.Cat} →
      (α : F ⟶ F') →
        (c : C) →
          (CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.map α) ≅
            (α.app c).toFunctor.comp (CategoryTheory.Grothendieck.ι F' c)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.sum_mem : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {t : Finset ι} {f : ι → M}, (∀ c ∈ t, f c ∈ p) → ∑ i ∈ t, f i ∈ p
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The kernel of `f` is always a smaller subobject than the kernel of `f ≫ h`.  -/
CategoryTheory.Limits.kernelSubobject_comp_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z)
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f h)],
  CategoryTheory.Limits.kernelSubobject f ≤
    CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.lt_zero_iff : ∀ {n : WithBot ℕ}, n < 0 ↔ n = ⊥
-- Std.Data.Iterators.Combinators.Monadic.Drop
Std.Iterators.Types.Drop.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {remaining : ℕ} {inner : Std.IterM m β} {remaining_1 : ℕ}
  {inner_1 : Std.IterM m β},
  { remaining := remaining, inner := inner } = { remaining := remaining_1, inner := inner_1 } →
    remaining = remaining_1 ∧ inner = inner_1
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_eq_zero_iff : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : ↥(MeasureTheory.Lp E p μ)}, 0 < p → (‖f‖ = 0 ↔ f = 0)
-- Mathlib.Analysis.MellinTransform
/-- If `f` is `O(x ^ (-a))` as `x → 0`, then `log • f` is `O(x ^ (-b))` for every `a < b`.  -/
isBigO_rpow_zero_log_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E},
  a < b →
    (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-a)) →
      (fun t => Real.log t • f t) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instLawfulFunctor : ∀ (p : ℕ), LawfulFunctor (WittVector p)
-- Mathlib.Logic.Denumerable
Nat.Subtype.exists_succ : ∀ {s : Set ℕ} [Infinite ↑s] (x : ↑s), ∃ n, ↑x + n + 1 ∈ s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.Parallel.refl : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P), s.Parallel s
-- Mathlib.Data.Set.Card
Set.Nat.encard_range : ∀ (k : ℕ), {i | i < k}.encard = ↑k
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The inverse functor establishing the equivalence `StructuredArrow.preEquivalence`.  -/
CategoryTheory.StructuredArrow.preEquivalenceInverse : {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] →
            (F : CategoryTheory.Functor C D) →
              {G : CategoryTheory.Functor D E} →
                {e : E} →
                  (f : CategoryTheory.StructuredArrow e G) →
                    CategoryTheory.Functor (CategoryTheory.StructuredArrow f.right F)
                      (CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G))
-- Lean.Meta.Closure
/-- Remark: This method does not guarantee unique user names.
The correctness of the procedure does not rely on unique user names.
Recall that the pretty printer takes care of unintended collisions.  -/
Lean.Meta.Closure.mkNextUserName : Lean.Meta.Closure.ClosureM Lean.Name
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (inner : Std.Bounded✝ α), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.isωSup_iff_isLUB : ∀ {α : Type u} [inst : Preorder α] {c : OmegaCompletePartialOrder.Chain α} {x : α},
  Scott.IsωSup c x ↔ IsLUB (Set.range ⇑c) x
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- **Alias** of `KaehlerDifferential.tensorKaehlerEquivBase_tmul`. -/
KaehlerDifferential.tensorKaehlerEquiv_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (a : S) (b : Ω[A⁄R]),
  (KaehlerDifferential.tensorKaehlerEquivBase R S A B) (a ⊗ₜ[R] b) = a • (KaehlerDifferential.map R S A B) b
-- Mathlib.Order.Max
IsTop.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.2
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.repr_apply_apply : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι), ↑(b.repr v) i = inner 𝕜 (b i) v
-- Init.Data.List.Basic
List.modifyHead.eq_1 : ∀ {α : Type u} (f : α → α), List.modifyHead f [] = []
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.bind_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X)
  (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y),
  (CategoryTheory.Sieve.bind S R).arrows = S.bind fun x x_1 h => (R h).arrows
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.ne_cast_int : ∀ {p x : ℝ}, LiouvilleWith p x → 1 < p → ∀ (m : ℤ), x ≠ ↑m
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.to_mul_symm_eq : ∀ {G : Type u_3} [inst : DivInvMonoid G], ConjAct.toConjAct.symm = ConjAct.ofConjAct
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.lt : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.SplitInfo → Bool
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.exists_coeff_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R}, p ≠ 0 → ∃ d, MvPolynomial.coeff d p ≠ 0
-- Batteries.Data.Array.Scan
Array.back?_scanr : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α}, (Array.scanr f init as).back? = some init
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.mk' : {α : Type v} → [small : Std.Internal.Small α] → Std.Internal.ComputableSmall.Target α → Std.Internal.USquash α
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.discard_eq_const : ∀ {α : Type u_1} {mα : MeasurableSpace α},
  ProbabilityTheory.Kernel.discard α = ProbabilityTheory.Kernel.const α (MeasureTheory.Measure.dirac PUnit.unit)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Pullback a monoid object along a fully faithful oplax monoidal functor.  -/
CategoryTheory.Functor.FullyFaithful.monObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.OplaxMonoidal] →
                F.FullyFaithful → (X : C) → [CategoryTheory.MonObj (F.obj X)] → CategoryTheory.MonObj X
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.mk_toOrderHom_apply : ∀ {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) (i : Fin (a.len + 1)),
  (SimplexCategory.Hom.mk f).toOrderHom i = f i
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
notMem_nonZeroDivisors_iff_left : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {r : M₀}, r ∉ nonZeroDivisors M₀ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.npow : {α : Type u} → [inst : Lean.Grind.Semiring α] → Lean.Grind.Ring.OfSemiring.Q α → ℕ → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.Order.Cover
Set.Ioc_eq_singleton_right_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ioc b a = {a} ↔ b ⋖ a
-- Mathlib.Topology.Constructible
Topology.isConstructible_compl : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Topology.IsConstructible sᶜ ↔ Topology.IsConstructible s
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_right_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
-- Init.Data.SInt.Lemmas
instLawfulOrderLTInt32 : Std.LawfulOrderLT Int32
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_symm_eq_symm_trans_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').symm = e'.symm.trans e.symm
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Init.Data.Int.Order
Int.natAbs_add_le : ∀ (a b : ℤ), (a + b).natAbs ≤ a.natAbs + b.natAbs
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_union : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {s t : Set E},
  B.polar (s ∪ t) = B.polar s ∩ B.polar t
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.elabWhere.describeOptions : Lean.Options → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_ushiftRight : ∀ {w : ℕ} {x : BitVec w} {i n : ℕ}, (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n)))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_snd : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x y : X} (f : x ⟶ y),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).map f).snd =
    S.snd.map f
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.ofLeftInverse_symm_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {g : S → R} {f : R →+* S}
  (h : Function.LeftInverse g ⇑f) (x : ↥f.range), (RingEquiv.ofLeftInverse h).symm x = g ↑x
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.transitive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (self : CategoryTheory.Pretopology C) ⦃X : C⦄ (S : CategoryTheory.Presieve X)
  (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
  S ∈ self.coverings X → (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ self.coverings Y) → S.bind Ti ∈ self.coverings X
-- Init.SimpLemmas
have_congr' : ∀ {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β}, a = a' → (∀ (x : α), f x = f' x) → f a = f' a'
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.costructuredArrowRightwards_map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (X₃ : C₃)
  {X Y : CategoryTheory.CostructuredArrow L X₃} (f : X ⟶ Y),
  (w.costructuredArrowRightwards X₃).map f =
    (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).map
      ((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).map
        (CategoryTheory.CostructuredArrow.homMk f.left ⋯))
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.instInhabitedTriangleMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (T : CategoryTheory.Pretriangulated.Triangle C) → Inhabited (CategoryTheory.Pretriangulated.TriangleMorphism T T)
-- Init.Core
/-- The term `opaqueId x` will not be reduced by the kernel.
 -/
Lean.opaqueId : {α : Sort u} → α → α
-- Mathlib.Data.Finset.Card
Multiset.dedup_card_eq_card_iff_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α}, m.dedup.card = m.card ↔ m.Nodup
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray.congr_simp : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Rco α),
  r = r_1 → r.toArray = r_1.toArray
-- Mathlib.Order.Filter.Pointwise
Filter.mem_mul : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α} {s : Set α}, s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyReal K] (F : Subfield K) [Algebra.IsAlgebraic (↥F) K],
  NumberField.IsTotallyReal ↥F
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_add : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    (∀ (n : ℕ), MeasureTheory.Integrable (g n) μ) →
      ∀ (n : ℕ),
        MeasureTheory.martingalePart (f + g) ℱ μ n =ᵐ[μ]
          MeasureTheory.martingalePart f ℱ μ n + MeasureTheory.martingalePart g ℱ μ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
`2 * cosh θ` to the value `2 * cosh (n * θ)`.  -/
Polynomial.Chebyshev.C_two_mul_real_cosh : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (2 * Real.cosh θ) (Polynomial.Chebyshev.C ℝ n) = 2 * Real.cosh (↑n * θ)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- Let `S` be a closed subalgebra of a Banach algebra `A`. If for `x : S` the complement of the
spectrum of `↑x : A` is connected, then `spectrum 𝕜 x = spectrum 𝕜 (x : A)`.  -/
Subalgebra.spectrum_eq_of_isPreconnected_compl : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A]
  [inst_6 : SMulMemClass SA 𝕜 A] (S : SA) [hS : IsClosed ↑S] (x : ↥S),
  IsPreconnected (spectrum 𝕜 ↑x)ᶜ → spectrum 𝕜 x = spectrum 𝕜 ↑x
-- Mathlib.Computability.Partrec
Computable.encode : ∀ {α : Type u_1} [inst : Primcodable α], Computable Encodable.encode
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)),
  List.findSomeM? f [] = pure none
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulLeft₀_symm : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : PosMulReflectLT G₀] (a : G₀)
  (ha : 0 < a), (OrderIso.mulLeft₀ a ha).symm = OrderIso.mulLeft₀ a⁻¹ ⋯
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- The function `seminormFromConst' c f` is bounded above by `f`.  -/
seminormFromConst_le_seminorm : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → ∀ (x : R), seminormFromConst' c f x ≤ f x
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.unfold : Lean.Meta.Grind.AttrKind
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instModule : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : ContinuousAdd β] →
            {R : Type u_2} →
              [inst_4 : Semiring R] →
                [inst_5 : Module R β] → [ContinuousConstSMul R β] → Module R (ZeroAtInftyContinuousMap α β)
-- Mathlib.Geometry.Manifold.Bordism
/-- The disjoint union of two singular `I`-manifolds on `X` is a singular `I`-manifold on `X`.  -/
SingularManifold.sum : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} →
                    SingularManifold X k I → SingularManifold X k I → SingularManifold X k I
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_C_mul : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R),
  MvPolynomial.C a • D f = a • D f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → ∀ {t : Set M}, s ∈ nhdsWithin x t → MDiffAt[t] f x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.filterMap f t)[k]! = (t[k]?.bind fun x => f k' x).get!
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_inter_eq_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_one_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] {x : M} {n : ℕ}, n ≠ 0 → (x ^ n ≤ 1 ↔ x ≤ 1)
-- Mathlib.Topology.UniformSpace.Defs
nhds_eq_uniformity' : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = (uniformity α).lift' fun s => {y | (y, x) ∈ s}
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.aux₁ : ∀ {α β : Type w} {m : Type w → Type w'} {it : Std.IterM m β} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Std.Iterator α m β] [Std.Iterators.Finite α m] {b : β} {bs : Array β},
  Std.IterM.toArray.go it (#[b] ++ bs) = (fun x => #[b] ++ x) <$> Std.IterM.toArray.go it bs
-- Lean.Data.Trie
Lean.Data.Trie.node1 : {α : Type} → Option α → UInt8 → Lean.Data.Trie α → Lean.Data.Trie α
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.instCoeOutRingEquiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → CoeOut (A ≃⋆+* B) (A ≃+* B)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.Context.pos : Lean.Server.Completion.Context✝ → Lean.Lsp.Position
-- Mathlib.CategoryTheory.Comma.Arrow
/-- `homMk'''` is the dual of `homMk'`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Arrow.homMk''' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {X Y : T} →
      {f : Y ⟶ X} →
        {P Q : T} →
          {g : Q ⟶ P} →
            (u : P ⟶ X) →
              (v : Q ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp g u = CategoryTheory.CategoryStruct.comp v f)
                    CategoryTheory.Arrow.homMk'''._auto_1 →
                  (CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk f)
-- Mathlib.Logic.Function.Basic
Function.RightInverse.comp_eq_id : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.RightInverse f g → g ∘ f = id
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.star_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {X_1 Y : C} (f : X_1 ⟶ Y),
  ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
-- Lean.Level
Lean.Level.instHashable : Hashable Lean.Level
-- Mathlib.Control.Monad.Writer
WriterT.adapt : {M : Type u → Type v} → {ω : Type u} → [Monad M] → {ω' α : Type u} → (ω → ω') → WriterT ω M α → WriterT ω' M α