mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Antichain
/-- An antichain `s` is a maximal antichain if there does not exists an antichain strictly including
`s`.  -/
IsMaxAntichain : {α : Type u_1} → (α → α → Prop) → Set α → Prop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.mk.inj : ∀ {expr : Lean.Expr} {i num : ℕ} {source : Lean.Meta.Grind.SplitSource} {expr_1 : Lean.Expr} {i_1 num_1 : ℕ}
  {source_1 : Lean.Meta.Grind.SplitSource},
  { expr := expr, i := i, num := num, source := source } =
      { expr := expr_1, i := i_1, num := num_1, source := source_1 } →
    expr = expr_1 ∧ i = i_1 ∧ num = num_1 ∧ source = source_1
-- Init.Data.Int.LemmasAux
Int.min_max_distrib_right : ∀ (a b c : ℤ), min (max a b) c = max (min a c) (min b c)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `simp`-normal form of `toFun_eq_coe`.  -/
MulEquiv.coe_toEquiv : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), ⇑↑f = ⇑f
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_mono_assoc_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {g h : Z ⟶ Y}
  {W : C} {k l : W ⟶ Z},
  CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp g f) =
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.CategoryStruct.comp h f) ↔
    CategoryTheory.CategoryStruct.comp k g = CategoryTheory.CategoryStruct.comp l h
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → FunLike (BoundedOrderHom α β) α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {l : List (α × β)}, (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toOne_one : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜],
  1 = GradedAlgHom.id R 𝒜
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.re_extendRCLike_apply`. -/
RCLike.re_extendTo𝕜ₗ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (g : StrongDual ℝ F) (x : F), RCLike.re (g.extendRCLike x) = g x
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.since? : Lean.Linter.DeprecationEntry → Option String
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.rid_tmul : ∀ {R : Type uR} (S : Type uS) {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (r : R) (a : A),
  (Algebra.TensorProduct.rid R S A) (a ⊗ₜ[R] r) = r • a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a b : α}
  (hab : cmp a b = Ordering.eq) {h' : a ∈ t}, t[a] = t[b]
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Int.trailingZeros_aux_succ : ∀ {k : ℕ} {i : ℤ} {hi : i ≠ 0} {hk : i.natAbs ≤ k} {acc : ℕ},
  Int.trailingZeros.aux k i hi hk (acc + 1) = Int.trailingZeros.aux k i hi hk acc + 1
-- Mathlib.Algebra.Category.Grp.Adjunctions
MonCat.units_obj_coe : ∀ (R : MonCat), ↑(MonCat.units.obj R) = (↑R)ˣ
-- Mathlib.Algebra.Group.Conj
IsConj.setoid.eq_1 : ∀ (α : Type u_1) [inst : Monoid α], IsConj.setoid α = { r := IsConj, iseqv := ⋯ }
-- Mathlib.Algebra.WithConv
WithConv.ofConv_eq_zero : ∀ {A : Type u_2} [inst : AddMonoid A] {x : WithConv A}, x.ofConv = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_neg_left`. -/
MonovaryOn.neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → AntivaryOn (-f) g s
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofAdd_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.total : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Total s], Std.Total r
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearEquiv.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E ≃L[𝕜] F)
  (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `isCofinal_of_isCofinal_iUnion`. -/
Cardinal.unbounded_of_unbounded_iUnion : ∀ {α ι : Type u_1} [inst : LinearOrder α] {s : ι → Set α},
  IsCofinal (⋃ i, s i) → Cardinal.mk ι < Order.cof α → ∃ i, IsCofinal (s i)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Bornology.IsBounded (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instSetLike : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → SetLike (ConvexCone R M) M
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.anyM_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n]
  [inst_6 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] {it : Std.IterM m β} {f : β → n β'}
  {p : β' → n (ULift.{w, 0} Bool)},
  Std.IterM.anyM p (Std.IterM.mapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        p __do_lift)
      (Std.IterM.mapM pure it)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_le_max_of_aleph0_le_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a * b ≤ max a b
-- Init.Tactics
/-- Assuming `x` is a variable in the local context with an inductive type,
`cases x` splits the main goal, producing one goal for each constructor of the
inductive type, in which the target is replaced by a general instance of that constructor.
If the type of an element in the local context depends on `x`,
that element is reverted and reintroduced afterward,
so that the case split affects that hypothesis as well.
`cases` detects unreachable cases and closes them automatically.

For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`,
`cases n` produces one goal with hypothesis `h : P 0` and target `Q 0`,
and one goal with hypothesis `h : P (Nat.succ a)` and target `Q (Nat.succ a)`.
Here the name `a` is chosen automatically and is not accessible.
You can use `with` to provide the variables names for each constructor.
- `cases e`, where `e` is an expression instead of a variable, generalizes `e` in the goal,
  and then cases on the resulting variable.
- Given `as : List α`, `cases as with | nil => tac₁ | cons a as' => tac₂`,
  uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case,
  and `a` and `as'` are used as names for the new variables introduced.
- `cases h : e`, where `e` is a variable or an expression,
  performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each goal,
  where `...` is the constructor instance for that particular case.
 -/
Lean.Parser.Tactic.cases : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_le_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G}, A.subConst B ≤ ↑B.card
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_push_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α (n + 1)} {b : β} {f : (i : ℕ) → α → i < n + 1 → β}
  {ys : Vector β n},
  xs.mapFinIdx f = ys.push b ↔ ∃ zs a, xs = zs.push a ∧ (zs.mapFinIdx fun i a h => f i a ⋯) = ys ∧ b = f n a ⋯
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_zsmul : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ι → G) (n : ℤ), ⇑f ∘ (n • g) = n • ⇑f ∘ g
-- Init.Core
instInhabitedThunk : {α : Type u_1} → [Inhabited α] → Inhabited (Thunk α)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_smul : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {l : Type u_7} [inst : Fintype n] [inst_1 : Monoid R]
  [inst_2 : AddCommMonoid A] [inst_3 : Mul A] [inst_4 : DistribMulAction R A] [SMulCommClass R A A]
  (M : CStarMatrix m n A) (a : R) (N : CStarMatrix n l A), M * a • N = a • (M * N)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_self' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (y : ↥S), f.mk' (↑y) y = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.instBraidedPullback : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → {X R : C} → {f : R ⟶ X} → (CategoryTheory.Over.pullback f).Braided
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Two cycles of a permutation commute.  -/
Equiv.Perm.cycleFactorsFinset_mem_commute : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  (↑f.cycleFactorsFinset).Pairwise Commute
-- Mathlib.Tactic.Translate.Reorder
/-- The list of disjoint cycles that represents the permutation.  -/
Mathlib.Tactic.Translate.ArgReorder.perm : Mathlib.Tactic.Translate.ArgReorder → Mathlib.Tactic.Translate.Permutation
-- Mathlib.SetTheory.Cardinal.Order
/-- `Cardinal.lift` as an `InitialSeg`.  -/
Cardinal.liftInitialSeg : Cardinal.{u} ≤i Cardinal.{max u v}
-- Mathlib.Analysis.Normed.Operator.Mul
/-- The norm of `lsmul` equals 1 in any nontrivial normed group.

This is `ContinuousLinearMap.opNorm_lsmul_le` as an equality.  -/
ContinuousLinearMap.opNorm_lsmul : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E],
  ‖ContinuousLinearMap.lsmul 𝕜 R‖ = 1
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_neg : ∀ {α : Type u} {x : FreeCommRing α} {s : Set α}, x.IsSupported s → (-x).IsSupported s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.mul : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β}
  [inst : TopologicalSpace β] [inst_1 : MulZeroClass β] [ContinuousMul β],
  MeasureTheory.FinStronglyMeasurable f μ →
    MeasureTheory.FinStronglyMeasurable g μ → MeasureTheory.FinStronglyMeasurable (f * g) μ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instIsArtinianSubtypeMem : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  [IsArtinian R L], IsArtinian R ↥L'
-- Mathlib.Analysis.Normed.Group.Basic
norm_neg : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ‖-a‖ = ‖a‖
-- Init.System.IO
IO.FS.Stream.mk.injEq : ∀ (flush : IO Unit) (read : USize → IO ByteArray) (write : ByteArray → IO Unit) (getLine : IO String)
  (putStr : String → IO Unit) (isTty : BaseIO Bool) (flush_1 : IO Unit) (read_1 : USize → IO ByteArray)
  (write_1 : ByteArray → IO Unit) (getLine_1 : IO String) (putStr_1 : String → IO Unit) (isTty_1 : BaseIO Bool),
  ({ flush := flush, read := read, write := write, getLine := getLine, putStr := putStr, isTty := isTty } =
      { flush := flush_1, read := read_1, write := write_1, getLine := getLine_1, putStr := putStr_1,
        isTty := isTty_1 }) =
    (flush = flush_1 ∧ read = read_1 ∧ write = write_1 ∧ getLine = getLine_1 ∧ putStr = putStr_1 ∧ isTty = isTty_1)
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Mathlib.Meta.FunProp.Origin.fvar fvarId) = 1 + sizeOf fvarId
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_additive : ∀ {α : Type u}, Cardinal.mk (Additive α) = Cardinal.mk α
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.addBlocks : Lean.VersoModuleDocs.DocContext✝ →
  Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) → Except String Lean.VersoModuleDocs.DocContext✝
-- Mathlib.Computability.Reduce
OneOneEquiv.le_congr_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, OneOneEquiv p q → (p ≤₁ r ↔ q ≤₁ r)
-- Batteries.Tactic.Lint.Simp
/-- Checks whether two expressions are equal for the simplifier. That is,
they are reducibly-definitional equal, and they have the same head symbol.  -/
Batteries.Tactic.Lint.isSimpEq : Lean.Expr → Lean.Expr → optParam Bool true → Lean.MetaM Bool
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α},
  Std.PRange.UpwardEnumerable.LE a b ↔ Std.PRange.UpwardEnumerable.LE (f.toFun a) (f.toFun b)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [Monad m] [inst : Std.Do.WP m ps] (f : {β : Type u} → m β → m β)
  {α : Type u} (x : OptionT m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp (f x.run)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)⦄
    MonadFunctor.monadMap (fun {β} => f) x ⦃Q⦄
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprElimInfo.repr : Lean.Meta.ElimInfo → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
/-- Standard basis vectors are eigenvectors of any associated diagonal linear operator.  -/
hasEigenvector_toLin'_diagonal : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [Nontrivial R]
  (d : n → R) (i : n), Module.End.HasEigenvector (Matrix.toLin' (Matrix.diagonal d)) (d i) ((Pi.basisFun R n) i)
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- **Alias** of `CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom`. -/
CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H),
  (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).hom = ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_ker : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Hom.ker f).map g = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Data.Position
Lean.Position.instToFormat : Std.ToFormat Lean.Position
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_union : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s ∪ t)ᶜ = sᶜ ∩ tᶜ
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_X₁ : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms], (S.map F).X₁ = F.obj S.X₁
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.toMon_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C), A.toMon.X = A.X
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `z - (toZMod z : ℤ_[p])` is contained in the maximal ideal of `ℤ_[p]`, for every `z : ℤ_[p]`.

The coercion from `ZMod p` to `ℤ_[p]` is `ZMod.cast`,
which coerces `ZMod p` into arbitrary rings.
This is unfortunate, but a consequence of the fact that we allow `ZMod p`
to coerce to rings of arbitrary characteristic, instead of only rings of characteristic `p`.
This coercion is only a ring homomorphism if it coerces into a ring whose characteristic divides
`p`. While this is not the case here we can still make use of the coercion.
 -/
PadicInt.toZMod_spec : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), x - (PadicInt.toZMod x).cast ∈ IsLocalRing.maximalIdeal ℤ_[p]
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.isIso_liftExtend_f_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ) {i' : ι'} {i : ι},
  e.f i = i' → (CategoryTheory.IsIso ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.IsIso (φ.f i))
-- Mathlib.Analysis.Seminorm
Seminorm.neg_mem_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, -x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r
-- Mathlib.Tactic.MinImports
/-- `getAllImports cmd id` takes a `Syntax` input `cmd` and returns the `NameSet` of all the
module names that are implied by
* the `SyntaxNodeKinds`,
* the attributes of `cmd` (if there are any),
* the identifiers contained in `cmd`,
* if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`.

The argument `id` is expected to be an identifier.
It is used either for the internally generated name of a "nameless" `instance` or when parsing
an identifier representing the name of a declaration.
 -/
Mathlib.Command.MinImports.getAllImports : Lean.Syntax → Lean.Syntax → optParam Bool false → Lean.Elab.Command.CommandElabM Lean.NameSet
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey?_modify_eq_minKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).minKey? = t.minKey?
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.MapsTo.neg : ∀ {α : Type u_2} {β : Type u_3} [inst : InvolutiveNeg β] {A : Set α} {B : Set β} {f : α → β},
  Set.MapsTo f A B → Set.MapsTo (-f) A (-B)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.Iso.minDegree_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj] [inst_2 : Fintype W] [inst_3 : DecidableRel G'.Adj] (f : G ≃g G'),
  G.minDegree = G'.minDegree
-- Lean.Expr
Lean.Expr.forallE.sizeOf_spec : ∀ (binderName : Lean.Name) (binderType body : Lean.Expr) (binderInfo : Lean.BinderInfo),
  sizeOf (Lean.Expr.forallE binderName binderType body binderInfo) =
    1 + sizeOf binderName + sizeOf binderType + sizeOf body + sizeOf binderInfo
-- Init.Data.Range.Polymorphic.PRange
/-- `a<...=b` is the range of elements greater than `a` and less than or equal to `b`.
See also `Std.Roc`.
 -/
Std.«term_<...=_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram'.mk.sizeOf_spec : ∀ (diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton), sizeOf { diagram := diagram } = 1 + sizeOf diagram
-- Mathlib.CategoryTheory.Products.Basic
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`.  -/
CategoryTheory.whiskeringLeftCompEvaluation : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (a : A) →
                ((CategoryTheory.Functor.whiskeringLeft A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) ≅
                  (CategoryTheory.evaluation B C).obj (F.obj a)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.free_obj : ∀ (C : CategoryTheory.Cat), ↑(CategoryTheory.Grpd.free.obj C) = CategoryTheory.FreeGroupoid ↑C
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  Ideal.associatesEquivIsPrincipal R = Ideal.associatesEquivIsPrincipal R
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [LocallyCompactSpace α]
  [inst_3 : NonUnitalSemiring β] [inst_4 : IsTopologicalSemiring β], IsTopologicalSemiring C(α, β)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges.eq_1 : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  Rel.interedges r s t = {e ∈ s ×ˢ t | r e.1 e.2}
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_comp_fst : ∀ (C : Type u₁) [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂)
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y Z : C × D} (f : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
  (g : (Y.1 ⟶ Z.1) × (Y.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1
-- Lean.DocString.Parser
/-- Items like *  -/
Lean.Doc.Parser.UnorderedListType.asterisk : Lean.Doc.Parser.UnorderedListType
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.symm : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [ContinuousSub M], Submodule.IsTopCompl p q → Submodule.IsTopCompl q p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.rightUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s)
  {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t),
  (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).inv =
    Q.lift
      (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X)
        (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))
-- Lean.Elab.Tactic.Omega.Core
/-- `Problem.assumptions[i]` generates a proof that `s.sat' coeffs atoms`
 -/
Lean.Elab.Tactic.Omega.Justification.assumption : (s : Lean.Omega.Constraint) → (x : Lean.Omega.Coeffs) → ℕ → Lean.Elab.Tactic.Omega.Justification s x
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜}, HasDerivAt f f' x → HasDerivWithinAt f f' s x