mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isLimit_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.limit.isLimit F).lift c = CategoryTheory.Limits.limit.lift F c
-- Mathlib.Analysis.Complex.Norm
Complex.abs_im_div_norm_le_one : ∀ (z : ℂ), |z.im / ‖z‖| ≤ 1
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C}
  (h : Q.X.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (f.f.f n) h) =
    CategoryTheory.CategoryStruct.comp (f.f.f n) (CategoryTheory.CategoryStruct.comp (Q.p.f n) h)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- `Trie`s at the root based of the `Key`.  -/
Lean.Meta.RefinedDiscrTree.root : {α : Type} →
  Lean.Meta.RefinedDiscrTree α → Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.Injective.onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'},
  ϕ.Injective → ∀ {n : ℕ}, Function.Injective fun f => ϕ.onFunction f
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.innerHornInclusions_eq_iSup : SSet.innerHornInclusions = ⨆ n, CategoryTheory.MorphismProperty.ofHoms fun p => (SSet.horn (n + 2) ↑p).ι
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.smul_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} {R : Type u_5} [inst_3 : Ring R]
  [inst_4 : CategoryTheory.Preadditive C] [inst_5 : CategoryTheory.Linear R C] (r : R) {a b c : M}
  (α : CategoryTheory.ShiftedHom X Y a) (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c),
  (r • α).comp β h = r • α.comp β h
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_csSup' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  (e : α ≃o β) {s : Set α}, s.Nonempty → BddAbove s → e (sSup s) = sSup (⇑e '' s)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isoSc'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k),
  K.isoSc' i j k hi hk = K.isoSc' i j k hi hk
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sigmaSet_apply : ∀ {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) (x : (i : ι) × ↑(s i)),
  (Function.Embedding.sigmaSet h) x = ↑x.snd
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Build a set from a list which is already sorted. Performs no comparisons.

```
ofAscList [1, 2, 3] = {1, 2, 3}
ofAscList [3, 2, 1] = precondition violation
```  -/
Ordnode.ofAscList : {α : Type u_1} → List α → Ordnode α
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry : Type
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.comp_explicitCokernelπ_assoc : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y) {Z : SemiNormedGrp} (h : SemiNormedGrp.explicitCokernel f ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.compactSet K =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis ''
        closure (NumberField.mixedEmbedding.fundamentalCone.paramSet K) ∪
      {0}
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.HasFunctorialFactorization.nonempty_functorialFactorizationData : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [self : W₁.HasFunctorialFactorization W₂], Nonempty (W₁.FunctorialFactorizationData W₂)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.AddMon_tensor_zero_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero CategoryTheory.AddMonObj.zero))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optTypeForStructInst.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_mul_of_aestronglyMeasurable_left : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.Integrable (f * g) μ → MeasureTheory.Integrable g μ → μ[f * g | m] =ᵐ[μ] f * μ[g | m]
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.public : Lean.Elab.Visibility
-- Init.Data.SInt.Lemmas
Int64.left_eq_add : ∀ {a b : Int64}, a = a + b ↔ b = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source) and
open source is an `OpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.ofContinuousOpen : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialEquiv X Y) → ContinuousOn (↑e) e.source → IsOpenMap ↑e → IsOpen e.source → OpenPartialHomeomorph X Y
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_eq_get_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {h' : k ∈ m}, m.get k h' = (m.get? k).get ⋯
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_eq : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {z : α} {y : β}, l y = z ↔ ∀ (x : α), z ≤ x ↔ y ≤ u x
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_eq_of_L2 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 2 β), nndist x y = NNReal.sqrt (∑ i, nndist (x.ofLp i) (y.ofLp i) ^ 2)
-- Mathlib.CategoryTheory.Presentable.Basic
/-- The property of objects that are `κ`-presentable.  -/
CategoryTheory.isCardinalPresentable : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (κ : Cardinal.{w}) → [Fact κ.IsRegular] → CategoryTheory.ObjectProperty C
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁.default : Mathlib.Tactic.BicategoryLike.Atom₁
-- Mathlib.Geometry.Manifold.Instances.Icc
mfderivWithin_comp_projIcc_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {x y : ℝ}
  [h : Fact (x < y)] {f : ↑(Set.Icc x y) → M} {w : ↑(Set.Icc x y)},
  (mfderiv[Set.Icc x y] (f ∘ Set.projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_toContinuousLinearEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑↑e = ⇑e
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p : P), ((signedDist v) p) p = 0
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.decidableMemCenter : {M : Type u_1} →
  [inst : Semigroup M] → (a : M) → [Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ Subsemigroup.center M)
-- Init.Data.Range.Lemmas
Std.Legacy.Range.forIn_eq_forIn_range' : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (r : Std.Legacy.Range) (init : β)
  (f : ℕ → β → m (ForInStep β)), forIn r init f = forIn (List.range' r.start r.size r.step) init f
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the keys of a hash map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.Raw.keysIter : {α β : Type u} → Std.HashMap.Raw α β → Std.Iter α
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.global : Aesop.GlobalRuleSetMember → Aesop.LocalRuleSetMember
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mem_coe : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x : L}, x ∈ ↑L' ↔ x ∈ L'
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.formula2 : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.Y✝ S ^ 3 +
      ↑(FermatLastTheoremForThreeGen.Solution.u₄✝ S) * FermatLastTheoremForThreeGen.Solution.Z✝ S ^ 3 =
    ↑(FermatLastTheoremForThreeGen.Solution.u₅✝ S) *
      ((hζ.toInteger - 1) ^ (FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 1) *
          FermatLastTheoremForThreeGen.Solution.X✝ S) ^
        3
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- **Alias** of `Real.logDeriv_exp`. -/
Real.LogDeriv_exp : logDeriv Real.exp = 1
-- Mathlib.Probability.Process.Predictable
MeasureTheory.measurableSet_predictable_Ioi_prod : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  {𝓕 : MeasureTheory.Filtration ι m} {i : ι} {s : Set Ω}, MeasurableSet s → MeasurableSet (Set.Ioi i ×ˢ s)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] {E : Type u₃}
  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] [inst_7 : CategoryTheory.MonoidalCategory E]
  [inst_8 : CategoryTheory.BraidedCategory E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E}
  [inst_9 : F.LaxBraided] [inst_10 : G.LaxBraided] (X : CategoryTheory.CommMon C),
  (CategoryTheory.Functor.mapCommMonCompIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Algebra.Star.Pointwise
StarMemClass.star_coe_eq : ∀ {S : Type u_1} {α : Type u_2} [inst : InvolutiveStar α] [inst_1 : SetLike S α] [StarMemClass S α] (s : S),
  star ↑s = ↑s
-- Mathlib.Algebra.Group.Action.Opposite
op_vadd_add : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid α] [inst_1 : AddAction αᵃᵒᵖ β] (b : β) (a₁ a₂ : α),
  AddOpposite.op (a₁ + a₂) +ᵥ b = AddOpposite.op a₂ +ᵥ AddOpposite.op a₁ +ᵥ b
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.multipliable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {s : Set β}, Multipliable (f ∘ Subtype.val) → (Multipliable (f ∘ Subtype.val) ↔ Multipliable f)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.double_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁),
  (HomologicalComplex.double f hi₀₁).d i₀ i₁ =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₀ f hi₀₁).hom
      (CategoryTheory.CategoryStruct.comp f (HomologicalComplex.doubleXIso₁ f hi₀₁ h).inv)
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicHomAssociator : ∀ {X Y Z : SFinKer}, CategoryTheory.Deterministic (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.universalHom_apply : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_3}
  [inst_2 : Semiring T] (f : R →+* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R} {s : ↥S},
  (OreLocalization.universalHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r
-- Mathlib.Analysis.Convex.PathConnected
Path.segment_symm : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b : E), (Path.segment a b).symm = Path.segment b a
-- Mathlib.Topology.MetricSpace.Polish
/-- Given a Polish space, and countably many finer Polish topologies, there exists another Polish
topology which is finer than all of them.  -/
PolishSpace.exists_polishSpace_forall_le : ∀ {α : Type u_1} {ι : Type u_3} [Countable ι] [t : TopologicalSpace α] [p : PolishSpace α] (m : ι → TopologicalSpace α),
  (∀ (n : ι), m n ≤ t) → (∀ (n : ι), PolishSpace α) → ∃ t', (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α
-- Init.Data.UInt.Basic
instMinUSize : Min USize
-- Mathlib.Algebra.Homology.DerivedCategory.Linear
DerivedCategory.instLinearShiftFunctorInt : ∀ (R : Type t) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : HasDerivedCategory C] (n : ℤ),
  CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (DerivedCategory C) n)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.cooper c_1 → c = c_1
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- The Cesaro average of a converging sequence converges to the same limit.  -/
Filter.Tendsto.cesaro_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {u : ℕ → E} {l : E},
  Filter.Tendsto u Filter.atTop (nhds l) →
    Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds l)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.associator_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q R : C),
  (CategoryTheory.Limits.coprod.associator P Q R).hom =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.neg_equiv_neg : ∀ {α : 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
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- **Alias** of `LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero`.

---

The **Cayley-Hamilton Theorem** for f.g. modules over arbitrary rings states that for each
`R`-endomorphism `φ` of an `R`-module `M` generated by `n` elements such that `φ(M) ≤ I • M`
for some ideal `I`, there exist some `aᵢ ∈ Iⁱ` such that `φⁿ + a₁ φⁿ⁻¹ + ⋯ + aₙ = 0`.

This is the version in [Matsumura 2.1][matsumura1987], which is stronger than those in
[Eisenbud 4.3][Eisenbud1995] and [Atiyah-Macdonald 2.4][atiyah-macdonald].
 -/
LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul : ∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  (f : Module.End R M) (I : Ideal R),
  LinearMap.range f ≤ I • ⊤ →
    ∃ p,
      p.Monic ∧
        p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableDiv_of_mul_inv : ∀ (G : Type u_2) [inst : MeasurableSpace G] [inst_1 : DivInvMonoid G] [MeasurableMul G] [MeasurableInv G],
  MeasurableDiv G
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_add_iff_of_nonpos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    f ≤ᵐ[μ] 0 →
      g ≤ᵐ[μ] 0 → (MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrRightₗ_symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] [inst_4 : AddCommMonoid Z] [inst_5 : Module R Z] (e : Y ≃ₗ[R] Z)
  (a : LocallyConstant X Z) (a_1 : X), ((LocallyConstant.congrRightₗ R e).symm a) a_1 = e.symm (a a_1)
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.bot : ∀ {G : Type u_3} [inst : AddGroup G], ⊥.FG
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailOption : Lean.Order.MonadTail Option
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop_atBot : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} [inst_2 : Preorder β],
  Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ i, ∀ (a : α), i ≤ a → f a ≤ b
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_add_C : ∀ {R : Type u} [inst : Semiring R] (c : R), Polynomial.derivative (Polynomial.X + Polynomial.C c) = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Iic_castSucc : ∀ {n : ℕ} (i : Fin n), Fin.castSucc ⁻¹' Set.Iic i.castSucc = Set.Iic i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The pushout cocone reconstructed using `PushoutCocone.mk` from a pushout cocone that is a
colimit, is also a colimit.  -/
CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk t.inl t.inr ⋯)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.coe_toDual_self : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (i : ι), b.toDual (b i) = b.coord i
-- Mathlib.Condensed.Discrete.LocallyConstant
LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop : ∀ (S : LightProfinite) (p : ↑S.toTop → Prop),
  CompHausLike.HasProp (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) (Subtype p)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiSup_of_not_bddAbove : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α},
  ¬BddAbove (Set.range fun i => f ↑i ⋯) → ⨆ i, ⨆ (h : p i), f i h = sSup ∅
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instAddZeroClass : {M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → AddZeroClass (AddMonoid.Coprod M N)
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.measurable_fun_prod : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, Measurable (f i)) → Measurable fun a => ∏ i ∈ s, f i a
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.isMultiplicative_finsetProd : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} (f : ι → ArithmeticFunction R) (s : Finset ι),
  (∀ i ∈ s, (f i).IsMultiplicative) → (∏ i ∈ s, f i).IsMultiplicative
-- Mathlib.Data.WSeq.Relation
/-- If two sequences are equivalent, then they have the same values and
the same computational behavior (i.e. if one loops forever then so does
the other), although they may differ in the number of `think`s needed to
arrive at the answer.  -/
Stream'.WSeq.Equiv : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α → Prop
-- Mathlib.Order.Filter.AtTopBot.Archimedean
atTop_hasCountableBasis_of_archimedean : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.atTop.HasCountableBasis (fun x => True) fun n => Set.Ici ↑n
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.eq_divMonomial_single : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [IsLeftCancelAdd R] {i : σ} {p q r : MvPolynomial σ R},
  p = MvPolynomial.X i * q + r → (∀ n ∈ r.support, n i = 0) → q = p.divMonomial fun₀ | i => 1
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Returns `some (r₁, c, r₂)` if `s₁ == r₁.union c` and `s₂ == r₂.union c`

It assumes `s₁` and `s₂` are sorted
 -/
Lean.Grind.AC.Seq.superposeAC? : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Option (Lean.Grind.AC.Seq × Lean.Grind.AC.Seq × Lean.Grind.AC.Seq)
-- Mathlib.RingTheory.Bezout
Function.Surjective.isBezout : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → ∀ [IsBezout R], IsBezout S
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.structuralIsoOfExpr_horizontalComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f₁ g₁ f₂ g₂ : C}
  (η : f₁ ⟶ g₁) (η' : f₁ ≅ g₁),
  η'.hom = η →
    ∀ (θ : f₂ ⟶ g₂) (θ' : f₂ ≅ g₂),
      θ'.hom = θ →
        (CategoryTheory.MonoidalCategory.tensorIso η' θ').hom = CategoryTheory.MonoidalCategoryStruct.tensorHom η θ
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mk : (Unit → Lean.MessageData) →
  Lean.Elab.Do.DoElabM Lean.Expr →
    (Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) →
      (Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr) →
        (Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont) → Lean.Elab.Do.ControlStack
-- Init.Data.List.MinMax
List.max.eq_1 : ∀ {α : Type u} [inst : Max α] (a : α) (tail : List α) (x_2 : a :: tail ≠ []),
  (a :: tail).max x_2 = List.foldl max a tail