mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Function.Injective.isPartialInv`. -/
Function.partialInv_of_injective : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β}, Function.Injective f → Function.IsPartialInv f (Function.partialInv f)
-- Mathlib.RingTheory.Valuation.Basic
/-- A valuation gives a preorder on the underlying ring.  -/
Valuation.toPreorder : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → Valuation R Γ₀ → Preorder R
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.instLawfulOperatorOverflowInput : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput
    Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β},
  Std.DHashMap.Const.getD (Std.DHashMap.filter f m) k fallback =
    ((Std.DHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The values of a multiplicative character on `R` are `n`th roots of unity, where `n = #Rˣ`.  -/
MulChar.apply_mem_rootsOfUnity : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Fintype Rˣ] (a : Rˣ)
  {χ : MulChar R R'}, (MulChar.equivToUnitHom χ) a ∈ rootsOfUnity (Fintype.card Rˣ) R'
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_le_iff : ∀ {α : Type u_1} {s : Set (Set α)} (m : MeasurableSpace α),
  MeasurableSpace.generateFrom s ≤ m ↔ s ⊆ {t | MeasurableSet t}
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.ite_one_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f : ι → M),
  (if p then 1 else ∏ x ∈ s, f x) = ∏ x ∈ s, if p then 1 else f x
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instPreorder : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [(i : ι) → Preorder (α i)] → Preorder (Π₀ (i : ι), α i)
-- Mathlib.Data.Multiset.NatAntidiagonal
Multiset.Nat.map_swap_antidiagonal : ∀ {n : ℕ}, Multiset.map Prod.swap (Multiset.Nat.antidiagonal n) = Multiset.Nat.antidiagonal n
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_smul : ∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {G : Type u_5} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] (g : G) [SMulCommClass G A B],
  Ideal.under A (g • P) = Ideal.under A P
-- Mathlib.Data.Set.Image
Function.Injective.mem_set_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {s : Set α} {a : α}, f a ∈ f '' s ↔ a ∈ s
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.comp_assoc : ∀ {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
  [inst_3 : Quiver Z] (F : U ⥤q V) (G : V ⥤q W) (H : W ⥤q Z), F ⋙q G ⋙q H = F ⋙q (G ⋙q H)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instSemilatticeInfElemCompactNhdsOfT2Space : {α : Type u_1} →
  [inst : TopologicalSpace α] → [T2Space α] → (K : TopologicalSpace.Compacts α) → SemilatticeInf ↑K.compactNhds
-- Mathlib.Order.Antichain
IsMaxAntichain.isAntichain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxAntichain r s → IsAntichain r s
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- For any `HasTemperateGrowth` measure and `p`, there exists an integer power `k` such that
`(1 + ‖x‖) ^ (-k)` is in `L^p`.  -/
MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] (p : ENNReal) {μ : MeasureTheory.Measure E},
  μ.HasTemperateGrowth → ∃ k, MeasureTheory.eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.match_3.eq_1 : ∀
  (motive :
    (x : Type u_1) →
      (x_1 : CommRing x) →
        (x_2 : Type u_2) →
          (x_3 : AddCommGroup x_2) →
            (x_4 : Module x x_2) → (x_5 : List x) → RingTheory.Sequence.IsWeaklyRegular x_2 x_5 → Sort u_3)
  (R : Type u_1) (x : CommRing R) (M : Type u_2) (x_1 : AddCommGroup M) (x_2 : Module R M)
  (x_3 : RingTheory.Sequence.IsWeaklyRegular M [])
  (h_1 :
    (R : Type u_1) →
      (x : CommRing R) →
        (M : Type u_2) →
          (x_4 : AddCommGroup M) →
            (x_5 : Module R M) → (x_6 : RingTheory.Sequence.IsWeaklyRegular M []) → motive R x M x_4 x_5 [] x_6)
  (h_2 :
    (α : Type u_1) →
      (x : CommRing α) →
        (M : Type u_2) →
          (x_4 : AddCommGroup M) →
            (x_5 : Module α M) →
              (r : α) →
                (rs : List α) →
                  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs)) → motive α x M x_4 x_5 (r :: rs) h),
  (match R, x, M, x_1, x_2, [], x_3 with
    | R, x, M, x_4, x_5, [], x_6 => h_1 R x M x_4 x_5 x_6
    | α, x, M, x_4, x_5, r :: rs, h => h_2 α x M x_4 x_5 r rs h) =
    h_1 R x M x_1 x_2 x_3
-- Init.Data.UInt.Lemmas
UInt16.add_eq_left : ∀ {a b : UInt16}, a + b = a ↔ b = 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.mk.injEq : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (ringInst semiringInst : Lean.Expr) (charInst? : Option (Lean.Expr × ℕ))
  (addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr) (vars : Lean.PArray Lean.Expr)
  (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr) (id_1 : ℕ) (type_1 : Lean.Expr)
  (u_1 : Lean.Level) (ringInst_1 semiringInst_1 : Lean.Expr) (charInst?_1 : Option (Lean.Expr × ℕ))
  (addFn?_1 mulFn?_1 subFn?_1 negFn?_1 powFn?_1 intCastFn?_1 natCastFn?_1 one?_1 : Option Lean.Expr)
  (vars_1 : Lean.PArray Lean.Expr) (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var)
  (denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr),
  ({ id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one?, vars := vars, varMap := varMap,
        denote := denote } =
      { id := id_1, type := type_1, u := u_1, ringInst := ringInst_1, semiringInst := semiringInst_1,
        charInst? := charInst?_1, addFn? := addFn?_1, mulFn? := mulFn?_1, subFn? := subFn?_1, negFn? := negFn?_1,
        powFn? := powFn?_1, intCastFn? := intCastFn?_1, natCastFn? := natCastFn?_1, one? := one?_1, vars := vars_1,
        varMap := varMap_1, denote := denote_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          ringInst = ringInst_1 ∧
            semiringInst = semiringInst_1 ∧
              charInst? = charInst?_1 ∧
                addFn? = addFn?_1 ∧
                  mulFn? = mulFn?_1 ∧
                    subFn? = subFn?_1 ∧
                      negFn? = negFn?_1 ∧
                        powFn? = powFn?_1 ∧
                          intCastFn? = intCastFn?_1 ∧
                            natCastFn? = natCastFn?_1 ∧
                              one? = one?_1 ∧ vars = vars_1 ∧ varMap = varMap_1 ∧ denote = denote_1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, (compare a k).isGE = true) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β ky) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (i : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
      (NumberField.mixedEmbedding.fundamentalCone.completeFamily K ↑i) =
    ↑((NumberField.Units.basisUnitLattice K) (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under addition.  -/
Dioph.«term_D+_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a right cancel semigroup, if it admits an injective map that
preserves `*` to a right cancel semigroup.  See note [reducible non-instances].  -/
Function.Injective.rightCancelSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : RightCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → RightCancelSemigroup M₁
-- Lean.Meta.Sym.SymM
/-- For functions with interlaced rewritable and non-rewritable arguments.
Each element indicates whether the corresponding argument position can be rewritten.

Example: For `HEq {α : Sort u} (a : α) {β : Sort u} (b : β)`, the mask would be
`#[false, true, false, true]` — we can rewrite `a` and `b`, but not `α` or `β`.
 -/
Lean.Meta.Sym.CongrInfo.interlaced : Array Bool → Lean.Meta.Sym.CongrInfo
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_snd : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.snd X TopCat.I) =
    TopCat.const 0
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.universal_property' : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCartesian f φ]
  {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'],
  ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- A Lie derivation `D` from the Lie `R`-algebra `L` to the `L`-module `M` is an `R`-linear map
that satisfies the Leibniz rule `D [a, b] = [a, D b] - [b, D a]`.  -/
LieDerivation : (R : Type u_1) →
  (L : Type u_2) →
    (M : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → Type (max u_2 u_3)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_seq : ∀ {α : Type u_1} {ι' : Sort u_5} [Countable ι'] (x : ι' → Set α), (⨅ i, Filter.principal (x i)).IsCountablyGenerated
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomRestrict_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [inst_5 : DecidablePred P]
  (x : (i : { a // P a }) → M₁ ↑i) (z : (i : { a // ¬P a }) → M₁ ↑i),
  (f.domDomRestrict P z) x = f fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩
-- Std.Http.Data.Status
/-- 103 Early Hints
 -/
Std.Http.Status.earlyHints : Std.Http.Status
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_neg : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], HomologicalComplex.homologyMap (-φ) i = -HomologicalComplex.homologyMap φ i
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivAtFilter.prodMk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {L : Filter (𝕜 × 𝕜)} {G : Type w} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G},
  HasDerivAtFilter f₁ f₁' L → HasDerivAtFilter f₂ f₂' L → HasDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁', f₂') L
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- [Stacks Tag 00Z6](https://stacks.math.columbia.edu/tag/00Z6) -/
CategoryTheory.GrothendieckTopology.instPartialOrder : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → PartialOrder (CategoryTheory.GrothendieckTopology C)
-- Mathlib.Data.Rel
/-- Composition of relation.

Note that this follows the `CategoryTheory` order of arguments.  -/
SetRel.comp : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → SetRel α β → SetRel β γ → SetRel α γ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t[a]? = none
-- Mathlib.CategoryTheory.Limits.VanKampen
_private.Mathlib.CategoryTheory.Limits.VanKampen.0.CategoryTheory.Limits.mapPair.match_1.splitter : (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) →
    (Unit → motive { as := CategoryTheory.Limits.WalkingPair.left }) →
      (Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }) → motive x
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.inhabited : {α : Type u} → Inhabited (Stream'.WSeq α)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A version of `AddMonoidHom.domRestrict` as a homomorphism.  -/
AddMonoidHom.domRestrictHom : {M : Type u_1} →
  [inst : AddZeroClass M] →
    {S : Type u_5} →
      [inst_1 : SetLike S M] →
        [inst_2 : AddSubmonoidClass S M] → (M' : S) → (A : Type u_6) → [inst_3 : AddCommMonoid A] → (M →+ A) →+ ↥M' →+ A
-- Mathlib.SetTheory.ZFC.PSet
PSet.Mem.congr_left : ∀ {x y : PSet.{u}}, x.Equiv y → ∀ {w : PSet.{u}}, x ∈ w ↔ y ∈ w
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centralizer_eq_top_iff_subset : ∀ {R : Type u_1} [inst : NonUnitalRing R] {s : Set R},
  NonUnitalSubring.centralizer s = ⊤ ↔ s ⊆ ↑(NonUnitalSubring.center R)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {l : Filter γ} {q : β → β → Prop} {u : γ → α}
  {v : α → β},
  (∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁)) → Filter.IsBoundedUnder r l u → Filter.IsBoundedUnder q l (v ∘ u)
-- Mathlib.Data.Prod.PProd
PProd.forall' : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop}, (∀ (x : α ×' β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a b
-- Mathlib.LinearAlgebra.FreeAlgebra
Algebra.rank_adjoin_le : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : Set S),
  Module.rank R ↥(Algebra.adjoin R s) ≤ max (Cardinal.mk ↑s) Cardinal.aleph0
-- Mathlib.RingTheory.Ideal.Over
Ideal.primesOver.liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] (p : Ideal A) {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B]
  (Q : ↑(p.primesOver B)), (↑Q).LiesOver p
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂) (f : (w.op.StructuredArrowRightwards g)ᵒᵖ),
  ((CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g).obj f).hom.right =
    (CategoryTheory.StructuredArrow.hom (Opposite.unop f)).left.unop
-- Mathlib.Analysis.Complex.Harmonic.Analytic
HarmonicAt.analyticAt : ∀ {f : ℂ → ℝ} {x : ℂ}, InnerProductSpace.HarmonicAt f x → AnalyticAt ℝ f x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv), ↑(f * g) = ↑f * ↑g
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β},
  (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.instDecidableEqPresburgerFunc.decEq : {a : ℕ} → (x x_1 : FirstOrder.presburgerFunc a) → Decidable (x = x_1)
-- Mathlib.RingTheory.Regular.RegularSequence
/-- Weakly regular sequences can be inductively characterized by:
* The empty sequence is weakly regular on any module.
* If `r` is regular on `M` and `rs` is a weakly regular sequence on `M⧸rM` then
  the sequence obtained from `rs` by prepending `r` is weakly regular on `M`.

This is the induction principle produced by the inductive definition above.
The motive will usually be valued in `Prop`, but `Sort*` works too.  -/
RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular : {R : Type u_1} →
  [inst : CommRing R] →
    {motive :
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsWeaklyRegular M rs → Sort u_7} →
      ((M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive M [] ⋯) →
        ({M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    (h1 : IsSMulRegular M r) →
                      (h2 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs) →
                        motive (QuotSMulTop r M) rs h2 → motive M (r :: rs) ⋯) →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → (h : RingTheory.Sequence.IsWeaklyRegular M rs) → motive M rs h
-- Mathlib.Logic.IsEmpty.Defs
Prod.isEmpty_left : ∀ {α : Type u_1} {β : Type u_2} [IsEmpty α], IsEmpty (α × β)
-- Lean.Util.Heartbeats
/-- Returns the remaining heartbeats available in this computation.  -/
Lean.getRemainingHeartbeats : Lean.CoreM ℕ
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₁.X₂ = (X ⊞ Y)
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_X_pow_char_sub_C : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R}, (Polynomial.X ^ p - Polynomial.C y).roots = p • {(frobeniusEquiv R p).symm y}
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.exists_norm_coe_lt_one : ∀ (K : Type u_1) [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K], ∃ x, 0 < ‖↑x‖ ∧ ‖↑x‖ < 1
-- Init.Data.Array.Lemmas
Array.decide_forall_mem : ∀ {α : Type u_1} {xs : Array α} {p : α → Prop} [inst : DecidablePred p],
  decide (∀ x ∈ xs, p x) = xs.all fun b => decide (p b)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_piMulSingle : ∀ {ι : Type u_6} [inst : DecidableEq ι] {M : ι → Type u_7} [inst_1 : (i : ι) → Monoid (M i)] (i : ι) (g : M i),
  orderOf (Pi.mulSingle i g) = orderOf g
-- Mathlib.Algebra.Ring.Defs
sub_one_mul : ∀ {α : Type u} [inst : NonAssocRing α] (a b : α), (a - 1) * b = a * b - b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddLeftCancelMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddLeftCancelMonoid Mᵃᵒᵖ], DomAddAct.instAddLeftCancelMonoidOfAddOpposite = inst
-- Init.System.IO
IO.FS.instOrdSystemTime.ord : IO.FS.SystemTime → IO.FS.SystemTime → Ordering
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.instInhabitedContent : {G : Type w} → [inst : TopologicalSpace G] → Inhabited (MeasureTheory.Content G)
-- ProofWidgets.Component.Panel.Basic
/-- Cursor position in the file at which the widget is being displayed.  -/
ProofWidgets.PanelWidgetProps.pos : ProofWidgets.PanelWidgetProps → Lean.Lsp.Position
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_modify_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : t.modify k f ≠ ∅}, (t.modify k f).minKey he = t.minKey ⋯
-- Mathlib.Data.List.Rotate
List.getElem_cyclicPermutations : ∀ {α : Type u} (l : List α) (n : ℕ) (h : n < l.cyclicPermutations.length), l.cyclicPermutations[n] = l.rotate n
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- The orthogonal complement of the inner derivations is a Lie submodule of all derivations.  -/
LieDerivation.IsKilling.rangeAdOrthogonal : (R : Type u_1) →
  (L : Type u_2) →
    [inst : Field R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubmodule R L (LieDerivation R L L)
-- Mathlib.Data.Set.Sups
Set.sups_sups_sups_comm : ∀ {α : Type u_2} [inst : SemilatticeSup α] (s t u v : Set α), s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A family of maps from `left (J.fst b)` to `right b`  -/
CategoryTheory.Limits.MulticospanIndex.fst : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MulticospanIndex J C) → (b : J.R) → self.left (J.fst b) ⟶ self.right b
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psum_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.psum σ R 0 = ↑(Fintype.card σ)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
/-- A type tag for `α` with `MeasurableSet` given by `NullMeasurableSet`.  -/
MeasureTheory.NullMeasurableSpace : (α : Type u_5) →
  [inst : MeasurableSpace α] → autoParam (MeasureTheory.Measure α) MeasureTheory.NullMeasurableSpace._auto_1 → Type u_5
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstPowInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.equalizer_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G] {U V : C} (f₁ f₂ : U ⟶ V),
  G.map f₁ = G.map f₂ → CategoryTheory.Sieve.equalizer f₁ f₂ ∈ J U
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.symm : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J},
  CategoryTheory.Zigzag j₁ j₂ → CategoryTheory.Zigzag j₂ j₁