mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.fix f k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_5 f k
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.zero_empty : ∀ {α : Type u_1} [inst : Zero α], 0 = ![]
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `f` is a monotone function and `g` tends to `atTop` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`.

This lemma together with `exists_seq_monotone_tendsto_atTop_atTop` below
is useful to reduce a statement
about a monotone family indexed by a type with countably generated `atTop` (e.g., `ℝ`)
to the case of a family indexed by natural numbers.  -/
Monotone.upperBounds_range_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {l : Filter α} [l.NeBot]
  {f : β → γ},
  Monotone f →
    ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The domain of a morphism.  -/
Mathlib.Tactic.Monoidal.srcExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Logic.Relator
Relator.BiTotal.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop},
  (∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) →
    Relator.BiTotal r₁₂ → Relator.BiTotal r₂₃ → Relator.BiTotal r₁₃
-- Mathlib.Algebra.Polynomial.Monic
/-- The type of monic polynomials of degree `n`.

The implementation is slightly different because it is useful to still contain `X ^ n` when
`R` is trivial. See `MonicDegreeEq.mk` for the usual constructor.
 -/
Polynomial.MonicDegreeEq : (R : Type u) → ℕ → [Semiring R] → Type u
-- Mathlib.Algebra.Order.Kleene
nsmul_eq_self : ∀ {α : Type u_1} [inst : IdemSemiring α] {n : ℕ}, n ≠ 0 → ∀ (a : α), n • a = a
-- Init.Data.Array.Extract
Array.popWhile_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  Array.popWhile p (xs ++ ys) =
    if (Array.popWhile p ys).isEmpty = true then Array.popWhile p xs else xs ++ Array.popWhile p ys
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_inv' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜], (deriv fun x => x⁻¹) = fun x => -(x ^ 2)⁻¹
-- Mathlib.RingTheory.WittVector.Compare
WittVector.fromPadicInt_comp_toPadicInt_ext : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)),
  ((WittVector.fromPadicInt p).comp (WittVector.toPadicInt p)) x = (RingHom.id (WittVector p (ZMod p))) x
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- The class of local subrings of a commutative ring.  -/
LocalSubring : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.sub_toLinearMap : ∀ {A : Type u_1} {G : Type u_2} [inst : Semiring A] [inst_1 : Monoid G] {V : Type u_6} {W : Type u_7}
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommGroup W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ),
  (f - g).toLinearMap = f.toLinearMap - g.toLinearMap
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α}, m.WF → m.keysArray.contains k = m.contains k
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α],
  Std.ExtDHashMap.ofList [] = ∅
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Hard part of FTC-2 for integrable derivatives, real-valued functions: one has
`g b - g a ≤ ∫ y in a..b, g' y` when `g'` is integrable.
Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`.
We give the slightly more general version that `g b - g a ≤ ∫ y in a..b, φ y` when `g' ≤ φ` and
`φ` is integrable (even if `g'` is not known to be integrable).
Version assuming that `g` is differentiable on `(a, b)`.  -/
intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le : ∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    ContinuousOn g (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
        MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
          (∀ x ∈ Set.Ioo a b, g' x ≤ φ x) → g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_eq_zero : ∀ {n : ℕ}, ArithmeticFunction.cardDistinctFactors n = 0 ↔ n ≤ 1
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 f s x → ContinuousWithinAt f s x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.invFun_eq_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] {e : A ≃⋆ₐ[R] B},
  EquivLike.inv e = ⇑e.symm
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.restrictScalars_toAlgHom : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (R₀ : Type u_11)
  [inst_9 : CommSemiring R₀] [inst_10 : Algebra R₀ R] [inst_11 : Algebra R₀ A] [inst_12 : Algebra R₀ B]
  [inst_13 : IsScalarTower R₀ R A] [inst_14 : IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ),
  AlgHom.restrictScalars R₀ ↑f = ↑(↑R₀ f)
-- Mathlib.Analysis.Normed.Algebra.Ultra
/-- The other direction of `IsUltrametricDist.of_normedAlgebra`.
Let `K` be a normed field. If a seminormed ring `L` is a normed `K`-algebra, and `‖1‖ = 1` in `L`,
then `K` is ultrametric (i.e. the norm on `L` is nonarchimedean) if `F` is.
This can be further generalized to the case where `‖1‖ ≠ 0` in `L`.
 -/
IsUltrametricDist.of_normedAlgebra' : ∀ {K : Type u_1} (L : Type u_2) [inst : NormedField K] [inst_1 : SeminormedRing L] [NormOneClass L] [NormedAlgebra K L]
  [h : IsUltrametricDist L], IsUltrametricDist K
-- Mathlib.Order.Filter.Partial
Filter.rtendsto_def : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
/-- Let `X : C` be an object in a Grothendieck abelian category,
`F : J ⥤ MonoOver X` a functor from a filtered category, `c` a cocone for
the composition `F ⋙ MonoOver.forget _ : J ⥤ Over X`. We assume
that `c.pt.hom : c.pt.left ⟶ X` is a monomorphism and that the corresponding
subobject of `X` is the supremum of the subobjects given by `(F.obj j).obj.hom`,
then `c` becomes a colimit cocone after the application of
the forget functor `Over X ⥤ C`. (See also `subobjectMk_of_isColimit_eq_iSup`.)  -/
CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
        {X : C} →
          {J : Type w} →
            [inst_3 : CategoryTheory.SmallCategory J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) →
                [CategoryTheory.IsFiltered J] →
                  (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.MonoOver.forget X))) →
                    [inst_5 : CategoryTheory.Mono c.pt.hom] →
                      CategoryTheory.Subobject.mk c.pt.hom = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom →
                        CategoryTheory.Limits.IsColimit ((CategoryTheory.Over.forget X).mapCocone c)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
FreeAlgebra.toTensor.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  FreeAlgebra.toTensor = (FreeAlgebra.lift R) ⇑(TensorAlgebra.ι R)
-- Mathlib.CategoryTheory.ComposableArrows.Four
/-- The morphism `mk₃ f₁₂ f₃ f₄ ⟶ mk₃ f₂ f₃ f₄` when `f₁ ≫ f₂ = f₁₂`.  -/
CategoryTheory.ComposableArrows.fourδ₁Toδ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i₀ i₁ i₂ i₃ i₄ : C} →
      (f₁ : i₀ ⟶ i₁) →
        (f₂ : i₁ ⟶ i₂) →
          (f₃ : i₂ ⟶ i₃) →
            (f₄ : i₃ ⟶ i₄) →
              (f₁₂ : i₀ ⟶ i₂) →
                autoParam (CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
                    CategoryTheory.ComposableArrows.fourδ₁Toδ₀._auto_1 →
                  (CategoryTheory.ComposableArrows.mk₃ f₁₂ f₃ f₄ ⟶ CategoryTheory.ComposableArrows.mk₃ f₂ f₃ f₄)
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_le_le_eq_Icc : ∀ {α : Type u_2} (a b : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun j => a ≤ j ∧ j ≤ b], {j | a ≤ j ∧ j ≤ b} = Finset.Icc a b
-- Init.Core
imp_true_iff : ∀ (α : Sort u), (∀ (a : α), True) ↔ True
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_mul_pow_card : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} {b : M},
  (∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈ s, f a * b
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.card_sum : ∀ {ι : Type u_1} {α : Type u_6} (s : Finset ι) (f : ι → Multiset α), (∑ i ∈ s, f i).card = ∑ i ∈ s, (f i).card
-- Lean.Structure
Lean.StructureFieldInfo.mk.injEq : ∀ (fieldName projFn : Lean.Name) (subobject? : Option Lean.Name) (binderInfo : Lean.BinderInfo)
  (autoParam? : Option Lean.Expr) (fieldName_1 projFn_1 : Lean.Name) (subobject?_1 : Option Lean.Name)
  (binderInfo_1 : Lean.BinderInfo) (autoParam?_1 : Option Lean.Expr),
  ({ fieldName := fieldName, projFn := projFn, subobject? := subobject?, binderInfo := binderInfo,
        autoParam? := autoParam? } =
      { fieldName := fieldName_1, projFn := projFn_1, subobject? := subobject?_1, binderInfo := binderInfo_1,
        autoParam? := autoParam?_1 }) =
    (fieldName = fieldName_1 ∧
      projFn = projFn_1 ∧ subobject? = subobject?_1 ∧ binderInfo = binderInfo_1 ∧ autoParam? = autoParam?_1)
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `addOrder_eq_card_multiples`.  -/
Nat.card_addSubmonoidMultiples : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {a : G}, Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_sSup : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)), (sSup S).unop = sSup (Subsemiring.op ⁻¹' S)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.isIso_ranAdjunction_homEquiv_iff : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] {F : CategoryTheory.Functor C H}
  {G : CategoryTheory.Functor D H} (α : L.comp G ⟶ F),
  CategoryTheory.IsIso (((L.ranAdjunction H).homEquiv G F) α) ↔ G.IsRightKanExtension α
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- A function `f` is differentiable at `conj z` iff `conj ∘ f ∘ conj` is differentiable at `z`.  -/
differentiableAt_conj_conj_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {x : 𝕜} [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜},
  DifferentiableAt 𝕜 (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) x ↔ DifferentiableAt 𝕜 f ((starRingEnd 𝕜) x)
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution is associative.  -/
MeasureTheory.Measure.mconv_assoc : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], (μ.mconv ν).mconv ρ = μ.mconv (ν.mconv ρ)
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIcoDiv` is eventually constant on the right at every point.  -/
eventuallyEq_toIcoDiv_nhdsGE : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  toIcoDiv hp a =ᶠ[nhdsWithin x (Set.Ici x)] fun x_1 => toIcoDiv hp a x
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The underlying substructure  -/
FirstOrder.Language.ElementarySubstructure.toSubstructure : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → L.ElementarySubstructure M → L.Substructure M
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.compLinearMapMultilinear_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (f : (i : ι) → M₁ i →ₗ[R] M₁' i), MultilinearMap.compLinearMapMultilinear f = MultilinearMap.compLinearMapₗ f
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.erase.eq_1 : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α),
  SkewMonoidAlgebra.erase a = { toFun := fun f => { coeff := Finsupp.erase a f.coeff }, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.msb_cons : ∀ {a : Bool} {w : ℕ} {x : BitVec w}, (BitVec.cons a x).msb = a
-- Lean.Data.PersistentArray
Lean.PersistentArray.anyMAux : {α : Type u} → {m : Type → Type w} → [Monad m] → (α → m Bool) → Lean.PersistentArrayNode α → m Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.mk.sizeOf_spec : ∀ (label : String) (detail? : Option String) (documentation? : Option Lean.Lsp.MarkupContent)
  (kind? : Option Lean.Lsp.CompletionItemKind) (textEdit? : Option Lean.Lsp.InsertReplaceEdit)
  (sortText? : Option String) (data? : Option Lean.Json) (tags? : Option (Array Lean.Lsp.CompletionItemTag)),
  sizeOf
      { label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
    1 + sizeOf label + sizeOf detail? + sizeOf documentation? + sizeOf kind? + sizeOf textEdit? + sizeOf sortText? +
        sizeOf data? +
      sizeOf tags?
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  Bicategory.Opposite.op2 (CategoryTheory.CategoryStruct.comp η θ) =
    CategoryTheory.CategoryStruct.comp (Bicategory.Opposite.op2 η) (Bicategory.Opposite.op2 θ)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.insert : {β : Type} → Lean.ScopedEnvExtension.ScopedEntries β → Lean.Name → β → Lean.ScopedEnvExtension.ScopedEntries β
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.exists_root_eq_sum_nat_or_neg : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base) (i : ι),
  ∃ f,
    Function.support f ⊆ ↑b.support ∧
      (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ P.root i = -∑ j ∈ b.support, f j • P.root j)
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Partial sums of an alternating monotone series with an odd number of terms provide
lower bounds on the limit.  -/
Monotone.alternating_series_le_tendsto : ∀ {E : Type u_4} [inst : Ring E] [inst_1 : PartialOrder E] [IsOrderedRing E] [inst_3 : TopologicalSpace E]
  [OrderClosedTopology E] {l : E} {f : ℕ → E},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l) →
    Monotone f → ∀ (k : ℕ), ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l
-- Lean.Data.Json.Parser
Lean.Json.Parser.numSign : Std.Internal.Parsec.String.Parser ℤ
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_eq_iff_im : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, (starRingEnd K) z = z ↔ RCLike.im z = 0
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
TwoSidedIdeal.ker_eq_bot : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_3}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  TwoSidedIdeal.ker f = ⊥ ↔ Function.Injective ⇑f
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Category structure on the oplax natural transformations between lax functors.

Note that this is a scoped instance in the `Lax.OplaxTrans` namespace.  -/
CategoryTheory.Lax.OplaxTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZPowersEqTop_symm_self : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : Group G] {g : G} (hg : Subgroup.zpowers g = ⊤),
  (intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1
-- Std.Async.Basic
Std.Async.EAsync.instMonadLiftEIO : {ε : Type} → MonadLift (EIO ε) (Std.Async.EAsync ε)
-- Init.Data.List.MinMaxOn
/-- Returns an element of the non-empty list `l` that maximizes `f`. If `x`, `y` are
such that `f x = f y`, it returns whichever comes first in the list.

The correctness of this function assumes `β` to be linearly pre-ordered.
The property that `List.maxOn` is the first maximizer in the list is guaranteed by the lemma
`List.getElem_maxIdxOn`.
 -/
List.maxOn : {β : Type u_1} → {α : Type u_2} → [i : LE β] → [DecidableLE β] → (α → β) → (l : List α) → l ≠ [] → α
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withFunLocalDecls.loop : {α : Type} →
  Array Lean.Elab.DefViewElabHeader →
    (Array Lean.Expr → Lean.Elab.TermElabM α) → ℕ → Array Lean.Expr → Lean.Elab.TermElabM α
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (l : List α),
  List.scanAuxM✝ f init l = List.scanAuxM.go✝ f l init []
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The left arrow of the walking cospan.  -/
CategoryTheory.Limits.WalkingCospan.Hom.inl : CategoryTheory.Limits.WalkingCospan.left ⟶ CategoryTheory.Limits.WalkingCospan.one
-- Aesop.Tree.Data
Aesop.Goal.hasMVar : Aesop.Goal → Bool
-- Mathlib.Geometry.Manifold.Instances.Real
range_euclideanQuadrant : ∀ (n : ℕ), Set.range Subtype.val = {y | ∀ (i : Fin n), 0 ≤ y.ofLp i}
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.FieldTheory.Perfect
/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable.  -/
Algebra.IsAlgebraic.isSeparable_of_perfectField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  [PerfectField K], Algebra.IsSeparable K L
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a multivariate power series is the the minimum total degree over all
exponents `d` with nonzero coefficient `coeff d f`.  -/
MvPowerSeries.order : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → MvPowerSeries σ R → ℕ∞
-- Lean.Data.Lsp.Basic
/-- The content of the opened text document.  -/
Lean.Lsp.TextDocumentItem.text : Lean.Lsp.TextDocumentItem → String
-- Mathlib.Analysis.Normed.Ring.Basic
/-- This class states that a ring homomorphism is isometric. This is a sufficient assumption
for a continuous semilinear map to be bounded and this is the main use for this typeclass.  -/
RingHomIsometric : {R₁ : Type u_5} →
  {R₂ : Type u_6} → [inst : Semiring R₁] → [inst_1 : Semiring R₂] → [Norm R₁] → [Norm R₂] → (R₁ →+* R₂) → Prop
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vsub_vsub_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P), dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_symm_zero : ∀ {n : ℕ} [inst : NeZero n] (i : Fin n), (Equiv.symm i.cycleRange) 0 = i
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage.eq_1 : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α),
  birkhoffAverage R f g n x = (↑n)⁻¹ • birkhoffSum f g n x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is positive.  -/
InnerProductGeometry.angle_add_pos_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → 0 < InnerProductGeometry.angle x (x + y)
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.exists_lt : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α},
  s.PartiallyWellOrderedOn r → ∀ {f : ℕ → α}, (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.δ_comp_σ_succ : ∀ {n : ℕ} {i : Fin (n + 1)},
  FreeSimplexQuiver.homRel
    (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.succ))
      ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ i)))
    (CategoryTheory.CategoryStruct.id ((CategoryTheory.Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk n)))
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_zero : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃), g ∘ₛₗ 0 = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `α ≫ β`  -/
Mathlib.Tactic.BicategoryLike.MkEvalComp.mkEvalCompNilNil : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsMultiplicative