mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_const_fun : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : OrderBot ι] (ℱ : MeasureTheory.Filtration ι m0)
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : Ω → E},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f μ → MeasureTheory.Martingale (fun x => f) ℱ μ
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientInfToPiQuotient_surj : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R},
  Pairwise (Function.onFun IsCoprime I) → Function.Surjective ⇑(Ideal.quotientInfToPiQuotient I)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.zigzag_isPreconnected : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  (∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂) → CategoryTheory.IsPreconnected J
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hasZeroMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (β : Type w) → CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.GradedObject β C)
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_ofReal_iff : ∀ {p q : ℝ}, 0 ≤ q → (ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
integral of the positive part of `f` and the integral of the negative part of `f`.  -/
MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y))),
  AddMonoid.Coprod.clift f hM₁ hN₁ hM hN = (AddMonoid.coprodCon M N).lift f ⋯
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sep_notMem : ∀ (x y : ZFSet.{u}), ZFSet.sep (fun x => x ∉ y) x = x \ y
-- Batteries.Data.BinomialHeap.Basic
/-- `before` is a difference list which can be appended to a binomial heap
with ranks at least `rank` to produce another well formed heap.  -/
Batteries.BinomialHeap.Imp.FindMin.WF.before : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α}
  (self : Batteries.BinomialHeap.Imp.FindMin.WF le res) {s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.WF le self.rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)
-- Mathlib.Topology.Spectral.ConstructibleTopology
isCompact_sInter_of_subset_constructibleTopologySubbasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [QuasiSeparatedSpace X] {s : Set (Set X)},
  s ⊆ constructibleTopologySubbasis X → s.Finite → IsCompact (⋂₀ s)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpTo_top_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N → (HasFTaylorSeriesUpTo N f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n) f p)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.step_eq : ∀ {β α₁ α₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β} (h : ita.Equiv itb),
  (fun s => Std.Shrink.deflate (Quot.mk (fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) s.inflate)) <$>
      ita.step =
    (fun s => Std.Shrink.deflate (Std.IterM.QuotStep.transportAlongEquiv ⋯ s.inflate)) <$>
      (fun s => Std.Shrink.deflate (Quot.mk (fun s₁ s₂ => (↑s₁).bundledQuotient = (↑s₂).bundledQuotient) s.inflate)) <$>
        itb.step
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- Definition for a primitive additive character on a finite ring `R` into a cyclotomic extension
of a field `R'`. It records which cyclotomic extension it is, the character, and the
fact that the character is primitive.  -/
AddChar.PrimitiveAddChar : (R : Type u) → [CommRing R] → (R' : Type v) → [Field R'] → Type (max u v)
-- Init.System.IO
IO.FS.Mode.readWrite.sizeOf_spec : sizeOf IO.FS.Mode.readWrite = 1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBoth.inj : ∀ {gen gen_1 : Bool},
  Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen = Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen_1 → gen = gen_1
-- Mathlib.Topology.Path
/-- Given a path `γ` and a function `f : I → I` where `f 0 = 0` and `f 1 = 1`, `γ.reparam f` is the
path defined by `γ ∘ f`.
 -/
Path.reparam : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {x y : X} → Path x y → (f : ↑unitInterval → ↑unitInterval) → Continuous f → f 0 = 0 → f 1 = 1 → Path x y
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instSetLike.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  ClosedAddSubgroup.instSetLike G = { coe := fun U => ↑↑U, coe_injective := ⋯ }
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_finsetProd_X_sub_C_eq_card : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {α : Type u_1} (s : Finset α) (f : α → R),
  (∏ a ∈ s, (Polynomial.X - Polynomial.C (f a))).natDegree = s.card
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.smul_centroid_vsub_point_eq_sum_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  (↑n + 1) • (s.centroid -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.Gen.runUntil.decr : Option ℕ → Option ℕ
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.sectionsFunctor_map : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] {F G : CategoryTheory.Functor J (Type w)} (φ : F ⟶ G),
  (CategoryTheory.Functor.sectionsFunctor J).map φ =
    TypeCat.ofHom fun x => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (φ.app j)) (↑x j), ⋯⟩
-- Mathlib.Analysis.Normed.Group.Uniform
abs_dist_sub_le_dist_mul_mul : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E), |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp (t.natTransTriangleLTGEOfLE a b hab) (t.natTransTriangleLTGEOfLE b c hbc) =
    t.natTransTriangleLTGEOfLE a c ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.diagramIsoSpan_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C) (X : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.diagramIsoSpan F).hom.app X = ((fun j => CategoryTheory.eqToIso ⋯) X).hom
-- Mathlib.Algebra.Order.Group.DenselyOrdered
exists_nsmul_lt_of_pos : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : AddCommMonoid M] [ExistsAddOfLE M]
  [IsOrderedCancelAddMonoid M], 0 < x → ∀ (n : ℕ), ∃ y, 0 < y ∧ n • y < x
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.nonneg_pi_iff : ∀ {ι : Type u_1} {R : Type u_2} {Mᵢ : ι → Type u_8} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)]
  [inst_2 : (i : ι) → Module R (Mᵢ i)] {P : Type u_10} [inst_3 : Fintype ι] [inst_4 : AddCommMonoid P]
  [inst_5 : PartialOrder P] [IsOrderedAddMonoid P] [inst_7 : Module R P] {Q : (i : ι) → QuadraticMap R (Mᵢ i) P},
  (∀ (x : (i : ι) → Mᵢ i), 0 ≤ (QuadraticMap.pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (a : MeasureTheory.FiniteMeasure Ω),
  MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom a = ↑a
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
Matrix.isHadamard_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
  (A : Matrix n n R),
  A.IsHadamard ↔
    (∀ (i j : n), A i j ∈ unitary R) ∧
      A * A.conjTranspose = ↑(Fintype.card n) • 1 ∧ A.conjTranspose * A = ↑(Fintype.card n) • 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.instBraidedTransportedFunctorEquivalenceTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [inst_3 : CategoryTheory.BraidedCategory C] →
              (CategoryTheory.Monoidal.equivalenceTransported e).functor.Braided
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.mem_closure_image : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → x ∈ closure s → f x ∈ closure (f '' s)
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C),
  P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
-- Plausible.ArbitraryFueled
/-- A typeclass for *fueled* random generation, i.e. a variant of
the `Arbitrary` typeclass where the fuel for the generator is made explicit.
- This typeclass is equivalent to Rocq QuickChick's `arbitrarySized` typeclass
  (QuickChick uses the `Nat` parameter as both fuel and the generator size,
   here we use it just for fuel, as Plausible's `Gen` type constructor
   already internalizes the size parameter.)  -/
Plausible.ArbitraryFueled : Type → Type
-- Mathlib.Algebra.Divisibility.Units
IsUnit.isRelPrime_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsUnit x → IsRelPrime x y
-- Mathlib.Algebra.Module.Injective
Module.Injective.out : ∀ {R : Type u} {inst : Ring R} {Q : Type v} {inst_1 : AddCommGroup Q} {inst_2 : Module R Q}
  [self : Module.Injective R Q] ⦃X Y : Type v⦄ [inst_3 : AddCommGroup X] [inst_4 : AddCommGroup Y] [inst_5 : Module R X]
  [inst_6 : Module R Y] (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ h, ∀ (x : X), h (f x) = g x
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.instHasDimensionLTTensorObjHAddNat : ∀ {X₁ X₂ : SSet} (d₁ d₂ : ℕ) [X₁.HasDimensionLT d₁] [X₂.HasDimensionLT d₂],
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLT (d₁ + d₂)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.casesOn_of_mul : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive (FreeMonoid.of x * xs)),
  FreeMonoid.casesOn (FreeMonoid.of x * xs) one of_mul = of_mul x xs
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_bot_injective : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : DiscreteTopology X], Function.Injective ⊥.proj
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_smul : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] {R : Type u_14}
  [inst_1 : Zero α] [inst_2 : SMulZeroClass R α] (x : R) (M : (i : o) → Matrix (m' i) (n' i) α),
  Matrix.blockDiagonal' (x • M) = x • Matrix.blockDiagonal' M
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- If the Lebesgue integral of a function is bounded by some constant on all sets with finite
measure and the measure is σ-finite, then the integral over the whole space is bounded by that same
constant.  -/
MeasureTheory.lintegral_le_of_forall_fin_meas_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (C : ENNReal)
  {f : α → ENNReal}, (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C) → ∫⁻ (x : α), f x ∂μ ≤ C
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
lift_trdeg_add_le : ∀ {R : Type u_3} {S : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [Nontrivial R]
  [FaithfulSMul R S] [FaithfulSMul S A],
  Cardinal.lift.{v, u} (Algebra.trdeg R S) + Cardinal.lift.{u, v} (Algebra.trdeg S A) ≤
    Cardinal.lift.{u, v} (Algebra.trdeg R A)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_neg_base_eq_logb : ∀ (b : ℝ), Real.logb (-b) = Real.logb b
-- Mathlib.Tactic.Core
/-- Extract the argument from a `usingArg` syntax as a syntax term  -/
Mathlib.Tactic.getUsingArg : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Syntax
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint8.sizeOf_spec : sizeOf Lean.IR.IRType.uint8 = 1
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Following any unicode character, this indicates that the emoji variant should be displayed  -/
Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.emoji : Char
-- Init.Control.Option
/-- Converts an action that returns an `Option` into one that might fail, with `none` indicating
failure.
 -/
OptionT.mk : {m : Type u → Type v} → {α : Type u} → m (Option α) → OptionT m α
-- Mathlib.CategoryTheory.Iso
/-- The backwards direction of an isomorphism.  -/
CategoryTheory.Iso.inv : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → (Y ⟶ X)
-- Mathlib.Algebra.Order.Archimedean.Hom
/-- There is at most one ordered ring homomorphism from a linear ordered field to an archimedean
linear ordered field.  -/
OrderRingHom.subsingleton : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β] [inst_3 : LinearOrder β]
  [IsStrictOrderedRing β] [Archimedean β], Subsingleton (α →+*o β)
-- Mathlib.Analysis.Normed.Group.Hom
/-- If `φ` satisfies `‖φ‖ ≤ C`, then the same is true for the lifted morphism.  -/
NormedAddGroupHom.Equalizer.norm_lift_le : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V)
  (h : f.comp φ = g.comp φ) (C : ℝ), ‖φ‖ ≤ C → ‖NormedAddGroupHom.Equalizer.lift φ h‖ ≤ C
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.eqToHom_comp_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {j j' : J} (hj : j = j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.colimit.ι F j) =
    CategoryTheory.Limits.colimit.ι F j'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_empty : ∀ {α : Type u_2} [inst : Mul α] {s : Set α}, s * ∅ = ∅
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] (i j k : ι),
  P.pairingIn S j ((P.reflectionPerm i) k) = P.pairingIn S ((P.reflectionPerm i) j) k
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.IsStableUnderBaseChange.localizationPreserves : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.IsStableUnderBaseChange P → RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keysArray_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.keysArray =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keysArray.attach).unattach
-- Mathlib.Analysis.Calculus.Monotone
/-- If `(f y - f x) / (y - x)` converges to a limit as `y` tends to `x`, then the same goes if
`y` is shifted a little bit, i.e., `f (y + (y-x)^2) - f x) / (y - x)` converges to the same limit.
This lemma contains a slightly more general version of this statement (where one considers
convergence along some subfilter, typically `𝓝[<] x` or `𝓝[>] x`) tailored to the application
to almost everywhere differentiability of monotone functions.  -/
tendsto_apply_add_mul_sq_div_sub : ∀ {f : ℝ → ℝ} {x a c d : ℝ} {l : Filter ℝ},
  l ≤ nhdsWithin x {x}ᶜ →
    Filter.Tendsto (fun y => (f y - d) / (y - x)) l (nhds a) →
      Filter.Tendsto (fun y => y + c * (y - x) ^ 2) l l →
        Filter.Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (nhds a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  Q 2 ≠ 0 →
    P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W'.negY Q * P 2 ^ 3 → W'.dblZ P = 0
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_ι_app : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α) (x : J),
  (CategoryTheory.Limits.CompleteLattice.colimitCocone F).cocone.ι.app x = CategoryTheory.homOfLE ⋯
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that the tree set is not empty, retrieves the smallest element.
 -/
Std.ExtTreeSet.min : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → t ≠ ∅ → α
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_spec : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α),
  ∃ t ⊆ s, t.card = addRothNumber s ∧ ThreeAPFree ↑t
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The center of a non-unital algebra is commutative and associative  -/
NonUnitalSubalgebra.center.instNonUnitalCommSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] → NonUnitalCommSemiring ↥(NonUnitalSubalgebra.center R A)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLtSpan : {x y : Std.Time.Nanosecond.Span} → Decidable (x < y)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opNNNorm_le_of_lipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  {f : E →SL[σ₁₂] F} {K : NNReal}, LipschitzWith K ⇑f → ‖f‖₊ ≤ K
-- Mathlib.Probability.Moments.SubGaussian
/-- **Alias** of `ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF`.

---

**Azuma-Hoeffding inequality** for sub-Gaussian random variables.  -/
ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ}
  {cY : ℕ → NNReal} {ℱ : MeasureTheory.Filtration ℕ mΩ} [inst_1 : MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.StronglyAdapted ℱ Y →
    ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) μ →
      ∀ (n : ℕ),
        (∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
          ∀ {ε : ℝ},
            0 ≤ ε →
              μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, cY i)))
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restrOpen_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s), (e.restrOpen s hs).toPartialEquiv = e.restr s
-- Init.Prelude
/-- Throw an error with the given message,
using the `ref` for the location information.
 -/
Lean.Macro.throwError : {α : Type} → String → Lean.MacroM α
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for the `positivity` tactic: `Int.cast` is positive (resp. non-negative)
if its input is.  -/
Mathlib.Meta.Positivity.evalIntCast : Mathlib.Meta.Positivity.PositivityExt
-- Lean.Parser.Do
Lean.Parser.Term.termReturn.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Defs
String.instInhabitedPos : {s : String} → Inhabited s.Pos
-- Batteries.Data.List.Lemmas
List.swap_eq_of_ge_right : ∀ {α : Type u_1} {j i : ℕ} {xs : List α}, xs.length ≤ j → xs.swap i j = xs
-- Lean.CoreM
/-- Restore backtrackable parts of the state.  -/
Lean.Core.SavedState.restore : Lean.Core.SavedState → Lean.CoreM Unit
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) (y : N) (x : R)
  (mem : x ∈ Module.Baer.ExtensionOfMaxAdjoin.ideal i f y),
  (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) x = (Module.Baer.ExtensionOfMaxAdjoin.idealTo i f y) ⟨x, mem⟩
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.toIsNormalEpiCategory : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C],
  CategoryTheory.IsNormalEpiCategory C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDeriv_odd_sin : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Real.sin = (-1) ^ n * Real.cos
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}