mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.ι_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (self : HomotopicalAlgebra.PrepathObject A),
  CategoryTheory.CategoryStruct.comp self.ι self.p₁ = CategoryTheory.CategoryStruct.id A
-- Mathlib.Algebra.Group.Opposite
AddOpposite.op_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), AddOpposite.op (a ^ b) = AddOpposite.op a ^ b
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_snd_eq_self_iff_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ S → (↑(hST.equiv g).2 = g ↔ g ∈ T)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_sub_left_image : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, ⋃ a ∈ s, (fun x => a - x) '' t = s - t
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.Tendsto.subseq_mem_entourage : ∀ {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α},
  (∀ (n : ℕ), V n ∈ uniformity α) →
    ∀ {u : ℕ → α} {a : α},
      Filter.Tendsto u Filter.atTop (nhds a) →
        ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_sup : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K] {E F : Subfield K}
  [hE : NumberField.IsTotallyReal ↥E] [hF : NumberField.IsTotallyReal ↥F], NumberField.IsTotallyReal ↥(E ⊔ F)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_mk : ∀ {G : Type u_1} [inst : Group G] {s : Submonoid G} {x : G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier),
  x ∈ { toSubmonoid := s, inv_mem' := h_inv } ↔ x ∈ s
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₂_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃))
      f₂ =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃
-- Mathlib.CategoryTheory.Limits.Final.Type
CategoryTheory.Functor.sectionsPrecomp_coe : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {P : CategoryTheory.Functor D (Type w)} (x : ↑P.sections) (x_1 : C),
  ↑(F.sectionsPrecomp x) x_1 = ↑x (F.obj x_1)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_isFlat_iff : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : IsDomain A] {s : Set A},
  (AlgebraicIndependent.matroid R A).IsFlat s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
-- Lean.ExtraModUses
_private.Lean.ExtraModUses.0.Lean.recordExtraModUseCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadTrace m] →
        [Lean.MonadOptions m] →
          [Lean.MonadRef m] →
            [Lean.AddMessageContext m] → Lean.Name → Bool → optParam Lean.Name Lean.Name.anonymous → m Unit
-- Init.Data.SInt.Lemmas
ISize.le_antisymm_iff : ∀ {a b : ISize}, a = b ↔ a ≤ b ∧ b ≤ a
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.parseTagged : Lean.Json → String → ℕ → Option (Array Lean.Name) → Except String (Array Lean.Json)
-- Mathlib.Order.RelClasses
Order.Preimage.instTotal : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Total r] {f : β → α}, Std.Total (f ⁻¹'o r)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
right_ne_zero_of_smul : ∀ {M : Type u_1} {A : Type u_7} [inst : Zero A] [inst_1 : SMulZeroClass M A] {a : M} {b : A}, a • b ≠ 0 → b ≠ 0
-- Mathlib.Topology.Order
continuous_sSup_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β},
  Continuous f ↔ ∀ t ∈ T, Continuous f
-- Mathlib.Algebra.Group.ULift
ULift.subNegAddMonoid.eq_1 : ∀ {α : Type u} [inst : SubNegMonoid α],
  ULift.subNegAddMonoid = Function.Injective.subNegMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.Spec
/-- The counit morphism `R ⟶ Γ(Spec R)` given by `AlgebraicGeometry.StructureSheaf.toOpen`.  -/
AlgebraicGeometry.toSpecΓ : (R : CommRingCat) →
  R ⟶
    AlgebraicGeometry.LocallyRingedSpace.Γ.obj
      (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R)))
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isUniformInducing_closure : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformInducing closure
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withAlts.mkNotAlt : Array Lean.Expr → Array Lean.Expr → Lean.Meta.Match.AltLHS → Lean.MetaM Lean.Expr
-- Init.Data.SInt.Lemmas
Int64.toInt.inj : ∀ {x y : Int64}, x.toInt = y.toInt → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.of_has_biproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
-- Mathlib.Algebra.Free
FreeSemigroup.traverse_mul' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) [LawfulApplicative m],
  Function.comp (traverse F) ∘ HMul.hMul = fun x y => (fun x1 x2 => x1 * x2) <$> traverse F x <*> traverse F y
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_multiset_of_isEmpty : ∀ (α : Type u) [IsEmpty α], Cardinal.mk (Multiset α) = 1
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), s.compl = { carrier := (↑s)ᶜ, lower' := ⋯ }
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.mem_closure_tfae : ∀ (a : Ordinal.{u}) (s : Set Ordinal.{u}),
  [a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a,
      ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE
-- Mathlib.Data.Finset.Functor
Finset.instLawfulMonad : ∀ [inst : (P : Prop) → Decidable P], LawfulMonad Finset
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.apply : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_5} {p : ι → Type u_6} {g : α → (x : ι) → p x},
  Filter.EventuallyConst g l → ∀ (i : ι), Filter.EventuallyConst (fun x => g x i) l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, Std.ExtDHashMap.Const.get? (m.erase k) k = none
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- A base of a root system yields a basis of the coroot space.  -/
RootPairing.Base.toCoweightBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [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} → (b : P.Base) → [P.IsRootSystem] → Module.Basis (↥b.support) R N
-- Init.BinderPredicates
/-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...`  -/
Lean.«binderPred<_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.eqToHom_comp_lift_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b b' : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : b = b'),
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.eqToHom h)) ↔ p.IsHomLift f φ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mem_span_pow_iff_le_valuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]), x ≠ 0 → ∀ (n : ℕ), x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation
-- Std.Data.DHashMap.Internal.HashesTo
Std.DHashMap.Internal.mkIdx.congr_simp : ∀ (sz : ℕ) (h : 0 < sz) (hash hash_1 : UInt64),
  hash = hash_1 → Std.DHashMap.Internal.mkIdx sz h hash = Std.DHashMap.Internal.mkIdx sz h hash_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.k_quaternionBasis : ∀ {R : Type u_1} [inst : CommRing R] (c₁ c₂ : R),
  (CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).k =
    (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) *
      (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.mk : {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₂} →
                {R R' : Φ.RightResolution X₂} →
                  (f : R.X₁ ⟶ R'.X₁) →
                    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f) = R'.w)
                        CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam →
                      R.Hom R'
-- Mathlib.Order.Heyting.Basic
PUnit.sdiff_eq : ∀ (a b : PUnit.{u + 1}), b \ a = PUnit.unit
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If a finset has cardinality larger than `finrank + 1`,
then there is a nontrivial linear relation amongst its elements,
such that the coefficients of the relation sum to zero.  -/
Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [StrongRankCondition R] {t : Finset M},
  Module.finrank R M + 1 < t.card → ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mapFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D), CategoryTheory.Square.mapFunctor.obj F = F.mapSquare
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eventually_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {q : α → Prop}, (∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isInducing_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsInducing ⇑DomAddAct.mk
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.isRegular_X : ∀ {R : Type u} [inst : Semiring R], IsRegular Polynomial.X
-- Mathlib.Data.Fin.Tuple.Finset
Finset.card_insertNthEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {p : Fin (n + 1)} (S : (i : Fin (n + 1)) → Finset (α i))
  (P : ((i : Fin n) → α (p.succAbove i)) → Prop) [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (p.removeNth r)}.card = (S p).card * {r ∈ Fintype.piFinset (p.removeNth S) | P r}.card
-- Std.Data.DTreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Raw.modify : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → Std.DTreeMap.Raw α β cmp → (a : α) → (β a → β a) → Std.DTreeMap.Raw α β cmp
-- Init.Core
instDecidableEqOfIff : {p q : Prop} → [d : Decidable (p ↔ q)] → Decidable (p = q)
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEquiv.map_map_symm : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Topology.Category.Sequential
/-- Construct an isomorphism from a homeomorphism.  -/
Sequential.isoOfHomeo : {X Y : Sequential} → ↑X.toTop ≃ₜ ↑Y.toTop → (X ≅ Y)
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_mul : ∀ {F : Type u} [inst : Field F] (f g : Polynomial F), (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.instCommSemiringAdjoinSingleton : (R : Type u) →
  {A : Type z} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (x : A) → CommSemiring ↥R[x]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (val val_1 : BitVec w),
  val = val_1 →
    ∀ (curr : ℕ) (s s_1 : aig.RefVec curr),
      s = s_1 →
        ∀ (hcurr : curr ≤ w),
          Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val curr s hcurr =
            Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig val_1 curr s_1 hcurr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE_comp_ofLEMk_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g]
  (h₁ : CategoryTheory.Subobject.mk f ≤ X) (h₂ : X ≤ CategoryTheory.Subobject.mk g) {Z : C} (h : A₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁)
      (CategoryTheory.CategoryStruct.comp (X.ofLEMk g h₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g ⋯) h
-- Mathlib.Tactic.Push
_private.Mathlib.Tactic.Push.0.Mathlib.Tactic.Push.pushNegBuiltin.mkSimpStep : Lean.Expr → Lean.Expr → Lean.Meta.Simp.Step
-- Plausible.Functions
Plausible.TotalFunction.shrink.dedup : {α : Type u_1} → {β : Type u_2} → [DecidableEq α] → List ((_ : α) × β) → List ((_ : α) × β)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.symm_mulLeft_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u : ↥(unitary A)) (x : A),
  ((Unitary.mulLeft R A) u).symm x = star ↑u * x
-- Mathlib.Analysis.Analytic.Composition
/-- Bounding below the radius of the composition of two formal multilinear series assuming
summability over all compositions.  -/
FormalMultilinearSeries.le_comp_radius_of_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (r : NNReal),
  (Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst) → ↑r ≤ (q.comp p).radius
-- Mathlib.Data.Matrix.PEquiv
/-- Restatement of `single_mul_single`, which will simplify expressions in `simp` normal form,
when associativity may otherwise need to be carefully applied.  -/
PEquiv.single_mul_single_right : ∀ {k : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : Fintype k]
  [inst_2 : DecidableEq n] [inst_3 : DecidableEq k] [inst_4 : DecidableEq m] [inst_5 : Semiring α] (a : m) (b : n)
  (c : k) (M : Matrix k l α),
  (PEquiv.single a b).toMatrix * ((PEquiv.single b c).toMatrix * M) = (PEquiv.single a c).toMatrix * M
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- This is the key theorem to prove the existence of the `traj`:
the `trajContent` of a decreasing sequence of cylinders with empty intersection
converges to `0`.

This implies the `σ`-additivity of `trajContent`
(see `addContent_iUnion_eq_sum_of_tendsto_zero`),
which allows to extend it to the `σ`-algebra by Carathéodory's theorem.  -/
ProbabilityTheory.Kernel.trajContent_tendsto_zero : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {A : ℕ → Set ((n : ℕ) → X n)},
  (∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) →
    Antitone A →
      ⋂ n, A n = ∅ →
        ∀ {p : ℕ} (x₀ : (i : ↥(Finset.Iic p)) → X ↑i),
          Filter.Tendsto (fun n => (ProbabilityTheory.Kernel.trajContent κ x₀) (A n)) Filter.atTop (nhds 0)
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_of_comm`. -/
isSolvable_of_comm : ∀ {G : Type u_3} [hG : Group G], (∀ (a b : G), a * b = b * a) → Group.IsSolvable G
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.map.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  W.map f = { a₁ := f W.a₁, a₂ := f W.a₂, a₃ := f W.a₃, a₄ := f W.a₄, a₆ := f W.a₆ }
-- Mathlib.Topology.Constructions
Topology.IsClosedEmbedding.inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (hst : s ⊆ t),
  IsClosed (Subtype.val ⁻¹' s) → Topology.IsClosedEmbedding (Set.inclusion hst)
-- Mathlib.Data.Finset.Grade
CovBy.card_finset : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → s.card ⋖ t.card
-- Mathlib.GroupTheory.Sylow
Sylow.sSup_of_normal : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (Hs : Set (Subgroup G)),
  (∀ H ∈ Hs, IsPGroup p ↥H) → (∀ H ∈ Hs, H.Normal) → IsPGroup p ↥(sSup Hs)
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- The localized category for `W : MorphismProperty C`
that is fixed by the `[HasLocalization W]` instance.  -/
CategoryTheory.MorphismProperty.Localization' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (W : CategoryTheory.MorphismProperty C) → [W.HasLocalization] → Type u
-- Mathlib.Data.Rat.Floor
Rat.floor_natCast_div_natCast : ∀ (n d : ℕ), ⌊↑n / ↑d⌋ = ↑n / ↑d
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec.eq_def : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.ushiftRightRec y n =
    have shiftAmt := y &&& BitVec.twoPow w₂ n;
    match n with
    | 0 => x >>> shiftAmt
    | n.succ => x.ushiftRightRec y n >>> shiftAmt
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.toSubgraph_iff : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} (h : M.spanningCoe ≤ G'),
  (SimpleGraph.toSubgraph M.spanningCoe h).IsPerfectMatching ↔ M.IsPerfectMatching
-- Mathlib.Data.Stream.Init
Stream'.take.eq_2 : ∀ {α : Type u} (x : Stream' α) (n : ℕ), Stream'.take n.succ x = x.head :: Stream'.take n x.tail
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_pred : ∀ (o : Ordinal.{v}), Ordinal.lift.{u, v} o.pred = (Ordinal.lift.{u, v} o).pred
-- Mathlib.Condensed.Solid
/-- The free condensed `R`-module on a profinite space.  -/
Condensed.profiniteFree : (R : Type (u + 1)) → [inst : Ring R] → CategoryTheory.Functor Profinite (CondensedMod R)
-- Mathlib.GroupTheory.OrderOfElement
pow_finEquivZPowers_symm_apply : ∀ {G : Type u_1} [inst : Group G] {x : G} (hx : IsOfFinOrder x) (a : ↥(Subgroup.zpowers x)),
  x ^ ↑((finEquivZPowers hx).symm a) = ↑a
-- Mathlib.Algebra.Star.Basic
IsRightRegular.star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsRightRegular x → IsLeftRegular (star x)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.support_optionEquivLeft : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial (Option σ) R),
  ((MvPolynomial.optionEquivLeft R σ) p).support = Finset.image (fun m => m none) p.support
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_finrank_range_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), T.singularValues (Module.finrank 𝕜 ↥T.range) = 0
-- Mathlib.Algebra.Module.Equiv.Defs
/-- See Note [custom simps projection]  -/
LinearEquiv.Simps.apply : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M → M₂
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- Indicator of a set as an element of `Lp`.  -/
MeasureTheory.indicatorConstLp : {α : Type u_1} →
  {E : Type u_2} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : NormedAddCommGroup E] →
          {s : Set α} → (p : ENNReal) → MeasurableSet s → μ s ≠ ⊤ → E → ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_lt_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  s.sup' H f < a ↔ ∀ i ∈ s, f i < a
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.collect : Lean.Meta.Grind.TGrind → Lean.Meta.Grind.Collector.Collect✝ Unit
-- Lean.Environment
Lean.PersistentEnvExtension.statsFn : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → σ → Std.Format
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.orderOf_le_card : ∀ {G : Type u_6} [inst : Group G] (s : Subgroup G), (↑s).Finite → ∀ {x : G}, x ∈ s → orderOf x ≤ Nat.card ↥s
-- Mathlib.Order.TransfiniteIteration
top_mem_range_transfiniteIterate : ∀ {I : Type u} [inst : CompleteLattice I] (φ : I → I) (i₀ : I) {J : Type w} [inst_1 : LinearOrder J] [OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J],
  (∀ (i : I), i ≠ ⊤ → i < φ i) →
    φ ⊤ = ⊤ → (¬Function.Injective fun j => transfiniteIterate φ j i₀) → ∃ j, transfiniteIterate φ j i₀ = ⊤
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source) is a
`PartialHomeomorph`.  -/
PartialHomeomorph.ofContinuousOpenRestrict : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialEquiv X Y) →
          ContinuousOn (↑e) e.source → IsOpenMap (e.source.domRestrict ↑e) → PartialHomeomorph X Y
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinOnBall.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G}
  {pf : FormalMultilinearSeries 𝕜 F G} {s : Set F} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f pf s (u x) r →
    HasFPowerSeriesWithinOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) (⇑u ⁻¹' s) x (r / ‖u‖ₑ)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.isBase_iff_ground_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → (M.IsBase I ↔ M.E ⊆ M.closure I)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.mk.sizeOf_spec : ∀ (bRiemann bHenstock bDistortion : Bool),
  sizeOf { bRiemann := bRiemann, bHenstock := bHenstock, bDistortion := bDistortion } =
    1 + sizeOf bRiemann + sizeOf bHenstock + sizeOf bDistortion
-- Std.Http.Server.Handler
/-- Function called when an I/O or transport error occurs. The default does nothing.
 -/
Std.Http.Server.StatelessHandler.onFailure : Std.Http.Server.StatelessHandler → IO.Error → Std.Async.Async Unit