mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Binomial
Polynomial.descPochhammer_smeval_eq_ascPochhammer : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (r : R) (n : ℕ),
  (descPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.irrational_rpow_rat_of_not_power : ∀ {q : ℚ} {a b : ℕ}, (∀ (p : ℚ), q ^ a ≠ p ^ b) → 0 < b → 0 ≤ q → Irrational ((↑q).rpow ↑(↑a / ↑b))
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coe_liftNCAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B) (g : M →* B)
  (h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)),
  ⇑(MonoidAlgebra.liftNCAlgHom f g h_comm) = ⇑(MonoidAlgebra.liftNC ↑f ⇑g)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `firstToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₁` to `max₃ j₁ j₂ j₃`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.firstToMax₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j₁ j₂ j₃ : C) → j₁ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁Map_toFun : ∀ {R : Type u_1} {V : Type u_3} {W : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] [inst_5 : AddCommGroup W] [inst_6 : TopologicalSpace W]
  [inst_7 : IsTopologicalAddGroup W] [inst_8 : Module R W] {G : Type u_7} [inst_9 : Group G]
  [inst_10 : TopologicalSpace G] [inst_11 : TopologicalSpace R] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] [inst_14 : IsTopologicalGroup G] {π₁ : ContRepresentation R G V}
  {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) (g : C(G, V)),
  (ContRepresentation.coind₁Map f) g = (↑f).comp g
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.param : {α : Type u} → Lean.JsonRpc.Notification α → α
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_range : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M}, Function.Surjective v → (Finsupp.linearCombination R v).range = ⊤
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_sum : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  (f : ι → ↥(lp E p)) (s : Finset ι), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ_σ₀Iter' : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (m + j = n) SimplexCategory.δ_σ₀Iter'._auto_1),
  autoParam (j < ↑i) SimplexCategory.δ_σ₀Iter'._auto_3 →
    autoParam (↑i = ↑i' + j) SimplexCategory.δ_σ₀Iter'._auto_5 →
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.σ₀Iter j ⋯) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter j ⋯) (SimplexCategory.δ i')
-- Mathlib.RepresentationTheory.Basic
Representation.free_asModule_free : ∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Monoid G] (α : Type u_6),
  Module.Free (MonoidAlgebra k G) (Representation.free k G α).asModule
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vadd_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x : P), nndist x (v +ᵥ x) = ‖v‖₊
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.eq_lim_of_const_equiv : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] {f : CauSeq β abv}
  {x : β}, CauSeq.const abv x ≈ f → x = f.lim
-- Mathlib.Data.Set.Lattice
/-- A reversed version of `iInter_psigma` with a curried map.  -/
Set.iInter_psigma' : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β), ⋂ i, ⋂ a, s i a = ⋂ ia, s ia.fst ia.snd
-- Init.Data.Array.Find
Array.findIdx?_append : ∀ {α : Type u_1} {xs ys : Array α} {p : α → Bool},
  Array.findIdx? p (xs ++ ys) = (Array.findIdx? p xs).or (Option.map (fun i => i + xs.size) (Array.findIdx? p ys))
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize' : String → ℕ
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.IsKProjective.leftOrthogonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) [K.IsKProjective],
  (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.coeFn_sup : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f g : MeasureTheory.Filtration ι m},
  ↑(f ⊔ g) = ↑f ⊔ ↑g
-- Mathlib.Topology.Algebra.UniformMulAction
IsUniformGroup.instUniformContinuousConstSMul : ∀ {G : Type u} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G], UniformContinuousConstSMul G G
-- Init.Data.UInt.Lemmas
UInt16.ofNat_uSizeToNat : ∀ (n : USize), UInt16.ofNat n.toNat = n.toUInt16
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.boundedSpace_iff_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α], BoundedSpace α ↔ ∃ C, ∀ (a b : α), edist a b ≤ ↑C
-- Mathlib.FieldTheory.Separable
Polynomial.separable_C : ∀ {R : Type u} [inst : CommSemiring R] (r : R), (Polynomial.C r).Separable ↔ IsUnit r
-- Init.Omega.IntList
Lean.Omega.IntList.get_cons_zero : ∀ {x : ℤ} {xs : List ℤ}, Lean.Omega.IntList.get (x :: xs) 0 = x
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.whiskerLeft_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a' ⟶ F.obj a) (g : a ⟶ b) {Z : a' ⟶ G.obj b}
  (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (F.map g) (θ.app b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map g)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app b))) h)
-- Mathlib.Topology.Algebra.Order.Field
tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : 𝕜 → α},
  Filter.Tendsto (fun x => f x⁻¹) Filter.atBot l → Filter.Tendsto f (nhdsWithin 0 (Set.Iio 0)) l
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldRedeclInfo.mk.sizeOf_spec : ∀ (stx : Lean.Syntax), sizeOf { stx := stx } = 1 + sizeOf stx
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k : α} {f : β k → β k} {hc : (m.modify k f).contains k = true},
  (m.modify k f).get k hc = f (m.get k ⋯)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mapHom_id : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Submodule.mapHom (AlgHom.id R A) = RingHom.id (Submodule R A)
-- Mathlib.Topology.Algebra.Order.UpperLower
HasUpperLowerClosure.isUpperSet_closure : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : HasUpperLowerClosure α] (s : Set α),
  IsUpperSet s → IsUpperSet (closure s)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on an additive quantale are similar
to the Heyting operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ᵣ z ↔ y + x ≤ z` or alternatively `x ⇨ₗ y = sSup { z | x + z ≤ y }`."  -/
AddQuantale.«term_⇨ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : C(X, ℝ)) (x : X), f.toNNReal x = (f x).toNNReal
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.pointWeightsWithCircumcenter.eq_1 : ∀ {n : ℕ} (i a : Fin (n + 1)),
  Affine.Simplex.pointWeightsWithCircumcenter i (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a) =
    if a = i then 1 else 0
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) h
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.hom_inv_s₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀), e.inv.s₀ (e.hom.s₀ i) = i
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, t.WF → k ∈ Std.TreeMap.Raw.filterMap f t → k ∈ t
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instPreadditive : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → CategoryTheory.Preadditive (Rep.{w, u, v} k G)
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- Lift a function to `WithLp`.  -/
WithLp.map : (p : ENNReal) → {V : Type u_4} → {V' : Type u_5} → (V → V') → WithLp p V → WithLp p V'
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.mk : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.LocalizationAwayPreserves P →
    RingHom.OfLocalizationSpanTarget P →
      RingHom.OfLocalizationSpan P →
        RingHom.StableUnderCompositionWithLocalizationAwayTarget P → RingHom.PropertyIsLocal P
-- Batteries.Data.BitVec.Lemmas
/-- **Alias** of `BitVec.getLsb_ofFnLE`. -/
BitVec.getLsb'_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnLE f).getLsb i = f i
-- Mathlib.Data.Sym.Basic
Sym.hasCoe : (α : Type u_1) → (n : ℕ) → CoeOut (Sym α n) (Multiset α)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_div_eq_mk_left : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a < MulArchimedeanClass.mk b → MulArchimedeanClass.mk (a / b) = MulArchimedeanClass.mk a
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictDerivAt_exp_smul_const' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸) (t : 𝕂), HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.instCoeFunForallElemRealIcc : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} →
        {x₀ : E} → {r L : NNReal} → CoeFun (ODE.FunSpace t₀ x₀ r L) fun x => ↑(Set.Icc tmin tmax) → E
-- Aesop.Script.Tactic
Aesop.Script.Tactic.instToMessageData : Lean.ToMessageData Aesop.Script.Tactic
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.getElem?_toList_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {r : Std.Rcc α} {i : ℕ},
  r.toList[i]? = Option.filter (fun x => decide (x ≤ r.upper)) (Std.PRange.succMany? i r.lower)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {ι : Sort u_3} {s : ι → Set E}, (∀ (i : ι), AbsConvex 𝕜 (s i)) → AbsConvex 𝕜 (⋂ i, s i)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsMonHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] {f : M ⟶ N},
  autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
      CategoryTheory.IsMonHom.one_hom._autoParam →
    autoParam
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
            CategoryTheory.MonObj.mul)
        CategoryTheory.IsMonHom.mul_hom._autoParam →
      CategoryTheory.IsMonHom f
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op V ⟶ Opposite.op V'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) (X.presheaf.map i) =
    AlgebraicGeometry.Scheme.Hom.appLE f U V' ⋯
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.args.sizeOf_spec : ∀ (a : Array ℕ), sizeOf (Lean.Elab.WF.GuessLex.MutualMeasure.args a) = 1 + sizeOf a
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Multiplicative congruence relations preserve product indexed by a multiset.  -/
Con.multiset_prod : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (c : Con M) {s : Multiset ι} {f g : ι → M},
  (∀ x ∈ s, c (f x) (g x)) → c (Multiset.map f s).prod (Multiset.map g s).prod
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- If `ι` is a linearly ordered type, `I : MultispanIndex (.prod ι) C`, and
`c` a colimit multicofork for `I`, then `c.toLinearOrder` is a colimit
multicofork for `I.toLinearOrder`.  -/
CategoryTheory.Limits.Multicofork.isColimitToLinearOrder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      [inst_1 : LinearOrder ι] →
        {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
          (c : CategoryTheory.Limits.Multicofork I) →
            CategoryTheory.Limits.IsColimit c → I.SymmStruct → CategoryTheory.Limits.IsColimit c.toLinearOrder
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_sub_cosh : ∀ (x : ℝ), Real.sinh x - Real.cosh x = -Real.exp (-x)
-- Init.Prelude
/-- `a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`. -/
GE.ge : {α : Type u} → [LE α] → α → α → Prop
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.add_eq_one : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] (s : ↑(stdSimplex S (Fin 2))), s 0 + s 1 = 1
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedSymbolPriorities.default : Lean.Meta.Grind.SymbolPriorities
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V V₁ : (x : M') → TangentSpace I' x},
  VectorField.mpullback I I' f (V + V₁) = VectorField.mpullback I I' f V + VectorField.mpullback I I' f V₁
-- Init.Data.List.Sort.Lemmas
List.zipIdxLE_total : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b : α), (le a b || le b a) = true) → ∀ (a b : α × ℕ), (List.zipIdxLE le a b || List.zipIdxLE le b a) = true
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.F₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.Functor (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂) C
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `R` satisfies the rank condition,
then the cardinality of any basis is bounded by the cardinality of any spanning set.
 -/
Module.Basis.le_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [RankCondition R] {J : Set M} (v : Module.Basis ι R M),
  Submodule.span R J = ⊤ → Cardinal.mk ↑(Set.range ⇑v) ≤ Cardinal.mk ↑J
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The natural isomorphism between the `n`-th index of the Tate complex and inhomogeneous
`n`-chains for `n < 0`.  -/
TateCohomology.tateComplex.evalNeg : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        (n : ℕ) →
          (tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc n)) ≅
            (groupHomology.chainsFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) n)
-- Mathlib.Algebra.Ring.Subring.Defs
NonUnitalSubring.toSubring_toNonUnitalSubring : ∀ {R : Type u} [inst : NonAssocRing R] (S : NonUnitalSubring R) (h1 : 1 ∈ S), (S.toSubring h1).toNonUnitalSubring = S
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A} {x : NNReal}, CFC.sqrt (a ^ x) = a ^ (x / 2)
-- Init.Control.Lawful.Instances
OptionT.run_seqRight : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β),
  (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run)
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  hS.singleTriangle.obj₃ = (DerivedCategory.singleFunctor C 0).obj S.X₃
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Int.castDef.eq_2 : ∀ {R : Type u} [inst : NatCast R] [inst_1 : Neg R] (n : ℕ), (Int.negSucc n).castDef = -↑(n + 1)
-- Init.Core
/-- `LawfulCommIdentity` can simplify defining instances of `LawfulIdentity`
on commutative functions by requiring only a left or right identity
proof.

This class is intended for simplifying defining instances of
`LawfulIdentity` and functions needed commutative operations with
identity should just add a `LawfulIdentity` constraint.
 -/
Std.LawfulCommIdentity : {α : Sort u} → (op : α → α → α) → outParam α → [hc : Std.Commutative op] → Prop
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindToInd_indToCoind : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [inst_3 : S.FiniteIndex],
  A.indToCoind ∘ₗ A.coindToInd = LinearMap.id
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- The identity of any object is a transfinite composition of shape `Fin 1`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (X : C) → W.TransfiniteCompositionOfShape (Fin 1) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.instAtPrimeCarrierStalkCommRingCatStructurePresheafInCommRingCatAsIdeal : ∀ {R : Type u} [inst : CommRing R] (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  IsLocalization.AtPrime (↑((AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x)) x.asIdeal
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1_cert.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_step1_cert p₁ k₂ m₂ p₂ p =
    p.beq' (p₁.combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂))
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxcLawfulHasSize : ∀ {n : ℕ}, Std.Rxc.LawfulHasSize (BitVec n)
-- Batteries.Data.Array.Scan
Array.scanrM.loop_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : Array α} {stop : ℕ} {acc : Array β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m β} {start : ℕ} {h : start ≤ as.size},
  Array.toList <$> Array.scanrM.loop f init as start stop h acc = do
    let __do_lift ← List.scanrM f init (List.take (start - stop) (List.drop stop as.toList))
    pure (__do_lift ++ acc.toList.reverse)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Interpret a `Homeomorph` as an `OpenPartialHomeomorph` by restricting it
to an open set `s` in the domain and to `t` in the codomain.  -/
Homeomorph.toOpenPartialHomeomorphOfImageEq : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : X ≃ₜ Y) → (s : Set X) → IsOpen s → (t : Set Y) → ⇑e '' s = t → OpenPartialHomeomorph X Y
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.instIsAlgebraicConstantsOn : ∀ (α : Type u_1), (FirstOrder.Language.constantsOn α).IsAlgebraic
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_pos : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b : α}, 0 < a - b ↔ b < a ∨ b = ⊤
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ioc_mul_eq_prod_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → (∏ x ∈ Finset.Ioc a b, f x) * f a = ∏ x ∈ Finset.Icc a b, f x
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'}, ContMDiff J (I.prod I') n f → ContMDiff J I n fun x => (f x).1