mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctor_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) (I₁ : Type u_7)
  (I₂ : Type u_8) (I₃ : Type u_9) (X₁ : CategoryTheory.GradedObject I₁ C₁),
  (CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁ =
    CategoryTheory.GradedObject.mapTrifunctorObj F X₁ I₂ I₃
-- Mathlib.Computability.PartrecBasis
Nat.rfindOpt.eq_1 : ∀ {α : Type u_1} (f : ℕ → Option α), Nat.rfindOpt f = (Nat.rfind fun n => ↑(some (f n).isSome)).bind fun n => ↑(f n)
-- Mathlib.Algebra.Group.Defs
/-- A mixin for cancellative addition.  -/
IsCancelAdd : (G : Type u) → [Add G] → Prop
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
SimpleGraph.Subgraph.IsMatching.exists_of_universalVerts : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {s : Set V},
  Disjoint G.universalVerts s →
    s.ncard ≤ G.universalVerts.ncard → ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.σ_smul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (x y : S), P.σ x • y = x * y
-- Init.Data.List.Pairwise
List.pairwise_flatMap : ∀ {β : Type u_1} {α : Type u_2} {R : β → β → Prop} {l : List α} {f : α → List β},
  List.Pairwise R (List.flatMap f l) ↔
    (∀ a ∈ l, List.Pairwise R (f a)) ∧ List.Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.congr : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : LE E],
  MeasureTheory.Submartingale f ℱ μ →
    MeasureTheory.StronglyAdapted ℱ g → (∀ (t : ι), f t =ᵐ[μ] g t) → MeasureTheory.Submartingale g ℱ μ
-- Lean.Elab.Tactic.Ext
/-- Ensures that the given structure has an ext theorem, without validating any pre-existing theorems.
Returns the name of the ext theorem.

See `Lean.Elab.Tactic.Ext.withExtHyps` for an explanation of the `flat` argument.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.realizeExtTheorem : Lean.Name → Bool → Lean.Elab.TermElabM Lean.Name
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.remainingBytes_le : ∀ {it : String.Legacy.Iterator}, it.Valid → it.remainingBytes ≤ it.s.utf8ByteSize
-- Mathlib.Algebra.Group.Basic
div_mul_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = c / b * a
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.endsWith_char_eq_endsWith_beq : ∀ {c : Char} {s : String.Slice}, s.endsWith c = s.endsWith fun x => x == c
-- Mathlib.Data.Vector.Basic
List.Vector.empty_toList_eq_ff : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α (n + 1)), v.toList.isEmpty = false
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_id : ∀ {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 : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E}, F.whiskerLeft (CategoryTheory.NatTrans.id G) = CategoryTheory.NatTrans.id (F.comp G)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.relevantArgs : Lean.Meta.FunInd.Call → Lean.Expr
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- An isomorphism between isocrystals respects the Frobenius map.

Notation `M ≃ᶠⁱ [p, k]` in the `Isocrystal` namespace.  -/
WittVector.IsocrystalEquiv : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            (V : Type u_2) →
              [inst_4 : AddCommGroup V] →
                [WittVector.Isocrystal p k V] →
                  (V₂ : Type u_3) → [inst_6 : AddCommGroup V₂] → [WittVector.Isocrystal p k V₂] → Type (max u_2 u_3)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Build an isomorphism in the category `CommGrpCat` from a `MulEquiv`
between `CommGroup`s.  -/
MulEquiv.toCommGrpIso : {X Y : CommGrpCat} → ↑X ≃* ↑Y → (X ≅ Y)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instStar : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Star β] → Star (MeasureTheory.SimpleFunc α β)
-- Mathlib.Data.Fintype.Card
Fintype.card_eq_zero : ∀ {α : Type u_1} [inst : Fintype α] [IsEmpty α], Fintype.card α = 0
-- Aesop.Stats.Basic
Aesop.ForwardStateStats.mk.sizeOf_spec : ∀ (ruleStateStats : Array Aesop.ForwardRuleStateStats),
  sizeOf { ruleStateStats := ruleStateStats } = 1 + sizeOf ruleStateStats
-- Batteries.Data.List.Basic
/-- Computes the difference of `l₁` and `l₂`, by removing each element in `l₂` from `l₁`.  -/
List.diff : {α : Type u_1} → [BEq α] → List α → List α → List α
-- Init.Data.Array.Extract
Array.extract_succ_right : ∀ {α : Type u_1} {as : Array α} {i j : ℕ},
  i < j + 1 → ∀ (h : j < as.size), as.extract i (j + 1) = (as.extract i j).push as[j]
-- Mathlib.CategoryTheory.Galois.Equivalence
/-- The induced functor from `C` to the category of finite, discrete `Aut F`-sets.  -/
CategoryTheory.PreGaloisCategory.functorToContAction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → CategoryTheory.Functor C (ContAction FintypeCat (CategoryTheory.Aut F))
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.pow : ∀ {R : Type u_1} [inst : Semiring R] {A : Type u_8} {B : Type u_9} [inst_1 : AddMonoid A] [inst_2 : AddMonoid B]
  [inst_3 : LinearOrder B] [inst_4 : OrderBot B] [AddLeftStrictMono B] [AddRightStrictMono B] {D : A → B}
  {p : AddMonoidAlgebra R A} {n : ℕ},
  (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
    Function.Injective D → AddMonoidAlgebra.Monic D p → AddMonoidAlgebra.Monic D (p ^ n)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey?_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.filter (fun p => f p.fst p.snd) l) =
      (Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValue x l ⋯)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_rightUnitor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`.  -/
Ideal.Quotient.mk : {R : Type u} → [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → R →+* R ⧸ I
-- Mathlib.Geometry.Manifold.Submersion
/-- Being a submersion at `x` is a local property.  -/
Manifold.isLocalSourceTargetProperty_submmersionAtProp : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : TopologicalSpace N], Manifold.IsLocalSourceTargetProperty (Manifold.SubmersionAtProp F I J M N)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.homeomorphOfUnique_symm_apply : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X]
  [inst_3 : Unique Y] (a : Y), (Homeomorph.homeomorphOfUnique X Y).symm a = default
-- Mathlib.Topology.Order
generateFrom_iInter_of_generateFrom_eq_self : ∀ {α : Type u} {ι : Sort v} (f : ι → Set (Set α)),
  (∀ (i : ι), {s | IsOpen s} = f i) →
    TopologicalSpace.generateFrom (⋂ i, f i) = ⨆ i, TopologicalSpace.generateFrom (f i)
-- Mathlib.Order.Birkhoff
LatticeHom.birkhoffFinset_injective : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred],
  Function.Injective ⇑LatticeHom.birkhoffFinset
-- Mathlib.Data.Set.Function
Set.InvOn.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g₁ g₂ : Equiv.Perm α}
  {s t : Set α},
  Set.InvOn (⇑g₁) (⇑g₂) s t →
    Set.InvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_functor_obj : ∀ {J : Type u_1} {K : Type u_2} (a : CategoryTheory.Discrete (J ⊕ K)),
  CategoryTheory.Discrete.sumEquiv.functor.obj a =
    match a.as with
    | Sum.inl j => Sum.inl { as := j }
    | Sum.inr k => Sum.inr { as := k }
-- Init.Data.String.Slice
String.Slice.instToFormat : Std.ToFormat String.Slice
-- ProofWidgets.Presentation.Expr
ProofWidgets.instRpcEncodableExprPresentationProps : Lean.Server.RpcEncodable ProofWidgets.ExprPresentationProps
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.Away.tensorRight : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R)
  (A : Type u_9) [inst_3 : CommSemiring A] [inst_4 : Algebra R A] [IsLocalization.Away r A],
  IsLocalization.Away ((algebraMap R S) r) (TensorProduct R A S)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + i = m) CategoryTheory.SimplicialObject.δ₀Iter_succ._auto_1),
  X.δ₀Iter (i + 1) ⋯ = CategoryTheory.CategoryStruct.comp (X.δ 0) (X.δ₀Iter i h)
-- Lean.Environment
/-- `constNames` contains all constant names in `constants`.
This information is redundant. It is equal to `constants.map fun c => c.name`,
but it improves the performance of `importModules`. `perf` reports that 12% of the
runtime was being spent on `ConstantInfo.name` when importing a file containing only `import Lean`
 -/
Lean.ModuleData.constNames : Lean.ModuleData → Array Lean.Name
-- Mathlib.Data.ENat.Basic
/-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`.  -/
ENat.toNat : ℕ∞ → ℕ
-- Mathlib.Order.Lex
/-- A recursor for `Colex`. Use as `induction x`.  -/
Colex.rec : {α : Type u_1} → {β : Colex α → Sort u_2} → ((a : α) → β (toColex a)) → (a : Colex α) → β a
-- Std.Http.Data.Method
Std.Http.Method.updateredirectref.sizeOf_spec : sizeOf Std.Http.Method.updateredirectref = 1
-- Lean.Log
/-- Log a named error warning using the given message data. The position is provided by `ref`.

Note: Use the macro `logNamedWarningAt`, which validates error names, instead of calling this function
directly.
 -/
Lean.logNamedWarningAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Syntax → Lean.Name → Lean.MessageData → m Unit
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Auxiliary definition for `HasCokernels SemiNormedGrp₁`.  -/
SemiNormedGrp₁.cokernelLift : {X Y : SemiNormedGrp₁} →
  (f : X ⟶ Y) → (s : CategoryTheory.Limits.CokernelCofork f) → (SemiNormedGrp₁.cokernelCocone f).pt ⟶ s.pt
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_shiftLeft : ∀ (a b : UInt8), (a <<< b).toUInt16 = a.toUInt16 <<< (b % 8).toUInt16 % 256
-- Mathlib.CategoryTheory.Core
/-- A natural isomorphism of functors induces a natural isomorphism between their cores.  -/
CategoryTheory.Iso.core : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {F G : CategoryTheory.Functor C D} → (F ≅ G) → (F.core ≅ G.core)
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.IsIrreducible.mk : ∀ {α : Type u_1} {mα : MeasurableSpace α} {φ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α α},
  (∀ ⦃A : Set α⦄, MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ n, ((κ ^ n) a) A > 0) →
    ProbabilityTheory.Kernel.IsIrreducible φ κ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey? k = none
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → Bool} {k : α},
  (Std.ExtHashMap.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix_eq_apply : ∀ {α : Sort u_2} {C : α → Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] {R : α → α → Prop}
  {F : (a : α) → ((a' : α) → R a' a → C a') → C a} {a : α},
  WellFounded R → WellFounded.partialExtrinsicFix R F a = F a fun a' x => WellFounded.partialExtrinsicFix R F a'
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, (s.dropEndWhile pat).dropEndWhile pat = s.dropEndWhile pat
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.zero_lt_pairingIn_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [inst_10 : Module S M] [IsScalarTower S R M]
  [IsStrictOrderedRing S], 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i
-- Init.Data.String.Lemmas.Order
String.Pos.next_le_iff_lt : ∀ {s : String} {p q : s.Pos} {h : p ≠ s.endPos}, p.next h ≤ q ↔ p < q
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖ = ↑(Finset.univ.sup fun i => ∑ j, ‖A i j‖₊)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- Real part of an element in quadratic algebra  -/
QuadraticAlgebra.re : {R : Type u} → {a b : R} → QuadraticAlgebra R a b → R
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Auxiliary definition for `Adjunction.comp`.  -/
CategoryTheory.Bicategory.Adjunction.compUnit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f₁ : a ⟶ b} →
        {g₁ : b ⟶ a} →
          {f₂ : b ⟶ c} →
            {g₂ : c ⟶ b} →
              CategoryTheory.Bicategory.Adjunction f₁ g₁ →
                CategoryTheory.Bicategory.Adjunction f₂ g₂ →
                  (CategoryTheory.CategoryStruct.id a ⟶
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f₁ f₂)
                      (CategoryTheory.CategoryStruct.comp g₂ g₁))
-- Lean.Data.PPContext
Lean.PPContext.mk.injEq : ∀ (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options)
  (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (env_1 : Lean.Environment) (mctx_1 : Lean.MetavarContext)
  (lctx_1 : Lean.LocalContext) (opts_1 : Lean.Options) (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl),
  ({ env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := currNamespace, openDecls := openDecls } =
      { env := env_1, mctx := mctx_1, lctx := lctx_1, opts := opts_1, currNamespace := currNamespace_1,
        openDecls := openDecls_1 }) =
    (env = env_1 ∧
      mctx = mctx_1 ∧ lctx = lctx_1 ∧ opts = opts_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1)
-- Mathlib.RingTheory.Smooth.StandardSmooth
/-- An `R`-algebra `S` is called standard smooth, if there
exists a submersive presentation.
 -/
Algebra.IsStandardSmooth : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.mem_zeroRootSubalgebra : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (x : L),
  x ∈ LieAlgebra.zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ k, ((LieModule.toEnd R (↥H) L) y ^ k) x = 0
-- Init.Grind.Ring.Basic
/-- Every element satisfies `x ^ p = x`.  -/
Lean.Grind.PowIdentity.pow_eq : ∀ {α : Type u} {inst : Lean.Grind.CommSemiring α} {p : outParam ℕ} [self : Lean.Grind.PowIdentity α p] (x : α),
  x ^ p = x
-- Mathlib.Order.PrimeSeparator
Lattice.mem_ideal_sup_principal : ∀ {α : Type u_1} [inst : Lattice α] (a b : α) (J : Order.Ideal α), b ∈ J ⊔ Order.Ideal.principal a ↔ ∃ j ∈ J, b ≤ j ⊔ a
-- Mathlib.Data.List.Destutter
List.isChain_destutter' : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α) (a : α), List.IsChain R (List.destutter' R a l)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Composition of closed immersions is a closed immersion.  -/
AlgebraicGeometry.IsClosedImmersion.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsClosedImmersion f]
  [AlgebraicGeometry.IsClosedImmersion g], AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- The principal ultrafilter associated to a point `x`.  -/
Ultrafilter.instPure : Pure Ultrafilter
-- Init.Data.List.MinMax
List.max?_cons : ∀ {α : Type u_1} {x : α} [inst : Max α] [Std.Associative max] {xs : List α},
  (x :: xs).max? = some (xs.max?.elim x (max x))
-- Mathlib.SetTheory.Ordinal.Notation
/-- `mulNat o n` is the ordinal notation for `o * n`.  -/
ONote.mulNat : ONote → ℕ → ONote
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- `eval(F)` restricted to the original category (via `incl`) is the original copresheaf `F`.  -/
CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : Type u₁) →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_2 : CategoryTheory.Limits.HasCoproducts A] →
          (CategoryTheory.Limits.FormalCoproduct.eval C A).comp
              ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Limits.FormalCoproduct C) A).obj
                (CategoryTheory.Limits.FormalCoproduct.incl C)) ≅
            CategoryTheory.Functor.id (CategoryTheory.Functor C A)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.epi_iff_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂),
  CategoryTheory.Epi f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))
-- Mathlib.Data.Rel
SetRel.right_subset_comp : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β}, S ⊆ R.comp S
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.algebraMap_eq_one_iff : ∀ {R : Type u1} [inst : CommRing R] (M : Type u2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : R),
  (algebraMap R (ExteriorAlgebra R M)) x = 1 ↔ x = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If all elements of a `Finset` satisfy the predicate `p`, a sum
over `s.subtype p` equals that sum over `s`.  -/
Finset.sum_subtype_of_mem : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] (f : ι → M) {p : ι → Prop}
  [inst_1 : DecidablePred p], (∀ x ∈ s, p x) → ∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s, f x
-- Mathlib.FieldTheory.Normal.Defs
/-- The group homomorphism given by restricting an algebra isomorphism to itself
is the identity map.  -/
AlgEquiv.restrictNormalHom_id : ∀ (F : Type u_6) (K : Type u_7) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : Normal F K],
  AlgEquiv.restrictNormalHom K = MonoidHom.id Gal(K/F)
-- Lean.Data.LBool
Lean.LBool.undef : Lean.LBool
-- Init.Data.Fin.Lemmas
Fin.val_one : ∀ (n : ℕ), ↑1 = 1
-- Std.Http.Server.Connection
Std.Http.Server.instToStringRemoteAddr : ToString Std.Http.Server.RemoteAddr
-- Init.Data.List.Lemmas
List.head_of_mem_head? : ∀ {α : Type u_1} {l : List α} {x : α} (hx : x ∈ l.head?), l.head ⋯ = x
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_zero : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  LieAlgebra.derivedSeriesOfIdeal R L 0 I = I
-- Mathlib.RingTheory.PicardGroup
CommRing.relPic_eq_top : ∀ (R : Type u) [inst : CommSemiring R] (A : Type u_5) [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [Subsingleton (CommRing.Pic A)], CommRing.relPic R A = ⊤
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- If `C` is idempotent complete, the functor `toKaroubi : C ⥤ Karoubi C` is an equivalence.  -/
CategoryTheory.Idempotents.toKaroubi_isEquivalence : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsIdempotentComplete C],
  (CategoryTheory.Idempotents.toKaroubi C).IsEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Y] {Z : C}
  (h : Y ⨯ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag Y) h)
-- Lean.Meta.Basic
Lean.Meta.mkFreshTypeMVar : optParam Lean.MetavarKind Lean.MetavarKind.natural → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM Lean.Expr
-- Mathlib.Probability.Process.Filtration
/-- The constant filtration which is equal to `m` for all `i : ι`.  -/
MeasureTheory.Filtration.const : {Ω : Type u_1} →
  (ι : Type u_2) →
    {m : MeasurableSpace Ω} → [inst : Preorder ι] → (m' : MeasurableSpace Ω) → m' ≤ m → MeasureTheory.Filtration ι m
-- Lean.Declaration
Lean.RecursorRule.mk.inj : ∀ {ctor : Lean.Name} {nfields : ℕ} {rhs : Lean.Expr} {ctor_1 : Lean.Name} {nfields_1 : ℕ} {rhs_1 : Lean.Expr},
  { ctor := ctor, nfields := nfields, rhs := rhs } = { ctor := ctor_1, nfields := nfields_1, rhs := rhs_1 } →
    ctor = ctor_1 ∧ nfields = nfields_1 ∧ rhs = rhs_1
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.mem_ball_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] {a : M} {c : FiniteArchimedeanClass M},
  a ∈ FiniteArchimedeanClass.ball K c ↔ ∀ (h : a ≠ 0), c < FiniteArchimedeanClass.mk a h
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x : α),
  ⇑e ⁻¹' Set.Ioi (e x) = Set.Ioi x
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.linearIndepOn_toRatVec : ∀ {ι : Type u_3} {s : Set (ι → ℕ)}, LinearIndepOn ℕ id s → LinearIndepOn ℚ (⇑toRatVec✝) s