mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- The ordinal predecessor of `a` is `b` if `a = succ b`, and `a` otherwise.  -/
Ordinal.pred : Ordinal.{u_4} → Ordinal.{u_4}
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.completeMultipartiteGraph.chromaticNumber : ∀ {ι : Type u_4} (V : ι → Type u_5) [inst : Fintype ι] (f : (i : ι) → V i),
  (SimpleGraph.completeMultipartiteGraph V).chromaticNumber = ↑(Fintype.card ι)
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_toUInt64 : ∀ (n : UInt8), n.toUInt64.toUInt16 = n.toUInt16
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv_eq_integral_klFun : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    (InformationTheory.klDiv μ ν).toReal = ∫ (x : α), InformationTheory.klFun (μ.rnDeriv ν x).toReal ∂ν
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_beq_unpack_iff : ∀ {spec : Float.Model.Format} {b b' : BitVec spec.numBits},
  spec.Valid b →
    spec.Valid b' →
      autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.unpack_beq_unpack_iff._auto_1 →
        ((Float.Model.UnpackedFloat.unpack spec b).beq (Float.Model.UnpackedFloat.unpack spec b') = true ↔
          b ≠ Float.Model.UnpackedFloat.packedNaN spec ∧
            b' ≠ Float.Model.UnpackedFloat.packedNaN spec ∧
              (b = b' ∨
                b = Float.Model.UnpackedFloat.packedZero spec Float.Model.UnpackedFloat.Sign.positive ∧
                    b' = Float.Model.UnpackedFloat.packedZero spec Float.Model.UnpackedFloat.Sign.negative ∨
                  b = Float.Model.UnpackedFloat.packedZero spec Float.Model.UnpackedFloat.Sign.negative ∧
                    b' = Float.Model.UnpackedFloat.packedZero spec Float.Model.UnpackedFloat.Sign.positive))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given that the left square is a pushout, the pasted square is a pushout iff the right square is.
 -/
CategoryTheory.Limits.pasteHorizIsPushoutEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₁ ⟶ X₂} →
        {f₂ : X₂ ⟶ X₃} →
          {i₁ : X₁ ⟶ Y₁} →
            {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} →
              {i₂ : X₂ ⟶ t₁.pt} →
                (t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂) →
                  (hi₂ : i₂ = t₁.inr) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit (t₁.pasteHoriz t₂ hi₂) ≃ CategoryTheory.Limits.IsColimit t₂
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.MonOpOpToComonObj_comon_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon Cᵒᵖ), CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.mul.unop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_ne_nil : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], r.toList ≠ []
-- Init.Data.List.MapIdx
List.mapFinIdx_append : ∀ {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : (i : ℕ) → α → i < (xs ++ ys).length → β},
  (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun i a h => f i a ⋯) ++ ys.mapFinIdx fun i a h => f (i + xs.length) a ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_keys_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)), (Std.Internal.List.keys l).isEmpty = l.isEmpty
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommSemigroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : CommSemigroup Y],
  LocallyConstant.instCommSemigroup = Function.Injective.commSemigroup DFunLike.coe ⋯ ⋯
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.decidableMemCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : AddMonoid M] → (a : M) → [Decidable (∀ b ∈ S, b + a = a + b)] → Decidable (a ∈ AddSubmonoid.centralizer S)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsStarProjection.conjugate_of_nonneg_of_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a e : A},
  IsStarProjection e → 0 ≤ a → a ≤ e → e * a * e = a
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.sumInv_pqr : ∀ (p q r : ℕ+), ADEInequality.sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.instSMulRat : {K : Type u} →
  [inst : DivisionRing K] → {S : Type u_1} → [inst_1 : SetLike S K] → [h : SubfieldClass S K] → (s : S) → SMul ℚ ↥s
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `χ m` is the only map for which the associated square
is a pullback square.
 -/
CategoryTheory.HasSubobjectClassifier.unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] (χ' : X ⟶ CategoryTheory.HasSubobjectClassifier.Ω C),
  CategoryTheory.IsPullback m (⋯.some.χ₀ U) χ' (CategoryTheory.HasSubobjectClassifier.truth C) →
    χ' = CategoryTheory.HasSubobjectClassifier.χ m
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_econs_bot : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post : Value → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post Lean.Order.bot) (Std.Internal.Do.wp x post epost)
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int16
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_pos'`.  -/
add_pos' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 < a → 0 < b → 0 < a + b
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.below.of : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} (X : C) (S : CategoryTheory.Presieve X)
  (hS : S ∈ K.coverings X), CategoryTheory.Coverage.Saturate.below ⋯
-- Mathlib.LinearAlgebra.Multilinear.Pi
/-- When applied to a family of finitely-supported functions each supported on a single element,
`piFamily` is itself supported on a single element, with value equal to the map `f` applied
at that point.  -/
MultilinearMap.piFamily_single : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] [inst_5 : Fintype ι] [inst_6 : (i : ι) → DecidableEq (κ i)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (p : (i : ι) → κ i) (m : (i : ι) → M i (p i)),
  ((MultilinearMap.piFamily f) fun i => Pi.single (p i) (m i)) = Pi.single p ((f p) m)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mk_eq_inl_mul_inr : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G) (n : N),
  ⟨n, g⟩ = SemidirectProduct.inl n * SemidirectProduct.inr g
-- Init.Data.List.SplitOn.Lemmas
/-- `intercalate [x]` is the left inverse of `splitOn x`  -/
List.intercalate_splitOn : ∀ {α : Type u_1} {xs : List α} [inst : BEq α] [LawfulBEq α] (x : α), [x].intercalate (List.splitOn x xs) = xs
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.finsetWalkLength.eq_def : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
  G.finsetWalkLength n u v =
    match n with
    | 0 => if h : u = v then ⋯ ▸ {SimpleGraph.Walk.nil} else ∅
    | n.succ =>
      Finset.univ.biUnion fun w =>
        Finset.map { toFun := fun p => SimpleGraph.Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)
-- Mathlib.Topology.Maps.Basic
IsClosedMap.of_inverse : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f' : Y → X},
  Continuous f' → Function.LeftInverse f f' → Function.RightInverse f f' → IsClosedMap f
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_erase_left : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  (Finset.Icc a b).erase a = Finset.Ioc a b
-- Mathlib.Algebra.Opposites
MulOpposite.op_neg : ∀ {α : Type u_1} [inst : Neg α] (x : α), MulOpposite.op (-x) = -MulOpposite.op x
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `B` is flat, then for any family of
`R`-linearly independent elements `{ a_i }` of `A`, and any family of
`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is
also `R`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B] {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B},
      LinearIndependent R a → LinearIndependent R b → LinearIndependent R fun i => ↑(a i.1) * ↑(b i.2)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.minValueSealed_def : Int16.minValueSealed✝ = Int16.minValue
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_erase : ∀ {M : Type u_4} [inst : CommMonoid M] {a : M} {l : List M} [inst_1 : DecidableEq M],
  a ∈ l → a * (l.erase a).prod = l.prod
-- Init.Data.Vector.Count
Vector.one_le_count_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, 1 ≤ Vector.count a xs ↔ a ∈ xs
-- Mathlib.Computability.Reduce
/-- The join of two degrees, induced by the disjoint union of two underlying sets.  -/
ManyOneDegree.instAdd : Add ManyOneDegree
-- Init.Data.String.Lemmas.Splits
String.splits_startPos_iff : ∀ {t₁ t₂ s : String}, s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s
-- Mathlib.Order.Filter.Bases.Basic
Disjoint.exists_mem_filter_basis : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  Disjoint l l' → l.HasBasis p s → l'.HasBasis p' s' → ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.mk : {α : Type u} →
  [toAdd : Add α] →
    [toMul : Mul α] →
      [natCast : NatCast α] →
        [ofNat : (n : ℕ) → OfNat α n] →
          [nsmul : SMul ℕ α] →
            [npow : HPow α ℕ α] →
              (∀ (a : α), a + 0 = a) →
                (∀ (a b : α), a + b = b + a) →
                  (∀ (a b c : α), a + b + c = a + (b + c)) →
                    (∀ (a b c : α), a * b * c = a * (b * c)) →
                      (∀ (a : α), a * 1 = a) →
                        (∀ (a : α), 1 * a = a) →
                          (∀ (a b c : α), a * (b + c) = a * b + a * c) →
                            (∀ (a b c : α), (a + b) * c = a * c + b * c) →
                              (∀ (a : α), 0 * a = 0) →
                                (∀ (a : α), a * 0 = 0) →
                                  (∀ (a : α), a ^ 0 = 1) →
                                    (∀ (a : α) (n : ℕ), a ^ (n + 1) = a ^ n * a) →
                                      autoParam (∀ (a : ℕ), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1)
                                          Lean.Grind.Semiring.ofNat_succ._autoParam →
                                        autoParam (∀ (n : ℕ), OfNat.ofNat n = ↑n)
                                            Lean.Grind.Semiring.ofNat_eq_natCast._autoParam →
                                          autoParam (∀ (n : ℕ) (a : α), n • a = ↑n * a)
                                              Lean.Grind.Semiring.nsmul_eq_natCast_mul._autoParam →
                                            Lean.Grind.Semiring α
-- Mathlib.Topology.Compactification.StoneCech
continuous_ultrafilter_extend : ∀ {α : Type u} {γ : Type u_1} [inst : TopologicalSpace γ] [T2Space γ] [CompactSpace γ] (f : α → γ),
  Continuous (Ultrafilter.extend f)
-- Mathlib.RepresentationTheory.Equiv
Representation.ofMulActionSubsingletonEquivTrivial_symm_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Monoid G] (H : Type w) [inst_2 : Subsingleton H]
  [inst_3 : MulOneClass H] [inst_4 : MulAction G H] (r : k),
  (↑(Representation.ofMulActionSubsingletonEquivTrivial k G H).symm).toLinearMap r = MonoidAlgebra.single 1 r
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_zero_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal), ∫⁻ (a : α), f a ∂0 = 0
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.map.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] (g : 𝒜 →+*ᵍ ℬ) (f : A),
  HomogeneousLocalization.Away.map g f = HomogeneousLocalization.map g ⋯
-- Std.Time.Time.HourMarker
/-- Converts a 24-hour clock time to a 12-hour clock time with a `HourMarker`.
 -/
Std.Time.HourMarker.toRelative : Std.Time.Hour.Ordinal → Std.Time.Internal.Bounded.LE 1 12 × Std.Time.HourMarker
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (φ : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.map₂ α β).map φ).left = F.map φ.left
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.isSeparated : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.coe_piOrderIso_apply : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] [inst_1 : Finite ι] (a : Ideal ((i : ι) → R i))
  (i : ι), ↑(Ideal.piOrderIso a i) = ⋂ s, ⋂ (_ : ↑a ⊆ (fun a => a i) ⁻¹' ↑s), ↑s
-- Mathlib.CategoryTheory.Limits.Creates
/-- `liftLimit t` is the cone for `K` given by lifting the limit `t` for `K ⋙ F`.  -/
CategoryTheory.liftLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [CategoryTheory.CreatesLimit K F] →
                  {c : CategoryTheory.Limits.Cone (K.comp F)} →
                    CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.Cone K
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsRepresentableObjOppositeTypeUliftYoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).IsRepresentable
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
min_lt_of_mul_lt_sq : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] [MulRightMono M] {a b c : M},
  a * b < c ^ 2 → min a b < c
-- Mathlib.Data.List.Nodup
List.Nodup.filter : ∀ {α : Type u} (p : α → Bool) {l : List α}, l.Nodup → (List.filter p l).Nodup
-- Mathlib.NumberTheory.LucasLehmer
/-- The cardinality of `X` is `q^2`.  -/
LucasLehmer.X.card_eq : ∀ {q : ℕ} [inst : NeZero q], Fintype.card (LucasLehmer.X q) = q ^ 2
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.lift.congr_simp : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (f f_1 : V →ₗ[k] W) (e_f : f = f_1) (h : ∀ (x : G), f ∘ₗ ρ x = f),
  Representation.Coinvariants.lift ρ f h = Representation.Coinvariants.lift ρ f_1 ⋯
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_sum : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_3} {s : Finset ι} {ν : ι → MeasureTheory.FiniteMeasure Ω},
  ↑(∑ i ∈ s, ν i) = ∑ i ∈ s, ↑(ν i)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
/-- Finds the first row starting from the `rowStart` with nonzero element in the column `col`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.findNonzeroRow : {n m : ℕ} →
  {matType : ℕ → ℕ → Type} →
    [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
      ℕ → ℕ → Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM n m matType (Option ℕ)
-- Mathlib.Data.Rat.Lemmas
Rat.add_natCast_den : ∀ (q : ℚ) (n : ℕ), (q + ↑n).den = q.den
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ioi a
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), (OrderMonoidHom.id β).comp f = f
-- Mathlib.Algebra.Group.Basic
mul_ne_right : ∀ {M : Type u_4} [inst : Monoid M] [IsRightCancelMul M] {a b : M}, a * b ≠ b ↔ a ≠ 1
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.injective_arg : Function.Injective fun z => (↑z).arg
-- Mathlib.FieldTheory.Galois.Profinite
/-- The functor from `FiniteGaloisIntermediateField` (ordered by reverse inclusion) to `FiniteGrp`,
mapping each `FiniteGaloisIntermediateField` `L` to `Gal (L/k)`  -/
finGaloisGroupFunctor : (k : Type u_1) →
  (K : Type u_2) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ FiniteGrp.{u_2}
-- Mathlib.Order.Filter.Basic
Filter.principal_neBot_iff : ∀ {α : Type u} {s : Set α}, (Filter.principal s).NeBot ↔ s.Nonempty
-- Std.Tactic.Do.Syntax
/-- `mspec_no_simp $spec` first tries to decompose `Bind.bind`s before applying `$spec`.
This variant of `mspec_no_simp` does not; `mspec_no_bind $spec` is defined as
```
try with_reducible mspec_no_bind Std.Do.Spec.bind
mspec_no_bind $spec
```
 -/
Lean.Parser.Tactic.mspecNoBind : Lean.ParserDescr
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.mem_bot : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  ChainCompletePartialOrder.IsExtremePt x f y → y ∈ ChainCompletePartialOrder.bot x f
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_mono : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L]
  (K K' : IntermediateField F L) [Normal F L],
  K ≤ K' → IntermediateField.normalClosure F (↥K) L ≤ IntermediateField.normalClosure F (↥K') L
-- Mathlib.Tactic.ByContra
_private.Mathlib.Tactic.ByContra.0.Mathlib.Tactic.ByContra.tacticTry_push_neg_ : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqCompletionItem.beq : Lean.Lsp.CompletionItem → Lean.Lsp.CompletionItem → Bool
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- In the special case `F = yoneda.obj Y`, the element `p.val` for `p : OverArrows η s` is itself
a morphism `X ⟶ Y`.  -/
CategoryTheory.OverPresheafAux.OverArrows.map_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A}
  (p : CategoryTheory.OverPresheafAux.OverArrows η s),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map p.val) η = s
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Provided we have the appropriate equalizers, we have an adjunction to the comparison functor.
 -/
CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              [inst_2 :
                  ∀ (A : adj.toComonad.Coalgebra),
                    CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] →
                CategoryTheory.Comonad.comparison adj ⊣
                  CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison adj
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.request.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID) (method : String) (params? : Option Lean.Json.Structured),
  sizeOf (Lean.JsonRpc.Message.request id method params?) = 1 + sizeOf id + sizeOf method + sizeOf params?
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toList_flatMapAfter : ∀ {α α₂ β γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} {it₂ : Option (Std.Iter γ)},
  (Std.Iter.flatMapAfter f it₁ it₂).toList =
    match it₂ with
    | none => (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten
    | some it₂ => it₂.toList ++ (Std.Iter.map (fun b => (f b).toList) it₁).toList.flatten
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G},
  H.Normal → ∀ (f : G →* N), Function.Surjective ⇑f → (Subgroup.map f H).Normal
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- **Alias** of `CategoryTheory.Adjunction.homEquiv_apply`. -/
CategoryTheory.Adjunction.homEquiv_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) (Y : D) (f : F.obj X ⟶ Y),
  (adj.homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (G.map f)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableWithinAt.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {f : E → E},
  DifferentiableWithinAt 𝕜 f s x → f x = x → Set.MapsTo f s s → ∀ (n : ℕ), DifferentiableWithinAt 𝕜 f^[n] s x
-- Batteries.Util.Cache
/-- Cached fold over the environment's declarations,
where a given function is applied to `α` for every constant.
 -/
Batteries.Tactic.DeclCache : Type → Type
-- Mathlib.RingTheory.FreeCommRing
/-- A helper to implement `lift`. This is essentially `FreeCommMonoid.lift`, but this does not
currently exist.  -/
_private.Mathlib.RingTheory.FreeCommRing.0.FreeCommRing.liftToMultiset : {α : Type u} → {R : Type v} → [inst : CommRing R] → (α → R) ≃ (Multiplicative (Multiset α) →* R)
-- Mathlib.Topology.Algebra.Ring.Basic
Subring.instIsSemitopologicalRing : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsSemitopologicalRing R] (S : Subring R),
  IsSemitopologicalRing ↥S
-- Mathlib.Data.Set.Insert
Set.insert_inj : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∉ s → (insert a s = insert b s ↔ a = b)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart = μ - ν