mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSet.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J J_1 : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))),
  J = J_1 →
    ∀ (a a_1 : NumberField.mixedEmbedding.mixedSpace K),
      a = a_1 →
        NumberField.mixedEmbedding.fundamentalCone.idealSet K J a =
          NumberField.mixedEmbedding.fundamentalCone.idealSet K J_1 a_1
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
_private.Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum.0.ZMod.χ₄.match_1.eq_3 : ∀ (motive : ZMod 4 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 1)
  (h_4 : Unit → motive 3),
  (match 1 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 1 => h_3 ()
    | 3 => h_4 ()) =
    h_3 ()
-- Mathlib.Util.AtomM.Recurse
/-- Configuration for `AtomM.Recurse`.  -/
Mathlib.Tactic.AtomM.Recurse.Config : Type
-- Init.Data.Ord.Basic
Ordering.ne_eq_of_eq_lt : ∀ {o : Ordering}, o = Ordering.lt → o ≠ Ordering.eq
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.out.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (A : MulArchimedeanClass M),
  A.out = MulArchimedeanOrder.val (Quotient.out A)
-- Mathlib.RingTheory.Idempotents
RingHom.prod_bijective_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {e f : R},
  IsIdempotentElem e →
    IsIdempotentElem f →
      e + f = 1 →
        e * f = 0 → Function.Bijective ⇑((Ideal.Quotient.mk (Ideal.span {e})).prod (Ideal.Quotient.mk (Ideal.span {f})))
-- Init.Data.List.Nat.Modify
List.eraseIdx_modify_of_gt : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), j > i → (l.modify i f).eraseIdx j = (l.eraseIdx j).modify i f
-- Init.Data.SInt.Lemmas
Int8.toInt_eq_toNatClampNeg : ∀ {a : Int8}, 0 ≤ a → a.toInt = ↑a.toNatClampNeg
-- Lean.Util.LeanOptions
/-- Formats the lean option as a CLI argument using the `-D` flag.  -/
Lean.LeanOption.asCliArg : Lean.LeanOption → String
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- `c • f` is majorized with the same exponent as `f` for any constant `c`.  -/
Tactic.ComputeAsymptotics.Majorized.smul : ∀ {f b : ℝ → ℝ} {exp : ℝ},
  Tactic.ComputeAsymptotics.Majorized f b exp → ∀ {c : ℝ}, Tactic.ComputeAsymptotics.Majorized (c • f) b exp
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the first vector passed to `oangle` from the second vector does not change the
sign of the angle.  -/
Orientation.oangle_sign_sub_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle x (y - x)).sign = (o.oangle x y).sign
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
IsGreatest.directedOn : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α},
  IsGreatest s a → DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.mk : ℕ → ℕ → Lean.Lsp.LineRange
-- Mathlib.Order.RelSeries
RelSeries.snoc.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (p p_1 : RelSeries r) (e_p : p = p_1) (newLast newLast_1 : α)
  (e_newLast : newLast = newLast_1) (rel : (p.last, newLast) ∈ r), p.snoc newLast rel = p_1.snoc newLast_1 ⋯
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C},
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P.isoClosure T.obj₃) →
    P.IsTriangulatedClosed₃
-- Mathlib.Algebra.Group.Conj
isConj_iff_conjugatesOf_eq : ∀ {α : Type u} [inst : Monoid α] {a b : α}, IsConj a b ↔ conjugatesOf a = conjugatesOf b
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.rotate_distinguished_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C]
  (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))),
  T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C ↔
    T.rotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_toUInt16 : ∀ (n : UInt8), n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsLeftQuasiInverse.equiv : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃},
  u.IsLeftQuasiInverse v → u ∘ₗ v ≈ LinearMap.id
-- Mathlib.Order.UpperLower.Prod
UpperSet.Ici_prod_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α) (b : β),
  UpperSet.Ici a ×ˢ UpperSet.Ici b = UpperSet.Ici (a, b)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The isomorphism between homotopy cofibers that is induced by an
isomorphism of arrows.  -/
HomologicalComplex.homotopyCofiber.mapArrowIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  {F' G' : HomologicalComplex C c} →
                    (φ' : F' ⟶ G') →
                      [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] →
                        (∀ (j : ι), ∃ i, c.Rel i j) →
                          (CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ') →
                            (HomologicalComplex.homotopyCofiber φ ≅ HomologicalComplex.homotopyCofiber φ')
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus.congr_simp : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] {inst_1 : DecidableEq N} [inst_2 : DecidableEq N]
  [inst_3 : Zero N] (f f_1 : α →₀ N), f = f_1 → ∀ (g g_1 : α →₀ N), g = g_1 → f.neLocus g = f_1.neLocus g_1
-- Mathlib.Algebra.CharZero.Defs
charZero_of_inj_zero : ∀ {R : Type u_1} [inst : AddGroupWithOne R], (∀ (n : ℕ), ↑n = 0 → n = 0) → CharZero R
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassForall : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : SMul M α] [inst_1 : SMul N β],
  SMulCommClass Mᵈᵐᵃ N (α → β)
-- Mathlib.Order.Monotone.Basic
antitoneOn_nat_Ici_of_succ_le : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (∀ n ≥ k, f (n + 1) ≤ f n) → AntitoneOn f {x | k ≤ x}
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.of_nhds_zero' : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) →
        (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x + x₀) (nhds 0)) → IsTopologicalAddGroup G
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α} {h' : a ∈ m}, m[a] = m[a]!
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An alternative constructor for `Hom`,
taking a morphism without a `[IsModHom]` instance, between objects with
a `ModObj` instance (rather than bundled as `Mod`),
as well as the relevant equality to put such an instance.  -/
CategoryTheory.Mod.Hom.mk'' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : D} →
                  [inst_5 : CategoryTheory.ModObj A M] →
                    [inst_6 : CategoryTheory.ModObj A N] →
                      (f : M ⟶ N) →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                                CategoryTheory.ModObj.smul)
                            CategoryTheory.Mod.Hom.mk''._auto_1 →
                          { X := M, mod := inst_5 }.Hom { X := N, mod := inst_6 }
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.coconeAtFunctor_obj : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) (E : L.LeftExtension F),
  (CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).obj E = E.coconeAt Y
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep_iff_finsetSum_eq_imp_eq : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  (p : ι → Submodule R N),
  iSupIndep p ↔
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.emptyUnique : {ι : Type u_1} →
  {R : Type u_3} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [Subsingleton M] → [IsEmpty ι] → Unique (Module.Basis ι R M)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- The Riesz content `λ` associated to a given positive linear functional `Λ` is
finitely subadditive: `λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂)` for any compact subsets `K₁, K₂ ⊆ X`.  -/
rieszContentAux_sup_le : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] (K1 K2 : TopologicalSpace.Compacts X),
  rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
-- Mathlib.Data.Set.Insert
/-- **Alias** of `Set.ofPred_eq_eq_singleton'`. -/
Set.setOf_eq_eq_singleton' : ∀ {α : Type u_1} {a : α}, {x | a = x} = {a}
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
      (Std.Internal.List.alterKey k f l).isEmpty = false →
        (Std.Internal.List.minKeyD (Std.Internal.List.alterKey k f l) fallback = k ↔
          (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
            ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofRepr.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SizeOf ι] [inst_4 : SizeOf R] [inst_5 : SizeOf M] (repr : M ≃ₗ[R] ι →₀ R),
  sizeOf { repr := repr } = 1 + sizeOf repr
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.div.go.match_1.splitter : (x : ℕ) →
  (motive : (fuel : ℕ) → x < fuel → Sort u_1) →
    (fuel : ℕ) →
      (hfuel : x < fuel) → ((fuel : ℕ) → (hfuel : x < fuel.succ) → motive fuel.succ hfuel) → motive fuel hfuel
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.rclikeToReal_apply : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, 𝕜)) (x : X),
  f.rclikeToReal x = RCLike.re (f x)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {fallback : Unit}, (t.insertManyIfNewUnit l).getD k fallback = ()
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀)
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').hom.app X_1).fst.app x =
    CategoryTheory.CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X_1.fst.obj x)))
-- Mathlib.Algebra.Group.Action.Pi
Function.update_vadd : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst_1 : DecidableEq ι] (c : M)
  (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i), Function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ Function.update f₁ i x₁
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
containing `s` contains the smallest congruence relation containing `r`.  -/
Con.conGen_mono : ∀ {M : Type u_1} [inst : Mul M] {r s : M → M → Prop}, (∀ (x y : M), r x y → s x y) → conGen r ≤ conGen s
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C)
  (X : CategoryTheory.Grothendieck (G.comp F)), ((CategoryTheory.Grothendieck.pre F G).obj X).base = G.obj X.base
-- Mathlib.Control.Functor
Functor.Comp.functor_comp_id : ∀ {F : Type u_1 → Type u_2} [AF : Functor F] [LawfulFunctor F], Functor.Comp.functor = AF
-- Init.Data.BitVec.Lemmas
BitVec.some_eq_getElem?_iff : ∀ {w : ℕ} {a : Bool} {n : ℕ} {l : BitVec w}, some a = l[n]? ↔ ∃ (h : n < w), l[n] = a
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.zero_mem_subsetSum : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M}, 0 ∈ A.subsetSum
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead = 0 → f.nextCoeff = 0
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some '' Set.Iic a = Set.Ioc ⊥ ↑a
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod_left : ∀ (a b : ℤ), (a + b).fmod a = b.fmod a
-- Mathlib.Algebra.Lie.Subalgebra
LieEquiv.ofInjective_apply : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Injective ⇑f) (x : L₁),
  ↑((LieEquiv.ofInjective f h) x) = f x
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_eq : Nat.Internal.Linear.Context → Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly → Prop
-- Std.Data.TreeSet.Basic
/-- Computes the intersection of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.TreeSet.inter : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.TreeSet α cmp → Std.TreeSet α cmp
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_pointwise_smul : ∀ {G : Type u_1} {H : Type u_2} [inst : Group H] (h : H) [inst_1 : AddGroup G] [inst_2 : DistribMulAction H G]
  (J K : AddSubgroup G), (h • J).relIndex (h • K) = J.relIndex K
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a fallback : α}, ∅.getD a fallback = fallback
-- Lean.Meta.LitValues
/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt8` with value `n`.  -/
Lean.Meta.getUInt8Value? : Lean.Expr → Lean.MetaM (Option UInt8)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.hasEval : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S}
  [inst_1 : TopologicalSpace S], MvPowerSeries.HasSubst a → MvPowerSeries.HasEval a
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_conj_eq' : ∀ (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift), (↑f⁻¹ * g * ↑f).translationNumber = g.translationNumber
-- Std.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops over strings.
A loop invariant is a `PostCond` that takes as parameters

* A `String.Pos` representing the current position in the string `s`.
* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
  `let mut` variables and early return.
 -/
Std.Do.StringInvariant : String → Type u → Std.Do.PostShape → Type u
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbers_one : Nat.smoothNumbers 1 = {1}
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- Abbreviation to see a primitive root of unity as a member of the ring of integers.  -/
IsPrimitiveRoot.toInteger : {K : Type u} → [inst : Field K] → {ζ : K} → {k : ℕ} → [NeZero k] → IsPrimitiveRoot ζ k → NumberField.RingOfIntegers K
-- Mathlib.MeasureTheory.PiSystem
generateFrom_piiUnionInter_singleton_left : ∀ {α : Type u_3} {ι : Type u_4} (s : ι → Set α) (S : Set ι),
  MeasurableSpace.generateFrom (piiUnionInter (fun k => {s k}) S) = MeasurableSpace.generateFrom {t | ∃ k ∈ S, s k = t}
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.toHomUnits_mul : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : CommMonoid M] (f g : G →* M),
  (f * g).toHomUnits = f.toHomUnits * g.toHomUnits
-- Init.Sym.Lemmas
Lean.Sym.Fin.lt_eq_true : ∀ {n : ℕ} (a b : Fin n), decide (a < b) = true → (a < b) = True
-- Mathlib.Order.Category.DistLat
DistLat.Hom.ext_iff : ∀ {X Y : DistLat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H : CategoryTheory.Functor D E} [inst_3 : H.Full] [inst_4 : H.Faithful] (comp_iso : F.comp H ≅ G.comp H) (X : C),
  (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
-- Init.Data.String.Basic
String.Pos.le_ofSliceFrom : ∀ {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos}, p₀ ≤ String.Pos.ofSliceFrom pos
-- Mathlib.Data.TypeVec
/-- `PredLast α p x` predicates `p` of the last element of `x : α.append1 β`.  -/
TypeVec.PredLast : {n : ℕ} → (α : TypeVec.{u_1} n) → {β : Type u_1} → (β → Prop) → ⦃i : Fin2 (n + 1)⦄ → (α ::: β) i → Prop
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : α × β) →
          ((fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (x : α × β) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                                (fallback : α × β) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Mathlib.Analysis.Calculus.Deriv.ZPow
differentiableAt_zpow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {m : ℤ}, DifferentiableAt 𝕜 (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (m + j = n) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_1),
  autoParam (j < ↑i) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_3 →
    autoParam (↑i = ↑i' + j) CategoryTheory.SimplicialObject.σ₀Iter_δ'._auto_5 →
      ∀ {Z : C} (h_1 : X.obj (Opposite.op { len := n }) ⟶ Z),
        CategoryTheory.CategoryStruct.comp (X.σ₀Iter j ⋯) (CategoryTheory.CategoryStruct.comp (X.δ i) h_1) =
          CategoryTheory.CategoryStruct.comp (X.δ i') (CategoryTheory.CategoryStruct.comp (X.σ₀Iter j ⋯) h_1)
-- Mathlib.GroupTheory.Sylow
Sylow.pointwise_smul_def : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {g : α}
  {P : Sylow p G}, ↑(g • P) = g • ↑P
-- Lean.Setup
/-- Whether to import IR for all definitions \(transitively\) reachable.  -/
Lean.Import.isMeta : Lean.Import → Bool
-- Mathlib.Data.FP.Basic
FP.Float.inf : [C : FP.FloatCfg] → Bool → FP.Float
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_H0Iso_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G)
  (x : ↑((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).obj A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso A).inv) ((Representation.Coinvariants.mk A.ρ) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π A)) x
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating coface map complex, on objects  -/
AlgebraicTopology.AlternatingCofaceMapComplex.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.CosimplicialObject C → CochainComplex C ℕ
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.gc_map_comap : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L),
  GaloisConnection (Subfield.map f) (Subfield.comap f)