mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
isStationary_iUnion_iff : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {ι : Type u} {f : ι → Set α},
  Order.cof α ≠ Cardinal.aleph0 →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < Cardinal.lift.{u, v} (Order.cof α) →
      (IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i))
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.convOne_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] (c : C),
  (WithConv.ofConv 1) c = (algebraMap R A) (CoalgebraStruct.counit c)
-- Mathlib.Data.Set.Image
Set.exists_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : Set β → Prop}, (∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)
-- Mathlib.NumberTheory.Pell
/-- If `(x, y)` is a solution with `x` and `y` positive, then all its powers with positive
natural exponents have positive `y`.  -/
Pell.Solution₁.y_pow_succ_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ (n : ℕ), 0 < (a ^ n.succ).y
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
IsEmpty.elim.congr_simp : ∀ {α : Sort u} (x : IsEmpty α) {p : α → Sort v} (a : α), x.elim a = x.elim a
-- Mathlib.Data.Nat.Pairing
Nat.unpair_lt : ∀ {n : ℕ}, 1 ≤ n → (Nat.unpair n).1 < n
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.rename.injEq : ∀ (a a_1 : Lean.Lsp.RenameFile), (Lean.Lsp.DocumentChange.rename a = Lean.Lsp.DocumentChange.rename a_1) = (a = a_1)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.coe_prodComm : ∀ (α : Type u) (β : Type u_1) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  ⇑(UniformEquiv.prodComm α β) = Prod.swap
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.yonedaEquiv_coe : ∀ {X : SSet} {A : X.Subcomplex} {n : SimplexCategory} (f : SSet.stdSimplex.obj n ⟶ A.toSSet),
  ↑(SSet.yonedaEquiv f) = SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp f A.ι)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.δ_naturality_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) {Z : C} (h : S₂.X₁.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₁ j) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i)
      (CategoryTheory.CategoryStruct.comp (hS₂.δ i j hij) h)
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardStateStats : Inhabited Aesop.ForwardStateStats
-- Mathlib.Algebra.GroupWithZero.Defs
IsRightCancelMulZero.to_isLeftCancelMulZero : ∀ {M₀ : Type u_1} [inst : CommMagma M₀] [inst_1 : Zero M₀] [IsRightCancelMulZero M₀], IsLeftCancelMulZero M₀
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_self : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m] (M : Matrix m n R)
  (i : n), ((Matrix.toLin v₁ v₂) M) (v₁ i) = ∑ j, M j i • v₂ j
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_neg : ∀ {w : ℕ} (a : BitVec w), a + (~~~a + 1#w) = 0#w
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F')
  (X : CategoryTheory.Grp C), ((CategoryTheory.Functor.mapGrpNatIso e).inv.app X).hom.hom = e.inv.app X.X
-- Mathlib.AlgebraicTopology.MooreComplex
AlgebraicTopology.normalizedMooreComplex_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.normalizedMooreComplex C).obj X = AlgebraicTopology.NormalizedMooreComplex.obj X
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.map_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y') [inst_2 : CategoryTheory.Limits.HasKernel f]
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (q : Y ⟶ Y')
  (w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp 0 f'),
  CategoryTheory.Limits.kernel.map f f' 0 q w = 0
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `single` as a linear map  -/
HahnSeries.single.linearMap : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid V] → [inst_3 : Module R V] → Γ → V →ₗ[R] HahnSeries Γ V
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instInhabitedOrigin : Inhabited Lean.Meta.Grind.Origin
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.MonoidalClosed.linearHomEquivComm_symm_hom : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G) (f : A ⟶ B ⟹ C),
  (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquivComm A B C).symm f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).toLinearMap
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜], (absConvexHull 𝕜) ∅ = ∅
-- Lean.Elab.MacroArgUtil
_private.Lean.Elab.MacroArgUtil.0.Lean.Elab.Command.expandMacroArg.mkAntiquotNode : Lean.TSyntax `stx → Lean.Term → Lean.Elab.Command.CommandElabM Lean.Term
-- Init.Data.Bool
Bool.or_eq_left_iff_imp : ∀ {a b : Bool}, (a || b) = a ↔ b = true → a = true
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsModuleConvexSpace.mk : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M],
  (∀ (w : Convexity.StdSimplex R M), Convexity.sConvexComb w = w.weights.sum fun m r => r • m) →
    Convexity.IsModuleConvexSpace R M
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientKerEquivRange.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P),
  Con.quotientKerEquivRange f =
    { toEquiv := Equiv.ofBijective ⇑((MulEquiv.submonoidCongr ⋯).toMonoidHom.comp (Con.kerLift f).mrangeRestrict) ⋯,
      map_mul' := ⋯ }
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprExpect.repr : Std.Http.Header.Expect → ℕ → Std.Format
-- Mathlib.Algebra.Module.Torsion.Basic
/-- Given an `R`-module `M` and an element `a` in `R`, submodules of the `a`-torsion submodule of
`M` do not depend on whether we take scalars to be `R` or `R ⧸ R ∙ a`.  -/
Submodule.submodule_torsionBy_orderIso : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (a : R) → Submodule (R ⧸ R ∙ a) ↥(Submodule.torsionBy R M a) ≃o Submodule R ↥(Submodule.torsionBy R M a)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup Mᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.Order.Heyting.Basic
/-- Pullback a `GeneralizedHeytingAlgebra` along an injection.  -/
Function.Injective.generalizedHeytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Top α] →
              [inst_5 : HImp α] →
                [inst_6 : GeneralizedHeytingAlgebra β] →
                  (f : α → β) →
                    Function.Injective f →
                      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                        (∀ {x y : α}, f x < f y ↔ x < y) →
                          (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                            (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                              f ⊤ = ⊤ → (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) → GeneralizedHeytingAlgebra α
-- Mathlib.NumberTheory.Modular
ModularGroup.re_T_smul : ∀ (z : UpperHalfPlane), (ModularGroup.T • z).re = z.re + 1
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_int_lt : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R), ∃ n, ↑n < x
-- Mathlib.SetTheory.Ordinal.Notation
/-- Notation for 0  -/
ONote.instZero : Zero ONote
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivAt.eventually_notMem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x →
    (∃ C, AntilipschitzWith C ⇑f') →
      ∀ (t : Set F), ¬AccPt (f x) (Filter.principal t) → ∀ᶠ (z : E) in nhdsWithin x {x}ᶜ, f z ∉ t
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_eq : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} [hF : CompleteSpace F] (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hf : MeasureTheory.Integrable f μ),
  MeasureTheory.setToFun μ T hT f = (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.instFunctor : Functor Stream'.Seq
-- Mathlib.Util.Export
Lean.Export.Entry.level : Lean.Level → Lean.Export.Entry
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_congr' : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b), ∑ i, f (Fin.cast h i) = ∑ i, f i
-- Mathlib.Data.Set.Function
Function.update_comp_eq_of_notMem_range' : ∀ {α : Sort u_7} {β : Type u_8} {γ : β → Sort u_9} [inst : DecidableEq β] (g : (b : β) → γ b) {f : α → β} {i : β}
  (a : γ i), i ∉ Set.range f → (fun j => Function.update g i a (f j)) = fun j => g (f j)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- If `f` and `g` are equivariant maps, then so is `(x, y) ↦ (f x, g y)`.  -/
MulActionHom.prodMap : {M : Type u_1} →
  {N : Type u_2} →
    {α : Type u_3} →
      {β : Type u_4} →
        {γ : Type u_5} →
          {δ : Type u_6} →
            [inst : SMul M α] →
              [inst_1 : SMul M β] →
                [inst_2 : SMul N γ] → [inst_3 : SMul N δ] → {σ : M → N} → (α →ₑ[σ] γ) → (β →ₑ[σ] δ) → α × β →ₑ[σ] γ × δ
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_surjective : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {f : M →ₗ[R] M'},
  Function.Surjective ⇑f → Function.Surjective ⇑((QuotSMulTop.map r) f)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.notification.inj : ∀ {method method_1 : String},
  Lean.JsonRpc.MessageMetaData.notification method = Lean.JsonRpc.MessageMetaData.notification method_1 →
    method = method_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isUnit_iff_singleton_aux : ∀ {α : Type u_5} [inst : Group α] {s : Finset α}, (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}
-- Mathlib.Data.Finsupp.Single
Finsupp.equivFunOnFinite.eq_1 : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Finite α],
  Finsupp.equivFunOnFinite =
    { toFun := DFunLike.coe, invFun := fun f => { support := ⋯.toFinset, toFun := f, mem_support_toFun := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toList_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {f : α → β → Bool},
  (Std.DHashMap.Const.toList (Std.DHashMap.filter f m)).Perm
    (List.filter (fun p => f p.1 p.2) (Std.DHashMap.Const.toList m))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The mixed space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`.  -/
NumberField.mixedEmbedding.mixedSpace : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
ContinuousLinearEquiv.coord_norm' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}
  (h : x ≠ 0), ‖↑‖x‖ • ContinuousLinearEquiv.coord 𝕜 x h‖ = 1
-- Mathlib.Order.Category.HeytAlg
HeytAlg.instCoeSortType : CoeSort HeytAlg (Type u_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.comp_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Under X) (f : a ⟶ b)
  (g : b ⟶ c),
  CategoryTheory.Under.Hom.right (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right f) (CategoryTheory.Under.Hom.right g)
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.coe_singleton : ∀ {ι : Type u_7} {R : Type u_8} [inst : Unique ι] [inst_1 : Semiring R], ⇑(Module.Basis.singleton ι R) = 1
-- Std.Data.ExtTreeMap.Basic
/-- Internal implementation detail of the tree map.  -/
Std.ExtTreeMap.inner : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1} →
      Std.ExtTreeMap α β cmp → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
BoundedContinuousFunction.instNonUnitalCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : NonUnitalCStarAlgebra A] → NonUnitalCStarAlgebra (BoundedContinuousFunction α A)
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.strictMono_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : Preorder β]
  (gi : GaloisInsertion l u), StrictMono u
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure_eq : ∀ {p : ↑unitInterval},
  p ≠ 0 →
    ProbabilityTheory.geometricMeasure p =
      MeasureTheory.Measure.sum fun n => ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • MeasureTheory.Measure.dirac n
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
_private.Lean.Meta.Tactic.Simp.Arith.Int.Simp.0.Int.Internal.Linear.Poly.gcdCoeffs'.go : ℕ → Int.Internal.Linear.Poly → ℕ
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.C_div : ∀ {R : Type u} {a b : R} [inst : Field R], Polynomial.C (a / b) = Polynomial.C a / Polynomial.C b
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- In characteristic zero, the exponential of a nilpotent derivation is a Lie algebra
automorphism.  -/
LieDerivation.exp : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → [LieAlgebra ℚ L] → (D : LieDerivation R L L) → IsNilpotent ↑D → L ≃ₗ⁅R⁆ L
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_inf_le : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Ico : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.Ico i j = Set.Ico ↑i ↑j
-- Mathlib.Order.Partition.Finpartition
Finpartition.ne_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (P : Finpartition s), t ∈ P.parts → t ≠ ∅
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- An idempotent operator `f` commutes with a unit operator `T` if and only if
`T (range f) = range f` and `T (ker f) = ker f`.  -/
ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : IsTopologicalAddGroup M] {f T : M →L[R] M},
  IsUnit T →
    IsIdempotentElem f →
      (Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker)
-- Mathlib.Order.Heyting.Hom
CoheytingHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] {f : CoheytingHom α β},
  f.toFun = ⇑f
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuousOn.const` -/
ScottContinuousOn.fun_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {D : Set (Set α)} (x : β),
  ScottContinuousOn D fun x_1 => x
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.one : ℝ
-- Mathlib.Order.Category.Preord
Preord.hom_ofHom : ∀ {X Y : Type u} [inst : Preorder X] [inst_1 : Preorder Y] (f : X →o Y), Preord.Hom.hom (Preord.ofHom f) = f
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraPowerSeries : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [Algebra R A] → Algebra (PowerSeries R) (PowerSeries A)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.alternatingWord.eq_def : ∀ {B : Type u_1} (i i' : B) (m : ℕ),
  CoxeterSystem.alternatingWord i i' m =
    match m with
    | 0 => []
    | m.succ => (CoxeterSystem.alternatingWord i' i m).concat i'
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.leftRel_prod : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {β : Type u_2} [inst_1 : Group β] (s' : Subgroup β),
  QuotientGroup.leftRel (s.prod s') = (QuotientGroup.leftRel s).prod (QuotientGroup.leftRel s')
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasFDerivAt_exp_smul_const : ∀ (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝕊] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝕊] [inst_4 : NormedAlgebra 𝕂 𝔸] [inst_5 : Algebra 𝕊 𝔸] [inst_6 : ContinuousSMul 𝕊 𝔸]
  [inst_7 : IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊),
  HasFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.smul_mem_rootSet_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  {G : Type u_1} [inst_4 : Group G] [inst_5 : MulSemiringAction G R] [SMulCommClass G S R] {f : Polynomial S} {g : G}
  {x : R}, g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R
-- Mathlib.CategoryTheory.Types.Set
/-- Given `X : Type u`, this is the functor `Set X ⥤ Type u` which sends `A`
to its underlying type.  -/
Set.functorToTypes : {X : Type u} → CategoryTheory.Functor (Set X) (Type u)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.to_subset : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {t : ι → Set α}, (∀ (i : ι), p i → t i ⊆ s i) → (∀ (i : ι), p i → t i ∈ l) → l.HasBasis p t
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanILeanHeaderSetupInfoParams : Lean.FromJson Lean.Lsp.LeanILeanHeaderSetupInfoParams
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instHasOfPostcompPropertyScheme : AlgebraicGeometry.IsOpenImmersion.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion
-- Std.Time.Format.Modifier
Std.Time.Modifier.k.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.k presentation) = 1 + sizeOf presentation
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceSubtype : ∀ {α : Type u_1} [inst : Bornology α] [BoundedSpace α] {p : α → Prop}, BoundedSpace (Subtype p)
-- Init.Data.Ord.Basic
Ordering.isNe_swap : ∀ {o : Ordering}, o.swap.isNe = o.isNe
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.map_mem_nthRootsFinset : ∀ {R : Type u} {n : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_1} {F : Type u_2} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [MonoidHomClass F R S] {a x : R},
  x ∈ Polynomial.nthRootsFinset n a → ∀ (f : F), f x ∈ Polynomial.nthRootsFinset n (f a)
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.mono : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P → ∀ᵐ (ω : Ω) ∂P, Monotone fun x => τ x ω
-- Std.Sync.Mutex
/-- Locks a `BaseMutex`.  Waits until no other thread has locked the mutex.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
Std.BaseMutex.lock : Std.BaseMutex → BaseIO Unit
-- Mathlib.Util.AtLocation
/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given
`loc`.
* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is
  included), and fails if any of the tactic applications fail.
* If `loc` is `*`, runs at the nondependent `Prop` hypotheses (those produced by
  `Lean.MVarId.getNondepPropHyps`) and then at the target.

This is a variant of `Lean.Elab.Tactic.withLocation`.  -/
Lean.Elab.Tactic.withNondepPropLocation : Lean.Elab.Tactic.Location →
  (Lean.FVarId → Lean.Elab.Tactic.TacticM Unit) →
    Lean.Elab.Tactic.TacticM Unit → (Lean.MVarId → Lean.Elab.Tactic.TacticM Unit) → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.ExtDTreeMap.map f t},
  (Std.ExtDTreeMap.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The condition of having a separable contraction.  -/
Polynomial.HasSeparableContraction : {F : Type u_1} → [inst : CommSemiring F] → ℕ → Polynomial F → Prop
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.PreservesInjectiveObjects.injective_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} [self : F.PreservesInjectiveObjects] {X : C},
  CategoryTheory.Injective X → CategoryTheory.Injective (F.obj X)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a⁻ᵐ ≤ 1 ↔ 1 ≤ a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_nnreal_real_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal}, (Measurable fun x => ↑(f x)) ↔ Measurable f
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.Swap.equivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Sum.Swap.equivalence C D).inverse = CategoryTheory.Sum.swap D C
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eraseKey_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  (k == a) = false →
    Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = Std.Internal.List.containsKey a l
-- Mathlib.Data.Set.Function
Set.SurjOn.nonempty_or_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → s.Nonempty ∨ t = ∅
-- Mathlib.RingTheory.Nilpotent.Basic
IsUnit.not_isNilpotent : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] {x : R}, IsUnit x → ¬IsNilpotent x
-- Mathlib.Data.Nat.Cast.Order.Basic
/-- `Nat.cast : ℕ → α` as an `OrderEmbedding`  -/
Nat.castOrderEmbedding : {α : Type u_1} →
  [inst : AddMonoidWithOne α] → [inst_1 : PartialOrder α] → [AddLeftMono α] → [ZeroLEOneClass α] → [CharZero α] → ℕ ↪o α