mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.Array.Scan
Array.back_scanr : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α}, (Array.scanr f init as).back ⋯ = init
-- Mathlib.Algebra.Order.Floor.Div
/-- Typeclass for division rounded up. For each `a > 0`, this asserts the existence of a left
adjoint to the map `b ↦ a • b : β → β`.  -/
CeilDiv : (α : Type u_2) →
  (β : Type u_3) →
    [AddCommMonoid α] →
      [PartialOrder α] → [inst : AddCommMonoid β] → [PartialOrder β] → [SMulZeroClass α β] → Type (max u_2 u_3)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C),
  (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app { len := 0 }
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.nontrivial_iff : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), Nontrivial ↥ρ.invtSubmodule ↔ Nontrivial V
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.BaseMutexImpl : NonemptyType
-- Lean.Message
Lean.MessageLog.errorsToWarnings : Lean.MessageLog → Lean.MessageLog
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableStateMRpcObjectStore : {α : Type} → [Lean.Server.RpcEncodable α] → Lean.Server.RpcEncodable (StateM Lean.Server.RpcObjectStore α)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.ofPNatMultiset.congr_simp : ∀ (v v_1 : Multiset ℕ+) (e_v : v = v_1) (h : ∀ p ∈ v, p.Prime),
  PrimeMultiset.ofPNatMultiset v h = PrimeMultiset.ofPNatMultiset v_1 ⋯
-- Mathlib.Topology.Partial
open_dom_of_pcontinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X →. Y},
  PContinuous f → IsOpen f.Dom
-- Mathlib.Algebra.Lie.Submodule
LieSubalgebra.topEquiv_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : ↥⊤),
  LieSubalgebra.topEquiv x = ↑x
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and insert all of its elements into `t`.  -/
Std.DTreeMap.Internal.Impl.insertMany : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ ((a : α) × β a)] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.Balanced → t.IteratedInsertionInto
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- Pushforward of a normed add torsor along a surjective map.  -/
Function.Surjective.normedAddTorsor : {V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : PseudoMetricSpace P] →
        [inst_2 : NormedAddTorsor V P] →
          {Q : Type u_6} →
            [inst_3 : VAdd V Q] →
              [inst_4 : VSub V Q] →
                [inst_5 : PseudoMetricSpace Q] →
                  (f : P → Q) →
                    Function.Surjective f →
                      (∀ (c : V) (x : P), f (c +ᵥ x) = c +ᵥ f x) →
                        (∀ (x y : P), x -ᵥ y = f x -ᵥ f y) →
                          (∀ (x y : P), dist x y = dist (f x) (f y)) → NormedAddTorsor V Q
-- Mathlib.Data.Matrix.Basis
Matrix.subsemiringCenter_eq_scalar_map : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α],
  Subsemiring.center (Matrix n n α) = Subsemiring.map (Matrix.scalar n) (Subsemiring.center α)
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X X_1 : CategoryTheory.Dial C),
  X = X_1 → ∀ (Y Y_1 : CategoryTheory.Dial C), Y = Y_1 → X.Hom Y = X_1.Hom Y_1
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.one_def : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → One (M i)], 1 = fun x => 1
-- Mathlib.Algebra.Tropical.Lattice
instConditionallyCompleteLinearOrderTropical : {R : Type u_1} → [ConditionallyCompleteLinearOrder R] → ConditionallyCompleteLinearOrder (Tropical R)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n],
  Topology.IsClosedEmbedding ⇑(Matrix.SpecialLinearGroup.mapGL ℝ)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_succAbove : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 1)),
  SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd ((SSet.prodStdSimplex.pairingCore.min x hd).castSucc.succAbove i) =
    (SSet.prodStdSimplex.objEquiv (x.cast hd).simplex) i
-- Mathlib.Algebra.MvPolynomial.Cardinal
/-- The cardinality of the multivariate polynomial ring, `MvPolynomial σ R` is at most the maximum
of `#R`, `#σ` and `ℵ₀`.

See `cardinalMk_le_max` for the universe monomorphic version.  -/
MvPolynomial.cardinalMk_le_max_lift : ∀ {σ : Type u} {R : Type v} [inst : CommSemiring R],
  Cardinal.mk (MvPolynomial σ R) ≤
    max (max (Cardinal.lift.{u, v} (Cardinal.mk R)) (Cardinal.lift.{v, u} (Cardinal.mk σ))) Cardinal.aleph0
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.instOrderBot : {ι : Type u_1} → {I : BoxIntegral.Box ι} → OrderBot (BoxIntegral.Prepartition I)
-- Lean.Parser.Basic
Lean.Parser.instOrElseParserFn : OrElse Lean.Parser.ParserFn
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), f.ReadyForRupAdd → (f.insert c).ReadyForRupAdd
-- Mathlib.Analysis.Complex.Basic
Complex.eq_coe_norm_of_nonneg : ∀ {z : ℂ}, 0 ≤ z → z = ↑‖z‖
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A minimal Weierstrass equation for a given Weierstrass curve over `K`.  -/
WeierstrassCurve.minimal : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} →
          [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → WeierstrassCurve K
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition`. -/
Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N →
    (∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) →
      ∃ t,
        t.inf id = N ∧
          (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
            (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical) ∧
              ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing morphism  -/
CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
          CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer F ⟶
            F.obj CategoryTheory.Limits.WalkingParallelPair.zero
-- Mathlib.MeasureTheory.Measure.Support
/-- A measure which is compact-inner-regular on open sets has conull support.  -/
MeasureTheory.Measure.support_mem_ae_of_innerRegularWRT_isCompact_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  μ.InnerRegularWRT IsCompact IsOpen → μ.support ∈ MeasureTheory.ae μ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_one : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M], 1⁻¹ = 1
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {g : γ → α}, UpperSemicontinuous f → Continuous g → UpperSemicontinuous (f ∘ g)
-- Mathlib.Logic.Function.Defs
Function.onFun_swap_comm : ∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β),
  Function.onFun (Function.swap f) g = Function.swap (Function.onFun f g)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.iInter : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} [Countable ι] {f : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ) → MeasureTheory.NullMeasurableSet (⋂ i, f i) μ
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.hasBasis_nhds_zero : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R],
  (nhds 0).HasBasis (fun x => True) fun γ => {x | v.restrict x < ↑γ}
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.forIn'.loop.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive __do_lift
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.C_sub : ∀ {R : Type u} (σ : Type u_1) (a a' : R) [inst : CommRing R],
  MvPolynomial.C (a - a') = MvPolynomial.C a - MvPolynomial.C a'
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.fun_cases_unfolding : ∀ (bytes : ByteArray) (i : ℕ) (motive : Option Char → Prop),
  (∀ (h : i < bytes.size),
      ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive none) →
    (∀ (h : i < bytes.size)
        (h_1 : ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.done),
        motive (ByteArray.utf8DecodeChar?.assemble₁ bytes[i] h_1)) →
      (∀ (h : i < bytes.size),
          ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
            ∀ (h_2 : i + 1 < bytes.size), motive (ByteArray.utf8DecodeChar?.assemble₂ bytes[i] bytes[i + 1])) →
        (∀ (h : i < bytes.size),
            ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.oneMore →
              ¬i + 1 < bytes.size → motive none) →
          (∀ (h : i < bytes.size),
              ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
                ∀ (h_2 : i + 2 < bytes.size),
                  motive (ByteArray.utf8DecodeChar?.assemble₃ bytes[i] bytes[i + 1] bytes[i + 2])) →
            (∀ (h : i < bytes.size),
                ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
                  ¬i + 2 < bytes.size → motive none) →
              (∀ (h : i < bytes.size),
                  ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
                    ∀ (h_2 : i + 3 < bytes.size),
                      motive (ByteArray.utf8DecodeChar?.assemble₄ bytes[i] bytes[i + 1] bytes[i + 2] bytes[i + 3])) →
                (∀ (h : i < bytes.size),
                    ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
                      ¬i + 3 < bytes.size → motive none) →
                  (¬i < bytes.size → motive none) → motive (bytes.utf8DecodeChar? i)
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_eq_one : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {n : ℤ}, ↑n = 1 ↔ n = 1
-- Init.System.IO
/-- Starts the child process in a new session and process group using `setsid`. Currently a no-op on
non-POSIX platforms.
 -/
IO.Process.SpawnArgs.setsid : IO.Process.SpawnArgs → Bool
-- Init.Data.Array.Lemmas
Array.filterMap_reverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  Array.filterMap f xs.reverse = (Array.filterMap f xs).reverse
-- Init.Data.String.Length
_private.Init.Data.String.Length.0.Nat.repeat.match_1.eq_1 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_1 a
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is upper semicontinuous at `x` within a set `s` if, for any `ε > 0`, for all
`x'` close enough to `x` in `s`, then `f x'` is at most `f x + ε`. We formulate this in a general
preordered space, using an arbitrary `y > f x` instead of `f x + ε`.  -/
UpperSemicontinuousWithinAt : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendComp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt),
  s.extendComp f g =
    CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.comp f g)).pt) ⋯
-- Mathlib.Order.Lattice
/-- The infimum distributes over the supremum  -/
DistribLattice.le_sup_inf : ∀ {α : Type u_1} [self : DistribLattice α] (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.instIsStablyFreeOfFree : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M],
  Module.IsStablyFree R M
-- Mathlib.Topology.Germ
/-- The map `Germ (𝓝 x) E → E` as an additive monoid homomorphism  -/
Filter.Germ.valueAddHom : {X : Type u_4} → {E : Type u_5} → [inst : AddMonoid E] → [inst_1 : TopologicalSpace X] → {x : X} → (nhds x).Germ E →+ E
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the Laplacian.

Version for a Schwartz function with values in continuous linear maps.  -/
SchwartzMap.integral_clm_comp_laplacian_right_eq_left : ∀ {𝕜 : Type u_2} {E : Type u_5} {F₁ : Type u_9} {F₂ : Type u_10} [inst : NormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F₁]
  [inst_4 : NormedSpace ℝ F₁] [inst_5 : NormedAddCommGroup F₂] [inst_6 : NormedSpace ℝ F₂] [inst_7 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] [inst_10 : RCLike 𝕜] [inst_11 : NormedSpace 𝕜 F₁]
  [inst_12 : NormedSpace 𝕜 F₂] (f : SchwartzMap E (F₁ →L[𝕜] F₂)) (g : SchwartzMap E F₁),
  ∫ (x : E), (f x) ((Laplacian.laplacian g) x) ∂μ = ∫ (x : E), ((Laplacian.laplacian f) x) (g x) ∂μ
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.mrange_mk' : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M}, AddMonoidHom.mrange c.mk' = ⊤
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_le_mul_of_left_le_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R]
  [AddLeftMono R], 2 ≤ a → a ≤ b → a + b ≤ a * b
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddActionOreLocalization.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X],
  AddOreLocalization.instAddActionOreLocalization =
    { toVAdd := AddOreLocalization.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_submodule_of_artinian : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), IsArtinian R M → IsArtinian R ↥N
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v)[k]? = some v
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.actionTerminalToTerm : Lean.Syntax → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.map : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {β : Type u_2} [inst_1 : DecidableEq β] {H : SimpleGraph β}
  {a : α} {f : G →g H} {p : G.Walk a a},
  Function.Bijective ⇑f → p.IsHamiltonianCycle → (SimpleGraph.Walk.map f p).IsHamiltonianCycle
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map_id : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} (M : CStarMatrix m n A), M.map id = M
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instCompleteLattice.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instCompleteLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Order.Basic
/-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then
it has second countable topology. Note that the "densely ordered" assumption cannot be dropped, see
[double arrow space](https://topology.pi-base.org/spaces/S000093) for a counterexample.  -/
SecondCountableTopology.of_separableSpace_orderTopology : ∀ (α : Type u) [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [TopologicalSpace.SeparableSpace α], SecondCountableTopology α
-- Std.Http.Data.Headers.Basic
/-- Parses a content length header value.
 -/
Std.Http.Header.ContentLength.parse : Std.Http.Header.Value → Option Std.Http.Header.ContentLength
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.natEnd.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.Γ' → Sort u_1) (x : Turing.PartrecToTM2.Γ')
  (h_1 : Unit → motive Turing.PartrecToTM2.Γ'.consₗ) (h_2 : Unit → motive Turing.PartrecToTM2.Γ'.cons)
  (h_3 : (x : Turing.PartrecToTM2.Γ') → motive x),
  (x = Turing.PartrecToTM2.Γ'.consₗ → False) →
    (x = Turing.PartrecToTM2.Γ'.cons → False) →
      (match x with
        | Turing.PartrecToTM2.Γ'.consₗ => h_1 ()
        | Turing.PartrecToTM2.Γ'.cons => h_2 ()
        | x => h_3 x) =
        h_3 x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk_surjective : ∀ {X : SSet} {A : X.Subcomplex} (s : A.N),
  ∃ n x, ∃ (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op { len := n })), s = SSet.Subcomplex.N.mk x hx hx'
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
/-- The closure of a property of objects of a category under colimits of
shape `J a` for a family of categories `J`.  -/
CategoryTheory.ObjectProperty.colimitsClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      {α : Type t} →
        (J : α → Type u') → [(a : α) → CategoryTheory.Category.{v', u'} (J a)] → CategoryTheory.ObjectProperty C
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piCongrLeft'_symm_apply : ∀ {ι : Type u_2} {ι' : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] {Y : ι → Type u_4}
  [inst_2 : (j : ι) → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (f : (b : ι') → Y (e.symm b)) (x : ι),
  (IsometryEquiv.piCongrLeft' e).symm f x = ⋯ ▸ f (e x)
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- A topological ring is nonarchimedean if its underlying topological additive
group is nonarchimedean.  -/
NonarchimedeanRing : (R : Type u_1) → [Ring R] → [TopologicalSpace R] → Prop
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Continuous.comp_stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : TopologicalSpace γ] {g : β → γ} {f : α → β},
  Continuous g → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => g (f x)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Lean.Meta.Eqns
Lean.Meta.eqUnfoldThmSuffix : String
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.isOpenMap_iff_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {H : Type u_1} [inst_3 : Monoid H]
  [inst_4 : TopologicalSpace H] [ContinuousConstSMul H H] {F : Type u_2} [inst_6 : FunLike F G H] [MonoidHomClass F G H]
  {f : F}, IsOpenMap ⇑f ↔ nhds 1 ≤ Filter.map (⇑f) (nhds 1)
-- Mathlib.Order.RelSeries
RelSeries.tail_cons : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r), (p.cons x hx).tail ⋯ = p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.fold_eq_foldl_toArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {f : δ → α → β → δ} {init : δ},
  m.WF → Std.HashMap.Raw.fold f init m = Array.foldl (fun a b => f a b.1 b.2) init m.toArray
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.forIn_eq_forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {α_1 : Type u_1} {init : α_1} {f : α → α_1 → m (ForInStep α_1)}
  [inst : Monad m] [LawfulMonad m] {t : RBTree.RBNode α}, forIn t init f = forIn t.toList init f
-- Init.Data.SInt.Lemmas
Int16.neg_inj : ∀ {a b : Int16}, -a = -b ↔ a = b
-- Std.Data.ExtDTreeMap.Basic
/-- Computes the difference of the given tree maps.
This function always iterates through the smaller map.
 -/
Std.ExtDTreeMap.diff : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.enorm : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn (fun x => ‖f x‖ₑ) s μ
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeriesBilinear.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : (x : ℕ) → motive x),
  (match 2 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | x => h_4 x) =
    h_3 ()
-- Mathlib.Analysis.Distribution.Support
Distribution.dsupport.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] (f : F → V),
  Distribution.dsupport f = ⋂₀ {s | Distribution.IsVanishingOn f sᶜ ∧ IsClosed s}
-- Init.Prelude
instDecidableEqBool : DecidableEq Bool
-- Mathlib.Combinatorics.Compactness
/-- Given a (dependent) function `g s : (a : α) → β a` for each finset `s` of `α`, provided that
each `β a` is finite, we can find another function `χ : (a : α) → β a` such that on every `s`,
there is some larger `t` such that `χ` agrees with `g t` on `s`.
Informally, we are stitching together the local functions `g s` into a global `χ` such that on
each `s`, `χ` can be expressed in terms of one of the `g`.
 -/
Finset.rado_selection : ∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : Finset α → (a : α) → β a),
  ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x