mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.mk.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (hom hom_1 : A.pt ⟶ B.pt) (e_hom : hom = hom_1)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j),
  { hom := hom, w := w } = { hom := hom_1, w := ⋯ }
-- Mathlib.Data.Matrix.Mul
/-- A semiring is stably finite if every matrix ring over it is Dedekind-finite.  -/
IsStablyFiniteRing : (R : Type u_10) → [MulOne R] → [AddCommMonoid R] → Prop
-- Mathlib.Algebra.Category.Ring.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
 -/
CommSemiRingCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommSemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] →
        CategoryTheory.Limits.IsLimit (CommSemiRingCat.limitCone F)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Expr),
  a = x →
    (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
      (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) →
        (match a with
          | Lean.Grind.CommRing.Expr.num n => h_1 n
          | Lean.Grind.CommRing.Expr.var x => h_2 x
          | x => h_3 x) ≍
          h_3 x
-- Mathlib.Order.Disjoint
IsComplemented.inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : α},
  IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b)
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_add_eq : ∀ {a : ℕ} (n : ℕ), a ≤ n + n → (n * n + a).sqrt = n
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional`. -/
Topology.CWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteDimensional C] (E : Topology.RelCWComplex.Subcomplex C),
  Topology.RelCWComplex.FiniteDimensional ↑E
-- Mathlib.Util.AtomM
/-- The mutable state of the `AtomM` monad.  -/
Mathlib.Tactic.AtomM.State : Type
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instInhabited.eq_1 : Semigrp.instInhabited = { default := Semigrp.of PEmpty.{u_1 + 1} }
-- Mathlib.Topology.MetricSpace.Perfect
/-- Any nonempty perfect set in a complete metric space admits a continuous injection
from the Cantor space, `ℕ → Bool`.  -/
Perfect.exists_nat_bool_injection : ∀ {α : Type u_1} [inst : MetricSpace α] {C : Set α},
  Perfect C → C.Nonempty → ∀ [CompleteSpace α], ∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
-- Mathlib.GroupTheory.Congruence.Hom
Con.kerLift.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P),
  Con.kerLift f = (Con.ker f).lift f ⋯
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Auxiliary definition for `presheafHom`.  -/
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.coconeApp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G :
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
                (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))} →
            (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶
                CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G) →
              {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} →
                (x : P.Elements) →
                  CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj (Opposite.unop x.fst) ⟶ F.op.comp (G.obj P)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Give a vertex as an element of the subgraph's vertex type.  -/
SimpleGraph.Subgraph.vert : {V : Type u} → {G : SimpleGraph V} → (G' : G.Subgraph) → (v : V) → v ∈ G'.verts → ↑G'.verts
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_eq_one_iff : ∀ {n : ℕ}, ArithmeticFunction.cardDistinctFactors n = 1 ↔ IsPrimePow n
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.mk.injEq : ∀ {R : Type u} [inst : Ring R] (n : ℕ) (S : Submodule R (Fin n → R)) (n_1 : ℕ) (S_1 : Submodule R (Fin n_1 → R)),
  ({ n := n, S := S } = { n := n_1, S := S_1 }) = (n = n_1 ∧ S ≍ S_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P Q : Fin 3 → R),
  W'.addY P Q = W'.negY ![W'.addX P Q, W'.negAddY P Q, W'.addZ P Q]
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Left-exactness, as a property of objects in `C ⥤ D`.  -/
CategoryTheory.leftExactFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_edgeFinset_map : ∀ {V : Type u_1} [inst : Fintype V] {W : Type u_2} [inst_1 : Fintype W] [inst_2 : DecidableEq W] (f : V ↪ W)
  (G : SimpleGraph V) [inst_3 : DecidableRel G.Adj], (SimpleGraph.map (⇑f) G).edgeFinset.card = G.edgeFinset.card
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.instInhabitedFirstObjBotPresieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) → {X : C} → Inhabited (CategoryTheory.Equalizer.FirstObj P ⊥)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ ∀ (a : α), a ∉ m
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhdsWithin_neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ closure s ↔ (nhdsWithin x s).NeBot
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.coe_eq_zero_iff : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M), ⇑χ = 0 ↔ χ.IsZero
-- Mathlib.MeasureTheory.Function.EssSup
essInf_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] (c : β), μ ≠ 0 → essInf (fun x => c) μ = c
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_neg_of_neg_of_nonpos`.  -/
add_neg_of_neg_of_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a < 0 → b ≤ 0 → a + b < 0
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabDeprecatedSyntax : Lean.Elab.Command.CommandElab
-- Mathlib.Topology.Sheaves.CommRingCat
/-- A subpresheaf with a submonoid structure on each of the components.  -/
TopCat.Presheaf.SubmonoidPresheaf : {X : TopCat} → TopCat.Presheaf CommRingCat X → Type (max u_1 w)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instZero : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Zero (CauSeq β abv)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.isDynCoverOf_univ : ∀ {X : Type u_1} {s : Set X} (T : X → X) (F : Set X) (n : ℕ), s.Nonempty → Dynamics.IsDynCoverOf T F Set.univ n s
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_le_of_nonneg : ∀ {n : ℤ} {s : ℕ}, 0 ≤ n → n >>> s ≤ n
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.coe_copy : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R)
  (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_X₂ : ∀ {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'' : κ) (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' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃
        hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).X₂ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq' hr
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- Version of `CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff` for a small
indexing type.  -/
CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C} {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B)
  [inst_2 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks]
  (x : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X),
  CategoryTheory.Presieve.Arrows.Compatible P π
      ((equivShrink ((i : I) → P.obj (Opposite.op (X i)))).symm
        ((CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Types.Small.productIso fun i => P.obj (Opposite.op (X i))).hom)
          x)) ↔
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π)) x
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.instVAddOfVAddCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : VAdd M X] → [inst_1 : VAdd N Y] → [inst_2 : VAdd R Y] → [VAddCommClass N R Y] → VAdd R (X →ₑ[σ] Y)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instIsLinearPreorderOpposite : ∀ {α : Type u_1} {i : LE α} [Std.IsLinearPreorder α], Std.IsLinearPreorder α
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`.  -/
GradedTensorProduct.includeRight : {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) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              [inst_9 : Module ι (Additive ℤˣ)] → B →ₐ[R] GradedTensorProduct R 𝒜 ℬ
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabHtmlText : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `ProofWidgets.Jsx.jsxText)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The preimage of a subset of the base set is homeomorphic to the product with the fiber.  -/
Bundle.Trivialization.preimageHomeomorph : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e : Bundle.Trivialization F proj) → {s : Set B} → s ⊆ e.baseSet → ↑(proj ⁻¹' s) ≃ₜ ↑s × F
-- Mathlib.Computability.EpsilonNFA
εNFA.evalFrom.eq_1 : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ), M.evalFrom start = List.foldl M.stepSet (M.εClosure start)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `S` is `R`-standard smooth of relative dimension zero, it is étale.  -/
Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmoothOfRelativeDimension 0 R S], Algebra.Etale R S
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_zero_iff_left : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → (a * b = 0 ↔ b = 0)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.functorPushforward_equalizer_mem : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [G.IsLocallyFaithful K] {U V : C}
  (f₁ f₂ : U ⟶ V),
  G.map f₁ = G.map f₂ → CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K (G.obj U)
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_lt : ∀ {x : ℤ} {m : ℕ}, 0 < m → x.bmod m < (↑m + 1) / 2
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformGroup.uniformity_eq : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : Group G} [self : IsRightUniformGroup G],
  uniformity G = Filter.comap (fun x => x.2 * x.1⁻¹) (nhds 1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RcoSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {a b : α}
  (hab : cmp a b = Ordering.eq) {h' : a ∈ t}, t[a] = t[b]
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddGrpCat.binaryProductLimitCone_isLimit_lift : ∀ (G H : AddGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    AddGrpCat.ofHom
      ((AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (AddGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `b` is a basis of `M` (indexed by a linearly ordered type), the basis of the `n`th
exterior power of `M` formed by the `n`-fold exterior products of elements of `b`.  -/
Module.Basis.exteriorPower : {R : Type u_1} →
  {M : Type u_3} →
    (n : ℕ) →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {I : Type u_5} → [LinearOrder I] → Module.Basis I R M → Module.Basis (↑(Set.powersetCard I n)) R ↥(⋀[R]^n M)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_inter_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a ∩ Set.Ioi b = Set.Ioi (max a b)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- If `g = h ∘ f`, then the sigma-algebra generated by `g` is
smaller than the one generated by `f`.  -/
MeasurableSpace.comap_le_comap_of_eq_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β} {g : α → γ}
  (h : β → γ), Measurable h → g = h ∘ f → MeasurableSpace.comap g mγ ≤ MeasurableSpace.comap f mβ
-- Mathlib.RingTheory.Ideal.Over
Ideal.ne_bot_of_mem_primesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {p : Ideal A} {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B]
  [FaithfulSMul A B], p ≠ ⊥ → ∀ {P : Ideal B}, P ∈ p.primesOver B → P ≠ ⊥
-- Mathlib.Probability.Process.Stopping
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.stoppedProcess`. -/
MeasureTheory.ProgMeasurable.stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace ι],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_const_mul : ∀ {n : ℕ} (a : ℂ) (f : (Fin n → ℂ) → ℂ) (c : Fin n → ℂ) (R : Fin n → ℝ),
  (∯ (x : Fin n → ℂ) in T(c, R), a * f x) = a * ∯ (x : Fin n → ℂ) in T(c, R), f x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₂ f₂ = h.p
-- Mathlib.Topology.Neighborhoods
mem_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.coe_chainTop' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  ⇑(LieModule.chainTop α β) = LieModule.chainTopCoeff α β • α + ⇑β
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `add_tsub_add_eq_tsub_left` for the equality.  -/
add_tsub_add_le_tsub_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b - (a + c) ≤ b - c
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖
-- Init.Internal.Order.Basic
Lean.Order.instCCPOStateT : {m : Type u_1 → Type u_2} →
  {σ α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.CCPO (m α)] → Lean.Order.CCPO (StateT σ m α)
-- Mathlib.SetTheory.ZFC.Basic
/-- The binary intersection operation  -/
ZFSet.inter : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Mathlib.RingTheory.Ideal.Pure
/-- [Stacks Tag 04PT](https://stacks.math.columbia.edu/tag/04PT) -/
Ideal.zeroLocus_inj_of_pure : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.Pure] [J.Pure],
  PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑J ↔ I = J
-- Mathlib.Algebra.Prime.Defs
Prime.not_dvd_one : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ¬p ∣ 1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeWhile_iff_dropWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  (s.takeWhile pat).isEmpty = true ↔ s.dropWhile pat = s
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.permutationsAux.rec.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (t : α) (ts is : List α) (h_1 : (is : List α) → motive [] is)
  (h_2 : (t : α) → (ts is : List α) → motive (t :: ts) is),
  (match t :: ts, is with
    | [], is => h_1 is
    | t :: ts, is => h_2 t ts is) =
    h_2 t ts is
-- Mathlib.Data.Set.Function
Function.invFunOn_pos : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {b : β} [inst : Nonempty α],
  (∃ a ∈ s, f a = b) → Function.invFunOn f s b ∈ s ∧ f (Function.invFunOn f s b) = b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_def : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (p : Polynomial R),
  Polynomial.eval₂ f x p = p.sum fun e a => f a * x ^ e
-- Mathlib.Order.BooleanAlgebra.Set
Set.instBooleanAlgebra : {α : Type u_1} → BooleanAlgebra (Set α)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.mem_op : ∀ {M : Type u_2} [inst : AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M}, x ∈ S.op ↔ AddOpposite.unop x ∈ S
-- Mathlib.Topology.Maps.Basic
IsClosedMap.of_nonempty : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)) → IsClosedMap f
-- Mathlib.Data.Matrix.Basis
Matrix.submonoidCenter_eq_scalar_map : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α],
  Submonoid.center (Matrix n n α) = Submonoid.map (Matrix.scalar n) (Submonoid.center α)
-- Mathlib.Order.Interval.Finset.Defs
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.  -/
IsEmpty.toLocallyFiniteOrderTop : {α : Type u_1} → [inst : Preorder α] → [IsEmpty α] → LocallyFiniteOrderTop α
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeD.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        (x_2 : α) →
          ((x : List α) → (x_3 : α) → motive 0 x x_3) →
            ((n : ℕ) → (l : List α) → (x : α) → motive n.succ l x) → motive x x_1 x_2
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend'_toFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)] (z : Z),
  ↑(Bundle.Pretrivialization.codExtend' hs e).toPartialEquiv z = (↑(↑e z).1, (↑e z).2)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The right unitor in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} →
      (α : a ⟶ b) → CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.id b) ≅ α
-- Mathlib.Analysis.Real.Pi.Wallis
/-- Wallis' product formula for `π / 2`.  -/
Real.tendsto_prod_pi_div_two : Filter.Tendsto (fun k => ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))) Filter.atTop
  (nhds (Real.pi / 2))
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.toGroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G],
  SubgroupClass.toGroup H =
    { toMonoid := SubmonoidClass.toMonoid H, toInv := InvMemClass.inv, toDiv := SubgroupClass.div, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }