mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (l : List α),
  List.scanlM f init l = List.reverse <$> List.scanAuxM✝ f init l
-- Mathlib.Topology.Category.Compactum
instCategoryCompactum : CategoryTheory.Category.{u_1, u_1 + 1} Compactum
-- Std.Time.Date.Unit.Month
/-- Transforms `Month.Ordinal` into `Second.Offset`.
 -/
Std.Time.Month.Ordinal.toSeconds : Bool → Std.Time.Month.Ordinal → Std.Time.Second.Offset
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_iUnion : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} (s : ι → Set G),
  AddSubgroup.closure (⋃ i, s i) = ⨆ i, AddSubgroup.closure (s i)
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.range_subtype : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), p.subtype.range = p
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.one_lt_ofENat : ∀ {m : ℕ∞}, 1 < ↑m ↔ 1 < m
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_vsub_right : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x y : P),
  (Equiv.pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_iSup : ∀ {ι : Sort u_1} {f : ι → ENNReal}, (∀ (i : ι), f i ≠ ⊤) → (iSup f).toNNReal = ⨆ i, (f i).toNNReal
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Composition of enriched functors.  -/
CategoryTheory.EnrichedFunctor.comp : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        {D : Type u₂} →
          {E : Type u₃} →
            [inst_2 : CategoryTheory.EnrichedCategory V C] →
              [inst_3 : CategoryTheory.EnrichedCategory V D] →
                [inst_4 : CategoryTheory.EnrichedCategory V E] →
                  CategoryTheory.EnrichedFunctor V C D →
                    CategoryTheory.EnrichedFunctor V D E → CategoryTheory.EnrichedFunctor V C E
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap'_f_of_not_rel_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀),
  (∀ (l : ι), ¬c.Rel k₀ l) →
    ∀ (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
      (Homotopy.nullHomotopicMap' h).f k₀ = CategoryTheory.CategoryStruct.comp (h k₀ k₁ r₁₀) (D.d k₁ k₀)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.int.sizeOf_spec : ∀ (i : ℤ), sizeOf (Aesop.Frontend.Priority.int i) = 1 + sizeOf i
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.le_nhds_lim : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} (hf : Cauchy f), f ≤ nhds f.lim
-- Mathlib.Algebra.Polynomial.CancelLeads
Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm : ∀ {R : Type u_1} [inst : Ring R] {p q : Polynomial R},
  p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff →
    p.natDegree ≤ q.natDegree → 0 < q.natDegree → (p.cancelLeads q).natDegree < q.natDegree
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.idx : Lean.IR.VarId → Lean.IR.Index
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.pow_apply : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → Pow (M i) α] (f : (i : ι) → M i) (a : α) (i : ι),
  (f ^ a) i = f i ^ a
-- Mathlib.RingTheory.Derivation.Basic
Derivation.restrictScalars_apply : ∀ (R : Type u_1) {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : CommSemiring S] [inst_7 : Algebra S A] [inst_8 : Module S M] [inst_9 : LinearMap.CompatibleSMul A M R S]
  (d : Derivation S A M) (x : A), (Derivation.restrictScalars R d) x = d x
-- Mathlib.Algebra.Order.Kleene
add_le_iff : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b c : α}, a + b ≤ c ↔ a ≤ c ∧ b ≤ c
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `p` lifts and `(r : R)` then `r * p` lifts.  -/
Polynomial.base_mul_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S} (r : R),
  p ∈ Polynomial.lifts f → Polynomial.C (f r) * p ∈ Polynomial.lifts f
-- Mathlib.RingTheory.Localization.BaseChange
/-- The map `(f : M →ₗ[R] M')` is a localization of modules iff the map
`(Localization S) × M → N, (s, m) ↦ s • f m` is the tensor product (insomuch as it is the universal
bilinear map).
In particular, there is an isomorphism between `LocalizedModule S M` and `(Localization S) ⊗[R] M`
given by `m/s ↦ (1/s) ⊗ₜ m`.
 -/
isLocalizedModule_iff_isBaseChange : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  {M' : Type u_4} [inst_6 : AddCommMonoid M'] [inst_7 : Module R M'] [inst_8 : Module A M']
  [inst_9 : IsScalarTower R A M'] (f : M →ₗ[R] M'), IsLocalizedModule S f ↔ IsBaseChange A f
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeftEquiv.eq_1 : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂] [inst_2 : Monoid N]
  (e : M₁ ≃* M₂),
  e.monoidHomCongrLeftEquiv =
    { toFun := fun f => f.comp e.symm.toMonoidHom, invFun := fun f => f.comp e.toMonoidHom, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instNontrivialStalkPresheafSmoothSheaf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] [Nontrivial N] (x : M),
  Nontrivial ((smoothSheaf IM I M N).presheaf.stalk x)
-- Mathlib.CategoryTheory.Action.Continuous
/-- Continuous version of `Functor.mapAction`.  -/
CategoryTheory.Functor.mapContAction : {V : Type u_5} →
  {W : Type u_6} →
    [inst : CategoryTheory.Category.{v_2, u_5} V] →
      {FV : V → V → Type u_7} →
        {CV : V → Type u_8} →
          [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory V FV] →
              [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
                [inst_4 : CategoryTheory.Category.{v_3, u_6} W] →
                  {FW : W → W → Type u_9} →
                    {CW : W → Type u_10} →
                      [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] →
                        [inst_6 : CategoryTheory.ConcreteCategory W FW] →
                          [inst_7 : CategoryTheory.HasForget₂ W TopCat] →
                            (G : Type u_11) →
                              [inst_8 : Monoid G] →
                                [inst_9 : TopologicalSpace G] →
                                  (F : CategoryTheory.Functor V W) →
                                    (∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) →
                                      CategoryTheory.Functor (ContAction V G) (ContAction W G)
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The proposition that the function preserves 0  -/
NonUnitalRingHom.map_zero' : ∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (self : α →ₙ+* β), self.toFun 0 = 0
-- Mathlib.Data.NNReal.Defs
NNReal.bddBelow_coe : ∀ (s : Set NNReal), BddBelow (NNReal.toReal '' s)
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The second projection from the pullback of `f` and `g` to `B`.  -/
AlgHom.pullbackSnd : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] →
                    [inst_6 : Algebra R C] → (f : A →ₐ[R] C) → (g : B →ₐ[R] C) → ↥(f.pullback g) →ₐ[R] B
-- Mathlib.CategoryTheory.Localization.Adjunction
/-- Auxiliary definition of the counit morphism for the adjunction `Adjunction.localization`  -/
CategoryTheory.Adjunction.Localization.η : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        (L₂ : CategoryTheory.Functor C₂ D₂) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            [L₂.IsLocalization W₂] →
                              (G' : CategoryTheory.Functor D₁ D₂) →
                                (F' : CategoryTheory.Functor D₂ D₁) →
                                  [CategoryTheory.CatCommSq G L₁ L₂ G'] →
                                    [CategoryTheory.CatCommSq F L₂ L₁ F'] → F'.comp G' ⟶ CategoryTheory.Functor.id D₂
-- Mathlib.Control.Traversable.Basic
/-- Defines a `traverse` function on the second component of a sum type.
This is used to give a `Traversable` instance for the functor `σ ⊕ -`.  -/
Sum.traverse : {σ : Type u} → {F : Type u → Type u} → [Applicative F] → {α : Type u_1} → {β : Type u} → (α → F β) → σ ⊕ α → F (σ ⊕ β)
-- Mathlib.Algebra.WithConv
/-- The additive equivalence between `WithConv A` and `A`.  -/
WithConv.addEquiv : (A : Type u_2) → [inst : AddMonoid A] → WithConv A ≃+ A
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.add_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [inst : Distrib α],
  (B + C).hadamard A = B.hadamard A + C.hadamard A
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instMulSemiringActionQuotientOfIsScalarTower : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid α] →
      [inst_1 : Semiring R] →
        [inst_2 : MulSemiringAction α R] → [IsScalarTower α R R] → (c : RingCon R) → MulSemiringAction α c.Quotient
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between `(lift F _ _).obj WithInitial.star` with `Z`.  -/
CategoryTheory.WithInitial.liftStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → Z ⟶ F.obj x) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) →
                (CategoryTheory.WithInitial.lift F M hM).obj CategoryTheory.WithInitial.star ≅ Z
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.zero_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Zero α] (i : m) (j : n), 0 i j = 0
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.eq_3 : ∀ (motive : Lean.Expr → List Lean.Expr → Sort u_1) (n : Lean.Name) (t v b : Lean.Expr) (nondep : Bool)
  (args : List Lean.Expr) (h_1 : (f : Lean.Expr) → motive f [])
  (h_2 :
    (binderName : Lean.Name) →
      (binderType b : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          (a : Lean.Expr) → (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as))
  (h_3 :
    (n : Lean.Name) →
      (t v b : Lean.Expr) → (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args)
  (h_4 : (data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args)
  (h_5 : (f : Lean.Expr) → (args : List Lean.Expr) → motive f args),
  (args = [] → False) →
    (match Lean.Expr.letE n t v b nondep, args with
      | f, [] => h_1 f
      | Lean.Expr.lam binderName binderType b binderInfo, a :: as => h_2 binderName binderType b binderInfo a as
      | Lean.Expr.letE n t v b nondep, args => h_3 n t v b nondep args
      | Lean.Expr.mdata data b, args => h_4 data b args
      | f, args => h_5 f args) =
      h_3 n t v b nondep args
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.toContinuousAffineMap_inj : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {f g : P →ᵃⁱ[𝕜] P₂},
  f.toContinuousAffineMap = g.toContinuousAffineMap ↔ f = g
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The left morphism in the pushout square in the definition of `pushoutObj f πX`.  -/
CategoryTheory.SmallObject.functorObjLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶
                  ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : SizeOf C] (i : X ⟶ Y) (r : Y ⟶ X)
  (retract :
    autoParam (CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.Retract.retract._autoParam),
  sizeOf { i := i, r := r, retract := retract } = 1 + sizeOf i + sizeOf r + sizeOf retract
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.supp_eq : ∀ {P : PFunctor.{uA, uB}} {α : Type u} (a : P.A) (f : P.B a → α), Functor.supp ⟨a, f⟩ = f '' Set.univ
-- Mathlib.Condensed.Discrete.Colimit
Condensed.finYoneda_obj : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) (X : FintypeCatᵒᵖ),
  (Condensed.finYoneda F).obj X =
    ((Opposite.unop X).obj → F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.nodup_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp], t.keys.Nodup
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `ProbabilityTheory.Kernel.finsetSum_apply'`. -/
ProbabilityTheory.Kernel.finset_sum_apply' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (I : Finset ι)
  (κ : ι → ProbabilityTheory.Kernel α β) (a : α) (s : Set β), ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s
-- Init.Data.AC
Lean.Data.AC.Expr.brecOn.go : {motive : Lean.Data.AC.Expr → Sort u} →
  (t : Lean.Data.AC.Expr) →
    ((t : Lean.Data.AC.Expr) → Lean.Data.AC.Expr.below t → motive t) → motive t ×' Lean.Data.AC.Expr.below t
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_comp_le_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.degHom f
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_eq : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C} (G : CategoryTheory.Functor D₁ D₂)
  (e : L₁.comp G ≅ L₂) (f : L₁.obj X ⟶ L₁.obj Y),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) f =
    CategoryTheory.CategoryStruct.comp (e.inv.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.hom.app Y))
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.RingObjCat C),
  (CategoryTheory.RingObjCat.forget C).obj R = R.X
-- Mathlib.Data.Int.Cast.Basic
Int.cast_ofNat : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.edist_le_eccent : ∀ {α : Type u_1} {G : SimpleGraph α} {u v : α}, G.edist u v ≤ G.eccent u
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toList_eq_if_rco : ∀ {α : Type u} {r : Std.Rco α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α],
  r.toList =
    if r.lower < r.upper then
      match Std.PRange.succ? r.lower with
      | none => [r.lower]
      | some next => r.lower :: (next...r.upper).toList
    else []
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.instInhabitedOfNonempty : (α : Type u_5) → (ι : Type u_6) → [Nonempty ι] → Inhabited (Combinatorics.Line α ι)
-- Mathlib.Order.Hom.Basic
OrderHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.unique : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} [p.NeBot] [T2Space β] {g : α → β},
  TendstoLocallyUniformlyOn F f p s → TendstoLocallyUniformlyOn F g p s → Set.EqOn f g s
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.comp_id : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂), f.comp (LinearMap.BilinForm.Isometry.id B₁) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism between `(Cofork.ofπ π w).op` and `Fork.ofι π.op w'`.  -/
CategoryTheory.Limits.Cofork.ofπOpIsoOfι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : C} →
      {f g : X ⟶ Y} →
        (π π' : Y ⟶ P) →
          (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) →
            (w' : CategoryTheory.CategoryStruct.comp π'.op f.op = CategoryTheory.CategoryStruct.comp π'.op g.op) →
              π = π' → ((CategoryTheory.Limits.Cofork.ofπ π w).op ≅ CategoryTheory.Limits.Fork.ofι π'.op w')
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeInterpStrQuotedChar : String → String.Pos.Raw → Option (Char × String.Pos.Raw)
-- Mathlib.Algebra.BigOperators.Finprod
/-- For finite sets, multiplication commutes with `finsum_mem`. See `mul_finsum_mem'` for a statement
assuming finiteness of support.
 -/
mul_finsum_mem' : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R),
  s.Finite → r * ∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α) (_ : a ∈ s), r * f a
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ 1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.parallelPairIsoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (p p_1 : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (e_p : p = p_1)
  (q q_1 : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (e_q : q = q_1)
  (hl :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q.hom =
      CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
  (hr :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q.hom =
      CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right)),
  CategoryTheory.Limits.parallelPairIsoMk p q hl hr = CategoryTheory.Limits.parallelPairIsoMk p_1 q_1 ⋯ ⋯
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsLeftCancelSMulSubtypeMem : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  [IsLeftCancelSMul R M], IsLeftCancelSMul R ↥s
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn_eq_iSup : ∀ (n : ℕ) (i : Fin (n + 1)), SSet.horn n i = ⨆ j, SSet.stdSimplex.face {↑j}ᶜ
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.recordLazySteps : Aesop.DisplayRuleName → Option (Array Aesop.Script.LazyStep) → Aesop.ExtractScriptM Unit
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.instZero : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → Zero (HahnSeries Γ R)
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- The main result, *Legendre's Theorem* on rational approximation:
if `ξ` is a real number and `q` is a rational number such that `|ξ - q| < 1/(2*q.den^2)`,
then `q` is a convergent of the continued fraction expansion of `ξ`.
This version uses `Real.convergent`.  -/
Real.exists_rat_eq_convergent : ∀ {ξ : ℝ} {q : ℚ}, |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2) → ∃ n, q = ξ.convergent n
-- Mathlib.Data.Set.Image
Set.forall_subset_range_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : Set β → Prop}, (∀ s ⊆ Set.range f, p s) ↔ ∀ (s : Set α), p (f '' s)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Ico i j) = Finset.Ioc j.rev i.rev
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.lsmul_flip_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (LinearMap.lsmul R M).flip m = LinearMap.toSpanSingleton R M m
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_mono : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F]
  {f g : MeasureTheory.SimpleFunc α F},
  ⇑f ≤ᵐ[μ] ⇑g →
    MeasureTheory.Integrable (⇑f) μ →
      MeasureTheory.Integrable (⇑g) μ → MeasureTheory.SimpleFunc.integral μ f ≤ MeasureTheory.SimpleFunc.integral μ g
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.leftOp_id : ∀ {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.NatTrans.leftOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftOp
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.hom_ext_iff : ∀ {n : ℕ} {X Y : SSet.Truncated n} {f g : X ⟶ Y},
  f = g ↔ ∀ (n_1 : (SimplexCategory.Truncated n)ᵒᵖ), f.app n_1 = g.app n_1