mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.operating.injEq : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (currPos_1 : s.Pos)
  (searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  (String.Slice.RevSplitIterator.operating currPos searcher =
      String.Slice.RevSplitIterator.operating currPos_1 searcher_1) =
    (currPos = currPos_1 ∧ searcher = searcher_1)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- A commutative comonoid object is a comonoid object.  -/
CategoryTheory.CommComon.toComon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommComon C → CategoryTheory.Comon C
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- A Type synonym for `A ⊗[R] B`, but with multiplication as `TensorProduct.gradedMul`.

This has notation `𝒜 ᵍ⊗[R] ℬ`.  -/
GradedTensorProduct : (R : Type u_1) →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) → [GradedAlgebra 𝒜] → [GradedAlgebra ℬ] → Type (max u_4 u_3)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R) (u v : R),
  W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- A subcomplex is again a CW complex.  -/
Topology.RelCWComplex.Subcomplex.instRelCWComplex : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [T2Space X] →
        [inst : Topology.RelCWComplex C D] → (E : Topology.RelCWComplex.Subcomplex C) → Topology.RelCWComplex (↑E) D
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_subtypePerm_of_not_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {g : Equiv.Perm α} (hg : ∀ (x : α), p (g x) ↔ p x) {a : α},
  ¬p a → (Equiv.Perm.ofSubtype (g.subtypePerm hg)) a = a
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.le_norm_iff : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} {x : M ⧸ S} {r : ℝ},
  r ≤ ‖x‖ ↔ ∀ (m : M), ↑m = x → r ≤ ‖m‖
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.invMulSubgroup_eq_inv_mul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card),
  ↑(A.invMulSubgroup h) = ↑A⁻¹ * ↑A
-- Mathlib.Order.Types.Defs
OrderType.instZero : Zero OrderType.{u_1}
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindIso_inv_hom_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S),
  (Rep.Hom.hom A.indCoindIso.inv).toLinearMap =
    { toFun := (Representation.Equiv.mk (LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ⋯).invFun,
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Data.Nat.Nth
Nat.isLeast_nth : ∀ {p : ℕ → Prop} {n : ℕ},
  (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
-- Init.Grind.AC
Lean.Grind.AC.eq_norm_ac_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.AC.Expr) (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ac_cert lhs rhs lhs' rhs' = (lhs.toSeq.sort.beq' lhs').and' (rhs.toSeq.sort.beq' rhs')
-- Mathlib.Data.Sym.Sym2
Sym2.other_eq_other' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z), Sym2.Mem.other h = Sym2.Mem.other' h
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_aleph0_eq : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a * Cardinal.aleph0 = a
-- Aesop.Search.Expansion
Aesop.RuleResult.proved.injEq : ∀ (newRapps newRapps_1 : Array Aesop.RappRef),
  (Aesop.RuleResult.proved newRapps = Aesop.RuleResult.proved newRapps_1) = (newRapps = newRapps_1)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y}
  (base_open : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  (∀ (U : TopologicalSpace.Opens ↑↑X), CategoryTheory.IsIso (f.c.app (Opposite.op (base_open.functor.obj U)))) →
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f
-- Mathlib.FieldTheory.Separable
Polynomial.separable_prod : ∀ {R : Type u} [inst : CommRing R] {ι : Type u_1} [inst_1 : Fintype ι] {f : ι → Polynomial R},
  Pairwise (Function.onFun IsCoprime f) → (∀ (x : ι), (f x).Separable) → (∏ x, f x).Separable
-- Mathlib.Topology.Hom.ContinuousEval
Continuous.eval : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] [inst_5 : TopologicalSpace Z]
  {f : Z → F} {g : Z → X}, Continuous f → Continuous g → Continuous fun z => (f z) (g z)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
FiberwiseLinear.openPartialHomeomorph.congr_simp : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {U U_1 : Set B} (e_U : U = U_1) (φ φ_1 : B → F ≃L[𝕜] F)
  (e_φ : φ = φ_1) (hU : IsOpen U) (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U),
  FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ = FiberwiseLinear.openPartialHomeomorph φ_1 ⋯ ⋯ ⋯
-- Lean.MetavarContext
Lean.MetavarContext.mkLambda : Array Lean.Expr →
  Lean.Expr →
    optParam Bool false →
      optParam Bool true →
        optParam Bool false →
          optParam Bool true →
            optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetavarContext.MkBindingM Lean.Expr
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.contains_iff_findEntry? : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBMap α β cmp},
  t.contains x = true ↔ ∃ v, t.findEntry? x = some v
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_le : ∀ {α β : Type u} {f : α → β} {s : Set α}, Cardinal.mk ↑(f '' s) ≤ Cardinal.mk ↑s
-- Mathlib.Data.Finset.Interval
/-- Cardinality of an `Ioo` of finsets.  -/
Finset.card_Ioo_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → (Finset.Ioo s t).card = 2 ^ (t.card - s.card) - 2
-- Lean.DocString.Types
Lean.Doc.instOrdBlock : {i : Type u_1} → {b : Type u_2} → [Ord i] → [Ord b] → Ord (Lean.Doc.Block i b)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.eqOn_adjoin : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  {D1 D2 : Derivation R A M} {s : Set A}, Set.EqOn (⇑D1) (⇑D2) s → Set.EqOn ⇑D1 ⇑D2 ↑(Algebra.adjoin R s)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullback_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y S : C} (f : X ⟶ S)
  (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g] [P.IsStableUnderBaseChangeAlong f],
  P g → P (CategoryTheory.Limits.pullback.fst f g)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.unitOfList l cmp) k = ()
-- Lean.Declaration
Lean.instInhabitedQuotKind.default : Lean.QuotKind
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.skipWhile.induct_unfolding : ∀ {ρ : Type} {s : String.Slice} (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat]
  (motive : s.Pos → s.Pos → Prop),
  (∀ (x nextCurr : s.Pos),
      x.skip? pat = some nextCurr →
        x < nextCurr → motive nextCurr (nextCurr.skipWhile pat) → motive x (nextCurr.skipWhile pat)) →
    (∀ (x nextCurr : s.Pos), x.skip? pat = some nextCurr → ¬x < nextCurr → motive x x) →
      (∀ (x : s.Pos), x.skip? pat = none → motive x x) → ∀ (pos : s.Pos), motive pos (pos.skipWhile pat)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Additive.isIsIsometricVAdd : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X],
  IsIsometricVAdd (Additive M) X
-- Mathlib.Data.Multiset.UnionInter
Multiset.add_inter_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Multiset α), s + t ∩ u = (s + t) ∩ (s + u)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_nest : ∀ {p : DyckWord}, p.nest.semilength = p.semilength + 1
-- Mathlib.Data.Int.ModEq
Int.ModEq.eq_1 : ∀ (n a b : ℤ), (a ≡ b [ZMOD n]) = (a % n = b % n)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitIsoLimitCurryCompLim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)],
  CategoryTheory.Limits.limitIsoLimitCurryCompLim G =
    Trans.simple (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.Functor.currying.symm.unitIso.app G))
      (CategoryTheory.Limits.limitUncurryIsoLimitCompLim (CategoryTheory.Functor.curry.obj G))
-- Mathlib.Analysis.Calculus.Deriv.Inv
fderivWithin_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ≠ 0 →
    UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => x⁻¹) s x = ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoal.mk.sizeOf_spec : ∀ (rendered : String) (goals : Array String),
  sizeOf { rendered := rendered, goals := goals } = 1 + sizeOf rendered + sizeOf goals
-- Mathlib.Data.Set.Function
Set.eqOn_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_7} {f : ι → α} {g₁ g₂ : α → β},
  Set.EqOn g₁ g₂ (Set.range f) ↔ g₁ ∘ f = g₂ ∘ f
-- Init.Data.Array.Lemmas
Array.toArray_append : ∀ {α : Type u_1} {xs : List α} {ys : Array α}, xs.toArray ++ ys = (xs ++ ys.toList).toArray
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_head_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.min he = t.toList.head ⋯
-- Mathlib.RingTheory.Valuation.Basic
/-- The support of a valuation is a prime ideal.  -/
Valuation.instIsPrimeSuppOfNontrivialOfNoZeroDivisors : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  [Nontrivial Γ₀] [NoZeroDivisors Γ₀], v.supp.IsPrime
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_functor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  (CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).functor =
    CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.smul_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) (v : V₁), (r • f) v = r • f v
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_iso_inv : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).iso.inv =
    CategoryTheory.CategoryStruct.id
      (X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Topology.Category.Sequential
Sequential.mk.sizeOf_spec : ∀ (toTop : TopCat) [is_sequential : SequentialSpace ↑toTop],
  sizeOf { toTop := toTop, is_sequential := is_sequential } = 1 + sizeOf toTop + sizeOf is_sequential
-- Mathlib.Algebra.Polynomial.Identities
_private.Mathlib.Algebra.Polynomial.Identities.0.Polynomial.poly_binom_aux2 : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R) (x y : R),
  Polynomial.eval (x + y) f =
    f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1✝ x y e a) * y ^ 2)
-- Mathlib.Data.List.Chain
WellFounded.listPairwise_reverse_compl : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α}, WellFounded r → List.IsChain r l → List.Pairwise rᶜ l.reverse
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.mem_Gamma_one : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), γ ∈ CongruenceSubgroup.Gamma 1
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimitsOfShape.of_essentiallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.EssentiallySmall.{u₁, v₂, u₂} J]
  [CategoryTheory.LocallySmall.{v₁, v₂, u₂} J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The sum over a set of an elements in distinct classes is in the lowest class.  -/
ArchimedeanClass.mk_sum : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {ι : Type u_2}
  [inst_3 : LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M},
  StrictMonoOn (ArchimedeanClass.mk ∘ a) ↑s →
    ArchimedeanClass.mk (∑ i ∈ s, a i) = ArchimedeanClass.mk (a (s.min' hnonempty))
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Oriented vector angle version of "angles in same segment are equal" and "opposite angles of
a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same
result), represented here as equality of twice the angles.  -/
Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x₁ x₂ y z : V},
  x₁ ≠ y →
    x₁ ≠ z →
      x₂ ≠ y →
        x₂ ≠ z →
          ∀ {r : ℝ},
            ‖x₁‖ = r → ‖x₂‖ = r → ‖y‖ = r → ‖z‖ = r → 2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)
-- Mathlib.GroupTheory.MonoidLocalization.Away
Localization.Away.invSelf.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M), Localization.Away.invSelf x = Localization.mk 1 ⟨x, ⋯⟩
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.down : Lean.Meta.Grind.BuiltinPropagators → Lean.Meta.Grind.PropagatorMap
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrableOn_rpow_mul_exp_neg_mul_rpow : ∀ {p s b : ℝ},
  -1 < s →
    0 < p → 0 < b → MeasureTheory.IntegrableOn (fun x => x ^ s * Real.exp (-b * x ^ p)) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Analysis.Complex.Basic
Complex.isOpen_slitPlane : IsOpen Complex.slitPlane
-- Mathlib.Probability.Process.Filtration
/-- Given a filtration `𝓕`, its **right continuation** is the filtration `𝓕₊` defined as follows:
- If `i` is isolated on the right, then `𝓕₊ i := 𝓕 i`;
- Otherwise, `𝓕₊ i := ⨅ j > i, 𝓕 j`.

It is sometimes simply defined as `𝓕₊ i := ⨅ j > i, 𝓕 j` when the index type is `ℝ`. In the
general case this is not ideal however. If `i` is maximal for instance, then `𝓕₊ i = ⊤`, which
is inconvenient because `𝓕₊` is not a `Filtration ι m` anymore. If the index type
is discrete (such as `ℕ`), then we would have `𝓕 = 𝓕₊` (i.e. `𝓕` is right-continuous) only if
`𝓕` is constant.

To avoid requiring a `TopologicalSpace` instance on `ι` in the definition, we endow `ι` with
the order topology `Preorder.topology` inside the definition. Say you write a statement about
`𝓕₊` which does not require a `TopologicalSpace` structure on `ι`,
but you wish to use a statement which requires a topology (such as `rightCont_apply`).
Then you can endow `ι` with the order topology by writing
```lean
  letI := Preorder.topology ι
  haveI : OrderTopology ι := ⟨rfl⟩
```  -/
MeasureTheory.Filtration.rightCont : {Ω : Type u_3} →
  {ι : Type u_4} →
    {m : MeasurableSpace Ω} → [inst : PartialOrder ι] → MeasureTheory.Filtration ι m → MeasureTheory.Filtration ι m
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_comp_succAbove : ∀ {n : ℕ} {β : Sort u_2} (i : Fin (n + 1)) (x : β) (p : Fin n → β), i.insertNth x p ∘ i.succAbove = p
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- The absolute value satisfies the triangle inequality  -/
AbsoluteValue.add_le' : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (self : AbsoluteValue R S) (x y : R), self.toFun (x + y) ≤ self.toFun x + self.toFun y
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_add_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f g : X → Y},
  eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Mathlib.Topology.Category.LightProfinite.Limits
LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology : CompHausLike.HasExplicitPullbacks fun Y => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_apply : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f) {x : X}, ↑(e.lift_openEmbedding hf) (f x) = ↑e x
-- Mathlib.RingTheory.PicardGroup
Module.Flat.submoduleAlgebraEquiv.congr_simp : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [inst_5 : Module.Flat R M]
  [inst_6 : FaithfulSMul R A], Module.Flat.submoduleAlgebraEquiv e = Module.Flat.submoduleAlgebraEquiv e
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase0.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.DiseqCnstr), sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 c) = 1 + sizeOf c
-- Lean.Meta.Sym.Util
_private.Lean.Meta.Sym.Util.0.Lean.Expr.checkMaxShared.throwNotMaxShared : String → Lean.Expr → Lean.Meta.Sym.SymM Unit
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right : ∀ {R : Type u} [inst : CommRing R] {M N P : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] [inst_7 : Coalgebra R M]
  [inst_8 : Coalgebra R N] [inst_9 : Coalgebra R P], CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.free_iff_isTorsionFree : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M], Module.Free R M ↔ Module.IsTorsionFree R M
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_one_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (x : R), (iterateFrobenius R p 1) x = x ^ p
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- In a separable normed space, there exists a sequence of continuous functions that
separates points of the weak dual.  -/
WeakDual.exists_countable_separating : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E],
  ∃ gs, (∀ (n : ℕ), Continuous (gs n)) ∧ ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ n, gs n x ≠ gs n y
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] [inst_1 : SizeOf R] (toTopologicalSpace : TopologicalSpace R)
  (toIsTopologicalRing : IsTopologicalRing R),
  sizeOf { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing } =
    1 + sizeOf toTopologicalSpace + sizeOf toIsTopologicalRing
-- Mathlib.Computability.NFA
NFA.reverse.eq_1 : ∀ {α : Type u} {σ : Type v} (M : NFA α σ),
  M.reverse = { step := fun s a => {s' | s ∈ M.step s' a}, start := M.accept, accept := M.start }
-- Lean.ScopedEnvExtension
Lean.scopedEnvExtensionsRef : IO.Ref (Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))
-- Mathlib.Topology.Algebra.MulAction
instContinuousSMulULift : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X], ContinuousSMul (ULift.{u_5, u_1} M) X
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.toLinearMap_map : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D),
  (Algebra.TensorProduct.map f g).toLinearMap = TensorProduct.AlgebraTensorModule.map f.toLinearMap g.toLinearMap
-- Init.Data.Vector.Basic
/-- The last element of a vector. Panics if the vector is empty.  -/
Vector.back! : {α : Type u_1} → {n : ℕ} → [Inhabited α] → Vector α n → α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.op_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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L), (φ.map L hL).op = φ.op.map L.op ⋯
-- Mathlib.Analysis.Calculus.TangentCone.Defs
tangentConeAt_def : ∀ (R : Type u_1) {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] (s : Set E)
  (x : E), tangentConeAt R s x = {y | ClusterPt y (⊤ • nhdsWithin 0 ((fun x_1 => x + x_1) ⁻¹' s))}