mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : Set α` and
`t : Set β`.  -/
generateFrom_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  MeasurableSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}) =
    Prod.instMeasurableSpace
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r : l → m) (c : o → n)
  (i : l) (j : o), A.submatrix r c i j = A (r i) (c j)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.SavedLocalContext.mk : Lean.LocalContext → Lean.LocalInstances → Lean.Meta.SavedState → Lean.Elab.WF.GuessLex.SavedLocalContext
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
reduceCtorEq : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length  -/
FreeMonoid.length : {α : Type u_1} → FreeMonoid α → ℕ
-- Init.Data.Int.DivMod.Lemmas
Int.neg_tdiv_of_dvd : ∀ {a b : ℤ}, b ∣ a → (-a).tdiv b = -a.tdiv b
-- Lean.Level
Lean.Level.mvarId! : Lean.Level → Lean.LMVarId
-- Init.Data.BitVec.Lemmas
BitVec.toFin_shiftLeftZeroExtend : ∀ {w n : ℕ} {x : BitVec w}, (x.shiftLeftZeroExtend n).toFin = Fin.ofNat (2 ^ (w + n)) (x.toNat * 2 ^ n)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.IsSolvable.mk_int : ∀ {L : Type v} [inst : LieRing L], (∃ k, LieAlgebra.derivedSeries ℤ L k = ⊥) → LieAlgebra.IsSolvable L
-- Mathlib.Order.BourbakiWitt
/-- The underlying set of a nonempty chain  -/
NonemptyChain.carrier : {α : Type u_4} → [inst : LE α] → NonemptyChain α → Set α
-- Mathlib.Order.Hom.Basic
Subtype.orderEmbedding_apply_coe : ∀ {α : Type u_2} [inst : Preorder α] {p q : α → Prop} (h : ∀ (a : α), p a → q a) (x : { x // p x }),
  ↑((Subtype.orderEmbedding h) x) = ↑x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Given left homology data `h₁` and `h₂` for two short complexes `S₁` and `S₂`,
a `LeftHomologyMapData` for a morphism `φ : S₁ ⟶ S₂`
consists of a description of the induced morphisms on the `K` (cycles)
and `H` (left homology) fields of `h₁` and `h₂`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → S₁.LeftHomologyData → S₂.LeftHomologyData → Type v_1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- A version of `WithTop.coe_sInf'` with a more convenient but less general statement.  -/
WithTop.coe_sInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α},
  s.Nonempty → BddBelow s → ↑(sInf s) = ⨅ a ∈ s, ↑a
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- The natural isomorphism `LF' ≅ LF` on left derived functors that is
induced by a natural isomorphism `F' ≅ F`.  -/
CategoryTheory.Functor.leftDerivedNatIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (LF' LF : CategoryTheory.Functor D H) →
              {F F' : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α' : L.comp LF' ⟶ F') →
                    (α : L.comp LF ⟶ F) →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] →
                          [LF.IsLeftDerivedFunctor α W] → [LF'.IsLeftDerivedFunctor α' W] → (F' ≅ F) → (LF' ≅ LF)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_mul' : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R), IsUnit A.det → ∀ (m n : ℤ), A ^ (m * n) = (A ^ n) ^ m
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} [inst_2 : SizeOf C] [inst_3 : (a : C) → SizeOf (P a)]
  [inst_4 : SizeOf J] (toColimitPresentation : CategoryTheory.Limits.ColimitPresentation J X)
  (prop_diag_obj : ∀ (j : J), P (toColimitPresentation.diag.obj j)),
  sizeOf { toColimitPresentation := toColimitPresentation, prop_diag_obj := prop_diag_obj } =
    1 + sizeOf toColimitPresentation
-- Mathlib.Geometry.Manifold.Submersion
/-- Being a submersion w.r.t. `F` is stable under replacing `F` by an isomorphic copy.  -/
Manifold.IsSubmersionOfComplement.congr_F : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] [inst_9 : TopologicalSpace H]
  [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11}
  {N : Type u_13} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] [inst_13 : TopologicalSpace N]
  [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} (e : F ≃L[𝕜] F'),
  Manifold.IsSubmersionOfComplement F I J n f ↔ Manifold.IsSubmersionOfComplement F' I J n f
-- Mathlib.Data.Set.Pairwise.Basic
Set.exists_ne_mem_inter_of_not_pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ι → Set α},
  ¬s.PairwiseDisjoint f → ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Any three points in an orthocentric system are affinely independent.  -/
EuclideanGeometry.OrthocentricSystem.affineIndependent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.OrthocentricSystem s →
    ∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → AffineIndependent ℝ p
-- Init.Data.Nat.Lemmas
Nat.one_lt_two_pow_iff : ∀ {n : ℕ}, 1 < 2 ^ n ↔ n ≠ 0
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimage_image_factorisation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_5 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f)
        (CategoryTheory.Abelian.image.ι f)) =
    f
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams.mk.inj : ∀ {hash : UInt64} {pos : Lean.Lsp.Position} {hash_1 : UInt64} {pos_1 : Lean.Lsp.Position},
  { hash := hash, pos := pos } = { hash := hash_1, pos := pos_1 } → hash = hash_1 ∧ pos = pos_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The inverse of the associator as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.associatorInvM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightId.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  CategoryTheory.Comma.mapRightId L R =
    CategoryTheory.NatIso.ofComponents'
      (fun X =>
        CategoryTheory.Comma.isoMk._to_dual_1
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapRight R (CategoryTheory.CategoryStruct.id L)).obj X).right)
          (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapRight R (CategoryTheory.CategoryStruct.id L)).obj X).left)
          ⋯)
      ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- The convolution of `f` and `g` with bilinear map `L` exists when it exists at every point.  -/
DiscreteConvolution.ConvolutionExists : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [Monoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] → [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → Prop
-- Mathlib.CategoryTheory.Limits.Over
/-- Given an arrow `c.pt ⟶ X`, the diagram `J ⥤ C` can be lifted to `Over X ⥤ C`, and
the cocone `c` also lifts to the diagram on `Over`.  -/
CategoryTheory.Over.liftCocone : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            {X : C} →
              (f : c.pt ⟶ X) →
                CategoryTheory.Limits.Cocone
                  (CategoryTheory.Over.lift F
                    (CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f)))
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a short complex `S` is such that `S.g = 0` and that the cokernel of `S.f` is preserved
by a functor `F`, then `F` preserves the left homology of `S`.  -/
CategoryTheory.Functor.preservesLeftHomology_of_zero_g : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C),
  S.g = 0 →
    ∀ [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F], F.PreservesLeftHomologyOf S
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipSuffix?_string_empty : ∀ {s : String.Slice}, s.skipSuffix? "" = some s.endPos
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mem_filter_of_mem : ∀ {α : Type u_1} (B : FilterBasis α) {U : Set α}, U ∈ B → U ∈ B.filter
-- Init.Data.UInt.Lemmas
UInt8.toNat_div : ∀ (a b : UInt8), (a / b).toNat = a.toNat / b.toNat
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Rewrite `PowerSeries.substAlgHom` as `PowerSeries.aeval`.

Its use is discouraged because it introduces a topology and might lead
into awkward comparisons.  -/
PowerSeries.substAlgHom_eq_aeval : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} [inst_3 : UniformSpace R] [inst_4 : DiscreteUniformity R] [inst_5 : UniformSpace S]
  [inst_6 : DiscreteUniformity S] (ha : PowerSeries.HasSubst a), PowerSeries.substAlgHom ha = PowerSeries.aeval ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_3 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (expr_2 : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr_2.not cache =
    match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig expr_2 cache with
    | { result := ⟨{ aig := aig_1, ref := exprRef }, hexpr⟩, cache := cache } =>
      let ret := aig_1.mkNotCached exprRef;
      have this := ⋯;
      have cache := cache.cast this;
      have this := ⋯;
      { result := ⟨ret, this⟩, cache := cache }
-- Mathlib.Topology.Path
Path.extend_symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) (t : ℝ), γ.symm.extend t = γ.extend (1 - t)
-- Mathlib.Tactic.NormNum.NatFactorial
/-- Evaluates the `Nat.descFactorial` function.  -/
Mathlib.Meta.NormNum.evalNatDescFactorial : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₄_eq_some_middle : ∀ {w x y z : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte y = false
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.ofScalar.sizeOf_spec : ∀ {R : Type u_1} {X : Type u_2} [inst : SizeOf R] [inst_1 : SizeOf X] (a : R),
  sizeOf (FreeAlgebra.Pre.ofScalar a) = 1 + sizeOf a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_mul_lt_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] {a b c d : α}, a * b < c → d ≤ b → a * d < c
-- Init.Data.SInt.Lemmas
Int16.toInt_toISize : ∀ (x : Int16), x.toISize.toInt = x.toInt
-- Mathlib.Algebra.Category.FGModuleCat.Abelian
FGModuleCat.instIsIsoCoimageImageComparison : ∀ {k : Type u} [inst : Ring k] [inst_1 : IsNoetherianRing k] {X Y : FGModuleCat k} (f : X ⟶ Y),
  CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
-- Mathlib.Topology.Constructions.SumProd
Filter.Tendsto.snd_nhds : ∀ {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {X : Type u_5} {l : Filter X}
  {f : X → Y × Z} {p : Y × Z}, Filter.Tendsto f l (nhds p) → Filter.Tendsto (fun a => (f a).2) l (nhds p.2)
-- Mathlib.Data.Fin.SuccPred
Fin.castLT_eq_castPred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i < Fin.last n) (h' : optParam (¬i = Fin.last n) ⋯), i.castLT h = i.castPred h'
-- Lean.Data.KVMap
Lean.KVMap.findCore : List (Lean.Name × Lean.DataValue) → Lean.Name → Option Lean.DataValue
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk.inj : ∀ {R : Type u} {a b re im re_1 im_1 : R}, { re := re, im := im } = { re := re_1, im := im_1 } → re = re_1 ∧ im = im_1
-- Mathlib.Data.Matrix.Mul
Matrix.ext_of_single_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  {M N : Matrix m n α}, (∀ (i : m), Matrix.vecMul (Pi.single i 1) M = Matrix.vecMul (Pi.single i 1) N) → M = N
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.comapMk'OrderIso.eq_1 : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [hn : N.Normal],
  QuotientGroup.comapMk'OrderIso N =
    { toFun := fun H' => ⟨Subgroup.comap (QuotientGroup.mk' N) H', ⋯⟩,
      invFun := fun H => Subgroup.map (QuotientGroup.mk' N) ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Algebra.Unitization
/-- The canonical inclusion `A → Unitization R A`.  -/
Unitization.inr : {R : Type u_1} → {A : Type u_2} → [Zero R] → A → Unitization R A
-- Init.Data.Nat.Lemmas
Nat.mod_add_div' : ∀ (a b : ℕ), a % b + a / b * b = a
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- `Ext` commutes with biproducts in its first variable.  -/
CategoryTheory.Abelian.Ext.biproductAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {J : Type u_1} →
          [Fintype J] →
            {X : J → C} →
              {c : CategoryTheory.Limits.Bicone X} →
                c.IsBilimit →
                  (Y : C) →
                    (n : ℕ) → CategoryTheory.Abelian.Ext c.pt Y n ≃+ ((i : J) → CategoryTheory.Abelian.Ext (X i) Y n)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceBEq : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) {Z : C}
  (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (n + 1)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.Ord.Basic
Ordering.isLE_lt : Ordering.lt.isLE = true
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ}
  {μ ν : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f ν a b → Set.uIcc c d ⊆ Set.uIcc a b → μ ≤ ν → IntervalIntegrable f μ c d
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instReprOfTransCmp : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Repr α] → [Repr β] → Repr (Std.ExtTreeMap α β cmp)
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort_zipIdx.go : ∀ {α : Type u_1} {le : α → α → Bool} (i : ℕ) (l : List α),
  List.map (fun x => x.1) ((l.zipIdx i).mergeSort (List.zipIdxLE le)) = l.mergeSort le
-- Mathlib.Algebra.Order.Archimedean.Defs
/-- An ordered additive commutative monoid is called `Archimedean` if for any two elements `x`, `y`
such that `0 < y`, there exists a natural number `n` such that `x ≤ n • y`.  -/
Archimedean : (R : Type u_2) → [AddCommMonoid R] → [PartialOrder R] → Prop
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.setRef : IO.CancelToken → IO.Ref Bool
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.ignoreFieldType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.snd_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (p₀ p₁ : P1 × P2) (c : k),
  ((AffineMap.lineMap p₀ p₁) c).2 = (AffineMap.lineMap p₀.2 p₁.2) c
-- Lean.Util.Recognizers
Lean.Expr.eq? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Lean.Meta.Closure
Lean.Meta.Closure.pushLocalDecl : Lean.FVarId → Lean.Name → Lean.Expr → optParam Lean.BinderInfo Lean.BinderInfo.default → Lean.Meta.Closure.ClosureM Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isShortNF_iff : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R), W.IsShortNF ↔ W.a₁ = 0 ∧ W.a₂ = 0 ∧ W.a₃ = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a : B} {a' : C} (f : G.obj a ⟶ a') {Z : F.obj a ⟶ a'}
  (h :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (G.obj a)) f) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a).hom f))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom h)))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
ClosedEmbeddingContinuousFunctionalCalculus.toNonUnital : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [ClosedEmbeddingContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] [CompleteSpace R], NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p
-- Init.Core
PSum.inl.inj : ∀ {α : Sort u} {β : Sort v} {val val_1 : α}, PSum.inl val = PSum.inl val_1 → val = val_1
-- Mathlib.Lean.Meta.KAbstractPositions
/-- The main loop that loops through all subexpressions  -/
Lean.Meta.kabstractPositions.visit : Lean.Expr →
  Lean.MetavarContext →
    Lean.HeadIndex → ℕ → Lean.Expr → Lean.SubExpr.Pos → Array Lean.SubExpr.Pos → Lean.MetaM (Array Lean.SubExpr.Pos)
-- Mathlib.NumberTheory.SelbergSieve
SelbergSieve.one_le_level : ∀ (self : SelbergSieve), 1 ≤ self.level
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.coe_op : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup M), ↑x.op = MulOpposite.unop ⁻¹' ↑x
-- Mathlib.Order.DirectedInverseSystem
/-- Extend `pEquivOnGlue` by one step, obtaining a partial family over a right-closed interval.  -/
InverseSystem.pEquivOnLim : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
            [inst_1 : SuccOrder ι] →
              {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
                [WellFoundedLT ι] →
                  Order.IsSuccPrelimit i →
                    ((j : ↑(Set.Iio i)) → InverseSystem.PEquivOn f equivSucc (Set.Iic ↑j)) →
                      [InverseSystem f] →
                        (equivLim : F i ≃ ↑(InverseSystem.limit f i)) →
                          (∀ (x : F i) (l : ↑(Set.Iio i)), ↑(equivLim x) l = f ⋯ x) →
                            InverseSystem.PEquivOn f equivSucc (Set.Iic i)
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.eq_of_mul_eq_mul_of_coprime : ∀ {a b x y : ℕ}, a.Coprime b → x.Coprime y → a * x = b * y → a = y
-- Batteries.Data.List.Lemmas
List.max!_nil : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Max α], [].max! = default
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- Nonnegativity of an element of `ℤ√d`.  -/
Zsqrtd.Nonneg : {d : ℕ} → ℤ√↑d → Prop
-- Init.Data.List.Nat.Modify
List.modify_id : ∀ {α : Type u_1} (i : ℕ) (l : List α), l.modify i id = l
-- Aesop.Tree.Tracing
Aesop.Rapp.traceTree : Aesop.Rapp → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The constant `GenLoop` at `x`.  -/
GenLoop.const : {N : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → ↑(GenLoop N X x)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Inclusion of the groupoid of `C^n` local diffeos in the groupoid of `C^m` local diffeos when
`m ≤ n`  -/
contDiffGroupoid_le : ∀ {m n : WithTop ℕ∞} {𝕜 : 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 ≤ n → contDiffGroupoid n I ≤ contDiffGroupoid m I
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose.eq_3 : ∀ (n k : ℕ), n.succ.choose k.succ = n.choose k + n.choose (k + 1)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.triv.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.Proof.triv = 1
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.hasForgetToFinBddDistLat : CategoryTheory.HasForget₂ FinBoolAlg FinBddDistLat
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsGT_coe_neBot : ∀ {r : NNReal}, (nhdsWithin (↑r) (Set.Ioi ↑r)).NeBot