mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroMorphisms.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [zero : (X Y : C) → Zero (X ⟶ Y)] →
      autoParam (∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0)
          CategoryTheory.Limits.HasZeroMorphisms.comp_zero._autoParam →
        autoParam (∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0)
            CategoryTheory.Limits.HasZeroMorphisms.zero_comp._autoParam →
          CategoryTheory.Limits.HasZeroMorphisms C
-- Init.Data.Nat.Lemmas
Nat.mod_two_bne_one : ∀ {a : ℕ}, (a % 2 != 1) = (a % 2 == 0)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- An involutive matrix which can transfer results between `RootPairing.GeckConstruction.e` and
`RootPairing.GeckConstruction.f`.  -/
RootPairing.GeckConstruction.ω : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} → (b : P.Base) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Given a point in the affine span from which all the points are
equidistant, that point is the circumcenter.  -/
Affine.Simplex.eq_circumcenter_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
  p ∈ affineSpan ℝ (Set.range s.points) → ∀ {r : ℝ}, (∀ (i : Fin (n + 1)), dist (s.points i) p = r) → p = s.circumcenter
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.mk.injEq : ∀ (state state_1 : Std.Mutex (Option ByteArray)), ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.edgeSet_deleteEdges : ∀ {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)), (G.deleteEdges s).edgeSet = G.edgeSet \ s
-- Mathlib.Control.Traversable.Lemmas
Traversable.traverse_eq_map_id' : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {β γ : Type u} (f : β → γ),
  traverse (pure ∘ f) = pure ∘ Functor.map f
-- Mathlib.CategoryTheory.Action.Basic
/-- Auxiliary definition for `functorCategoryEquivalence`.  -/
Action.FunctorCategoryEquivalence.unitIso : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] →
        CategoryTheory.Functor.id (Action V G) ≅
          Action.FunctorCategoryEquivalence.functor.comp Action.FunctorCategoryEquivalence.inverse
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `E(L) = E[L]`.  -/
IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K),
  Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L →
    (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of a measurable function is smaller than its mean.  -/
MeasureTheory.exists_le_laverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → AEMeasurable f μ → ∃ x, f x ≤ ⨍⁻ (a : α), f a ∂μ
-- Mathlib.Algebra.Group.Defs
CancelCommMonoid.toIsLeftCancelMul : ∀ {M : Type u} [self : CancelCommMonoid M], IsLeftCancelMul M
-- Lean.Environment
/-- Loads the module data from the given file names. The files must be (a prefix of) the result of a
`saveModuleDataParts` call.
 -/
Lean.readModuleDataParts : Array System.FilePath → IO (Array (Lean.ModuleData × Lean.CompactedRegion))
-- Aesop.Forward.State
/-- Update the forward state. This applies any previously enqueued changes to
all rule states, potentially generating new complete matches in the process.
If a phase is given, only rules from that phase are updated.  -/
Aesop.ForwardState.update : Lean.MVarId →
  Aesop.ForwardState → Option Aesop.PhaseName → Aesop.BaseM (Aesop.ForwardState × Array Aesop.ForwardRuleMatch)
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanlMUnsafe : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → {n : ℕ} → [Monad m] → (β → α → m β) → β → Vector α n → m (Vector β (n + 1))
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The element of `alternatingGroup α` induced by an element
of `alternatingGroup s`, when `s : Finset α`.  -/
alternatingGroup.ofSubtype : {α : Type u_1} →
  [inst : Fintype α] → [inst_1 : DecidableEq α] → (s : Finset α) → ↥(alternatingGroup ↥s) →* ↥(alternatingGroup α)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  {X Y : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} (f : X ⟶ Y) (X_1 : C₁)
  (X_2 : C₂) (X_3 : C₃),
  ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).map f).app X_1).app X_2).app X_3 =
    ((f.app (F₁.obj X_1)).app (F₂.obj X_2)).app (F₃.obj X_3)
-- Init.MetaTypes
Lean.Meta.Simp.instBEqConfig : BEq Lean.Meta.Simp.Config
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_eq_ciSup : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β),
  ‖f‖₊ = ⨆ i, ‖f.ofLp i‖₊
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.coe_completeGraph : ∀ {α : Type u_5} {β : Type u_6} (f : α ↪ β), ⇑(SimpleGraph.Embedding.completeGraph f) = ⇑f
-- Init.Data.Array.Lemmas
List.filter_toArray : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, Array.filter p l.toArray = (List.filter p l).toArray
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔
    0 ≤ s.radius ∧ q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context : Type
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddCommGrpCat.tensorObj_eq : ∀ (G H : AddCommGrpCat), CategoryTheory.MonoidalCategoryStruct.tensorObj G H = AddCommGrpCat.of (↑G × ↑H)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.denselyOrdered_range_nnnorm : ∀ (α : Type u_2) [inst : DenselyNormedField α], DenselyOrdered ↑(Set.range nnnorm)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.foldl : ∀ {α : Type u_1} (f : α → Char → α) (init : α) {s : Substring.Raw},
  s.Valid → Substring.Raw.Legacy.foldl f init s = List.foldl f init s.toString.toList
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  (t.truncGE n).map ((t.truncGEπ n).app X) = (t.truncGEπ n).app ((t.truncGE n).obj X)
-- Lean.Environment
Lean.instInhabitedConstantKind.default : Lean.ConstantKind
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below : {R : Type u_1} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      {r : R → R → Prop} →
        {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} → {a a_1 : R} → RingConGen.Rel r a a_1 → Prop
-- Mathlib.RingTheory.Invariant.Galois
/-- A variant of `Algebra.isInvariant_of_isGalois`, replacing `Gal(L/K)` by `Aut(B/A)`.  -/
Algebra.isInvariant_of_isGalois' : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Field K] [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [IsFractionRing A K]
  [IsFractionRing B L] [inst_8 : Algebra A B] [inst_9 : Algebra K L] [inst_10 : Algebra A L] [IsScalarTower A K L]
  [IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsGalois K L],
  Algebra.IsInvariant A B (B ≃ₐ[A] B)
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.mk.injEq : ∀ (expr type : Lean.Expr) (modified : Bool) (expr_1 type_1 : Lean.Expr) (modified_1 : Bool),
  ({ expr := expr, type := type, modified := modified } = { expr := expr_1, type := type_1, modified := modified_1 }) =
    (expr = expr_1 ∧ type = type_1 ∧ modified = modified_1)
-- Mathlib.Algebra.DirectSum.Decomposition
/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
to a direct sum of components. This is the canonical spelling of the `decompose'` field.  -/
DirectSum.decompose : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) → [DirectSum.Decomposition ℳ] → M ≃ DirectSum ι fun i => ↥(ℳ i)
-- Mathlib.RingTheory.RootsOfUnity.Basic
disjoint_rootsOfUnity_of_coprime : ∀ {M : Type u_1} [inst : CommMonoid M] {m n : ℕ}, m.Coprime n → Disjoint (rootsOfUnity m M) (rootsOfUnity n M)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_one : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M}, Localization.mk 1 1 = 1
-- Mathlib.Data.Finset.Grade
Multiset.isAtom_iff : ∀ {α : Type u_1} {s : Multiset α}, IsAtom s ↔ ∃ a, s = {a}
-- Init.Data.Array.Find
/-- If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
Moreover, no earlier array in `xs` has an element satisfying `p`.
 -/
Array.find?_flatten_eq_some_iff : ∀ {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} {a : α},
  Array.find? p xss.flatten = some a ↔
    p a = true ∧
      ∃ as ys zs bs,
        xss = as.push (ys.push a ++ zs) ++ bs ∧ (∀ ws ∈ as, ∀ x ∈ ws, (!p x) = true) ∧ ∀ x ∈ ys, (!p x) = true
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.lift.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f f_1 : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤)
  (e_f : f = f_1) (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m),
  AdicCompletion.lift I f h = AdicCompletion.lift I f_1 ⋯
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.termH : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.IsHamiltonian.of_unique : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α] [Unique α], G.IsHamiltonian
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism (in `Type`) between
morphisms from a specified object `W` to the limit object,
and cones with cone point `W`.
 -/
CategoryTheory.Limits.limit.homIso : {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] →
            (W : C) → ULift.{u₁, v} (W ⟶ CategoryTheory.Limits.limit F) ≅ F.cones.obj (Opposite.op W)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.hom_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C},
  Function.Surjective CategoryTheory.ConcreteCategory.hom
-- Mathlib.Data.Seq.Computation
/-- Corecursor constructor for `corec`  -/
Computation.Corec.f : {α : Type u} → {β : Type v} → (β → α ⊕ β) → α ⊕ β → Option α × (α ⊕ β)
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concat_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → ∀ {t : ↑(Set.Icc a c)} (ht : ↑t ≤ b), (f.concat g) t = f ⟨↑t, ⋯⟩
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypicOfType.linearEquiv_finsupp : ∀ {R : Type u_2} {M : Type u} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S] [IsSemisimpleModule R M],
  IsIsotypicOfType R M S → ∃ ι, Nonempty (M ≃ₗ[R] ι →₀ S)
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.toFilterBasis : {G : Type u} → {inst : Group G} → [self : GroupFilterBasis G] → FilterBasis G
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l toInsert : List ((a : α) × β a)},
  l.length ≤ (Std.Internal.List.insertList l toInsert).length
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.mem_maximalIdeal_iff : ∀ (K : Type u) [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
  {a : ↥v.valuationSubring}, a ∈ IsLocalRing.maximalIdeal ↥v.valuationSubring ↔ v ↑a < 1
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.splitterMatchInfo : Lean.Meta.Match.MatchEqns → Lean.Meta.MatcherInfo
-- Mathlib.Data.ENNReal.Basic
ENNReal.instIsOrderedMonoid : IsOrderedMonoid ENNReal
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {H₃ : CategoryTheory.Functor C₃ D₃}
  (eL : C₂ ≌ C₃) (eR : D₂ ≌ D₃) (w' : H₂.comp eR.functor ≅ eL.functor.comp H₃),
  (w.vComp w'.hom).GuitartExact ↔ w.GuitartExact
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.modifiers : Lean.Elab.PreDefinition → Lean.Elab.Modifiers
-- Mathlib.CategoryTheory.Types.Basic
equivEquivIso_hom : ∀ {X Y : Type u} (e : X ≃ Y), equivEquivIso e = e.toIso
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (t : Set α),
  s.sdiff t = { carrier := ↑s \ ↑(upperClosure t), lower' := ⋯ }
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [inst_3 : J.HasSheafCompose F] [J.PreservesSheafification F],
  CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.pow : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [ContinuousMul α], Multipliable f L → ∀ (n : ℕ), Multipliable (fun x => f x ^ n) L
-- Mathlib.RingTheory.Jacobson.Ring
/-- A ring `R` is Jacobson if and only if for every prime ideal `I`,
`I` can be written as the infimum of some collection of maximal ideals.
Allowing ⊤ in the set `M` of maximal ideals is equivalent, but makes some proofs cleaner.  -/
isJacobsonRing_iff_sInf_maximal : ∀ {R : Type u_1} [inst : CommRing R],
  IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_eq_toArray_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toArray = it.toIterM.toArray.run
-- Std.Time.Date.Unit.Day
/-- `Offset` represents an offset in days. It is defined as an `Int` with a base unit of 86400
(the number of seconds in a day).
 -/
Std.Time.Day.Offset : Type
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {hc : t.max he ∈ t}, t.get (t.max he) hc = t.max he
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piCurry_apply : ∀ {ι : Type u_6} {κ : ι → Type u_7} (X : (i : ι) → κ i → Type u_8)
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)] (f : (x : (i : ι) × κ i) → X x.fst x.snd) (x : ι) (y : κ x),
  (MeasurableEquiv.piCurry X) f x y = Sigma.curry f x y
-- Mathlib.Condensed.Limits
instHasLimitsCondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.Limits.HasLimits (CondensedMod R)
-- Aesop.Rule
Aesop.UnsafeRule : Type
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.orbitRel_addSubgroup_le : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (H : AddSubgroup G),
  AddAction.orbitRel (↥H) α ≤ AddAction.orbitRel G α
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.Flat.mono : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] {C₁ C₂ : ConvexCone R G}, C₁ ≤ C₂ → C₁.Flat → C₂.Flat
-- Init.Data.String.Length
String.Internal.size_toArray : ∀ {b : String}, (String.Internal.toArray b).size = b.length
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).obj A =
    CategoryTheory.LaxBraidedFunctor.of (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ Submodule.comap f q}, p.mapQ q f h ∘ₛₗ p.mkQ = q.mkQ ∘ₛₗ f
-- Mathlib.Order.SuccPred.Limit
SuccOrder.prelimitRecOn_succ : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : WellFoundedLT α]
  (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a) [inst_3 : NoMaxOrder α]
  (b : α),
  SuccOrder.prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯ (SuccOrder.prelimitRecOn b succ isSuccPrelimit)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone
point `Y`.  -/
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {X : C} → F.cocones.CorepresentableBy X → {Y : C} → (X ⟶ Y) → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If we preserve limits of some arbitrary size, then we preserve all finite limits.  -/
CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LT ι] [Std.Trichotomous fun x1 x2 => x1 < x2] [hι : WellFoundedGT ι]
  [inst_2 : (i : ι) → AddMonoid (α i)] [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)]
  [hα : ∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Lex (Π₀ (i : ι), α i))
-- Lean.Server.Requests
Lean.Server.ServerRequestResponse : Type → Type
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_one : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.ofVal 1 = 1
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.LinearMap.dp_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [IsScalarTower R S N] {n : ℕ} {r : R} {a : M},
  DividedPowerAlgebra.dp S n (f (r • a)) = r ^ n • DividedPowerAlgebra.dp S n (f a)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The definition of the class group does not depend on the choice of field of fractions.  -/
ClassGroup.equiv : {R : Type u_1} →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsFractionRing R K] →
            [inst_4 : IsDomain R] →
              ClassGroup R ≃* (FractionalIdeal (nonZeroDivisors R) K)ˣ ⧸ (toPrincipalIdeal R K).range
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- Morphisms `Y ⟶ M` act on morphisms `Y ⟶ X` via the internal scalar multiplication.  -/
CategoryTheory.Hom.instSMulHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.MonObj M] → {X : C} → [CategoryTheory.ModObj M X] → (Y : C) → SMul (Y ⟶ M) (Y ⟶ X)
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id : ∀ (V : Type u_2) [inst : CategoryTheory.ReflQuiver V] (X : V),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).map (CategoryTheory.ReflQuiver.id X).toPath =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Cat.FreeRefl.quotientFunctor V).obj X)
-- Mathlib.Algebra.Ring.Pi
Pi.evalRingHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → NonAssocSemiring (f i)] (i : I) (g : (i : I) → f i),
  (Pi.evalRingHom f i) g = g i