mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DeclModifiers
Lean.Elab.ExpandDeclIdResult.mk.injEq : ∀ (shortName declName : Lean.Name) (levelNames : List Lean.Name)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (shortName_1 declName_1 : Lean.Name)
  (levelNames_1 : List Lean.Name) (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)),
  ({ shortName := shortName, declName := declName, levelNames := levelNames, docString? := docString? } =
      { shortName := shortName_1, declName := declName_1, levelNames := levelNames_1, docString? := docString?_1 }) =
    (shortName = shortName_1 ∧ declName = declName_1 ∧ levelNames = levelNames_1 ∧ docString? = docString?_1)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_associator_hom_assoc : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {E : Type u_5} [inst_4 : CategoryTheory.Category.{v_5, u_5} E]
  (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D E)
  {Z : CategoryTheory.Functor (CategoryTheory.Join A B) (CategoryTheory.Join A E)}
  (h : CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) (F.comp (G.comp H)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (F.associator G H).hom) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A (F.comp G) H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapCompRight A F G).hom
          (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).associator
              (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) G)
              (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H)).hom
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).whiskerLeft
              (CategoryTheory.Join.mapCompRight A G H).inv)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F (G.comp H)).inv h))))
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.stronglyAdapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.StronglyAdapted f u
-- Lean.Elab.Binders
/-- Generalize the value from the expected type when elaborating the body.  -/
Lean.Elab.Term.LetConfig.generalize : Lean.Elab.Term.LetConfig → Bool
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- See `Module.finrank_zero_iff` for the stronger version with `IsTorsionFree R M`.  -/
Module.finrank_eq_zero_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M], Module.finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.coequifibered_unop_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered (CategoryTheory.NatTrans.unop α) ↔ CategoryTheory.NatTrans.Equifibered α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.value : Lean.Lsp.CompletionItemKind
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.le_basis_iff : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α}, l.HasBasis p s → l'.HasBasis p' s' → (l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i')
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f +ᵥ g) μ
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift'_apply_dp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : M), f (0, m) = 1)
  (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m))
  (hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m))
  (hf_add :
    ∀ (n : ℕ) (u v : M),
      f (n, u + v) =
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          match x with
          | (k, l) => f (k, u) * f (l, v))
  (n : ℕ) (m : M), (DividedPowerAlgebra.lift' hf_zero hf_smul hf_mul hf_add) (DividedPowerAlgebra.dp R n m) = f (n, m)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero : ∀ (z : UpperHalfPlane) (m : ℤ),
  ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap'_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂).op =
    CategoryTheory.CategoryStruct.comp h₂.iso.inv.op
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.ShortComplex.opMap φ) h₂.op h₁.op) h₁.iso.hom.op)
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : ↥s),
  (EuclideanGeometry.orthogonalProjection s) ↑p = p
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.mk.injEq : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier)
  (contentChanges : Array Lean.Lsp.TextDocumentContentChangeEvent)
  (textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier)
  (contentChanges_1 : Array Lean.Lsp.TextDocumentContentChangeEvent),
  ({ textDocument := textDocument, contentChanges := contentChanges } =
      { textDocument := textDocument_1, contentChanges := contentChanges_1 }) =
    (textDocument = textDocument_1 ∧ contentChanges = contentChanges_1)
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.goal.sizeOf_spec : sizeOf Mathlib.Linter.Flexible.Stained.goal✝ = 1
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
/-- Choose an arbitrary simple subobject of a non-zero Artinian object.  -/
CategoryTheory.simpleSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] →
        {X : C} → [CategoryTheory.IsArtinianObject X] → ¬CategoryTheory.Limits.IsZero X → C
-- Mathlib.Order.Category.BoolAlg
/-- The equivalence between `BoolAlg` and itself induced by `OrderDual` both ways.  -/
BoolAlg.dualEquiv : BoolAlg ≌ BoolAlg
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.sheafHom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  (J : CategoryTheory.GrothendieckTopology C) [inst_1 : F.IsPrestack J] {S : C}
  (M N : ↑(F.obj { as := Opposite.op S })), (F.sheafHom J M N).obj = F.presheafHom M N
-- Batteries.Data.Char.Basic
Char.toNat_not_surrogate : ∀ (c : Char), ¬(Char.minSurrogate ≤ c.toNat ∧ c.toNat ≤ Char.maxSurrogate)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.Raw.ofList l cmp).get! k' = cast ⋯ v
-- Lean.Elab.DocString
Lean.Doc.CodeBlockSuggestion.mk.inj : ∀ {name : Lean.Name} {args moreInfo : Option String} {name_1 : Lean.Name} {args_1 moreInfo_1 : Option String},
  { name := name, args := args, moreInfo := moreInfo } = { name := name_1, args := args_1, moreInfo := moreInfo_1 } →
    name = name_1 ∧ args = args_1 ∧ moreInfo = moreInfo_1
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_or : ∀ (a b : BitVec 64), Int64.ofBitVec (a ||| b) = Int64.ofBitVec a ||| Int64.ofBitVec b
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.noConfusionType : Sort v✝ → Std.Time.Reason✝ → Std.Time.Reason✝ → Sort v✝
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
of `s`, and is preserved under addition and multiplication, then `p` holds for all elements
of the closure of `s`.  -/
Subsemiring.closure_induction : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {p : (x : R) → x ∈ Subsemiring.closure s → Prop},
  (∀ (x : R) (hx : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      p 1 ⋯ →
        (∀ (x y : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s), p x hx → p y hy → p (x + y) ⋯) →
          (∀ (x y : R) (hx : x ∈ Subsemiring.closure s) (hy : y ∈ Subsemiring.closure s),
              p x hx → p y hy → p (x * y) ⋯) →
            ∀ {x : R} (hx : x ∈ Subsemiring.closure s), p x hx
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The pushout cocone built from the pushout coprojections is a pushout.  -/
CategoryTheory.Limits.pushoutIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPushout f g] →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.inl f g)
                (CategoryTheory.Limits.pushout.inr f g) ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.rightOp : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered α → CategoryTheory.NatTrans.Equifibered (CategoryTheory.NatTrans.rightOp α)
-- Mathlib.AlgebraicGeometry.Spec
/-- Spec, as a contravariant functor from commutative rings to sheafed spaces.
 -/
AlgebraicGeometry.Spec.toSheafedSpace : CategoryTheory.Functor CommRingCatᵒᵖ (AlgebraicGeometry.SheafedSpace CommRingCat)
-- Init.SizeOf
ULift.up.sizeOf_spec : ∀ {α : Type s} [inst : SizeOf α] (down : α), sizeOf { down := down } = 1 + sizeOf down
-- Mathlib.GroupTheory.Coprod.Basic
/-- An `AddEquiv` version of `AddMonoid.Coprod.swap`.  -/
AddEquiv.coprodComm : (M : Type u_1) →
  (N : Type u_2) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → AddMonoid.Coprod M N ≃+ AddMonoid.Coprod N M
-- Mathlib.Topology.Order
continuous_iff_coinduced_le : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β},
  Continuous f ↔ TopologicalSpace.coinduced f t₁ ≤ t₂
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames : Type
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instSMulDistribMulActionHomId : {M : Type u_1} →
  {N : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : AddMonoid A] →
          [inst_1 : DistribSMul M A] →
            [inst_2 : Monoid N] →
              [inst_3 : AddMonoid B] →
                [inst_4 : DistribMulAction N A] →
                  [SMulCommClass M N A] → [inst_6 : DistribMulAction N B] → SMul Mᵈᵐᵃ (A →+[N] B)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.commute_X_pow : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), Commute (Polynomial.X ^ n) p
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup : {G : Type u} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] → [SeparatelyContinuousAdd G] → SemilatticeSup (OpenNormalAddSubgroup G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k' (Std.Internal.List.alterKey k f l) =
      if (k == k') = true then (f (Std.Internal.List.getValueCast? k l)).isSome else Std.Internal.List.containsKey k' l
-- Mathlib.Topology.Algebra.Monoid
/-- The continuous map `fun y => y + x`  -/
ContinuousMap.addRight : {X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Add X] → [SeparatelyContinuousAdd X] → X → C(X, X)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_swap_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (x y : α), (Equiv.swap x y).support = {x, y} ↔ x ≠ y
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAddEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → A ≃+ B
-- Mathlib.Order.Concept
Concept.extent_ofIsExtent : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) (hs : Order.IsExtent r s),
  (Concept.ofIsExtent r s hs).extent = s
-- Mathlib.Algebra.Module.Presentation.Cokernel
_private.Mathlib.Algebra.Module.Presentation.Cokernel.0.Module.Presentation.cokernelRelations.match_1.eq_1 : ∀ {A : Type u_4} [inst : Ring A] {M₂ : Type u_5} [inst_1 : AddCommGroup M₂] [inst_2 : Module A M₂]
  (pres₂ : Module.Presentation A M₂) {ι : Type u_2} (motive : pres₂.R ⊕ ι → Sort u_6) (r : pres₂.R)
  (h_1 : (r : pres₂.R) → motive (Sum.inl r)) (h_2 : (i : ι) → motive (Sum.inr i)),
  (match Sum.inl r with
    | Sum.inl r => h_1 r
    | Sum.inr i => h_2 i) =
    h_1 r
-- Init.Data.BitVec.Lemmas
/-- If the current width `w` is larger than the extended width `v`,
then the value when interpreted as an integer is truncated,
and we compute a modulo by `2^v`.
 -/
BitVec.toInt_signExtend_eq_toNat_bmod_of_le : ∀ {w v : ℕ} {x : BitVec w}, v ≤ w → (BitVec.signExtend v x).toInt = (↑x.toNat).bmod (2 ^ v)
-- Mathlib.Condensed.Light.Basic
/-- **Alias** of `LightCondensed.id_hom`. -/
LightCondensed.id_val : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] (X : LightCondensed C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
-- Mathlib.Topology.Compactification.StoneCech
/-- The range of `pure : α → Ultrafilter α` is dense in `Ultrafilter α`.  -/
denseRange_pure : ∀ {α : Type u}, DenseRange pure
-- Mathlib.RingTheory.Coprime.Basic
/-- `IsCoprime` is not a useful definition if an inverse is available.  -/
Semifield.isCoprime_iff : ∀ {R : Type u_1} [inst : Semifield R] {m n : R}, IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instT2Space : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F],
  T2Space (E [⋀^ι]→L[𝕜] F)
-- Init.Data.Nat.Lemmas
Nat.mul_eq_zero : ∀ {m n : ℕ}, n * m = 0 ↔ n = 0 ∨ m = 0
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_equivMapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : CommMonoid N] (f : α ≃ β)
  (l : α →₀ M) (g : β → M → N), (Finsupp.equivMapDomain f l).prod g = l.prod fun a m => g (f a) m
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_comp : ∀ {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z),
  BddDistLat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (BddDistLat.Hom.hom g).comp (BddDistLat.Hom.hom f)
-- Init.Core
LawfulBEq.toReflBEq : ∀ {α : Type u} {inst : BEq α} [self : LawfulBEq α], ReflBEq α
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.hasBadParamDep? : Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.toSubring_top : ∀ {K : Type u} [inst : Field K], ⊤.toSubring = ⊤
-- Mathlib.RingTheory.RegularLocalRing.Defs
isRegularLocalRing_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  IsRegularLocalRing R ↔ ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) = ringKrullDim R
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.descToInjective.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {J : C} (f f_1 : S.X₂ ⟶ J) (e_f : f = f_1)
  [inst_2 : CategoryTheory.Injective J] (hf : CategoryTheory.CategoryStruct.comp S.f f = 0),
  hS.descToInjective f hf = hS.descToInjective f_1 ⋯
-- Init.PropLemmas
or_or_distrib_right : ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.multiset_sum_sum : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M}
  {h : α → M → Multiset N}, (f.sum h).sum = f.sum fun a b => (h a b).sum
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimitRecOn_succ_of_not_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a)
  (hb : ¬IsMax b), Order.isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_inv_hom_id' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.inv f))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id W))
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- If `f₀ : X ⟶ Y` is homotopic to `f₁` relative to a cylinder `P`,
and `f₁` is homotopic to `f₂` relative to a good cylinder `P'`,
then `f₀` is homotopic to `f₂` relative to the cylinder `P.trans P'`
when `X` is cofibrant.  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.ModelCategory C] →
        {P : HomotopicalAlgebra.Cylinder X} →
          [inst_2 : HomotopicalAlgebra.IsCofibrant X] →
            {f₀ f₁ f₂ : X ⟶ Y} →
              P.LeftHomotopy f₀ f₁ →
                {P' : HomotopicalAlgebra.Cylinder X} →
                  [inst_3 : P'.IsGood] →
                    P'.LeftHomotopy f₁ f₂ →
                      [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] → (P.trans P').LeftHomotopy f₀ f₂
-- Mathlib.Topology.UniformSpace.Basic
/-- Uniform space structure on `ULift α`.  -/
ULift.uniformSpace : {α : Type ua} → [UniformSpace α] → UniformSpace (ULift.{u_2, ua} α)
-- Mathlib.Data.Finset.Sum
Finset.toRight_inter : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u ∩ v).toRight = u.toRight ∩ v.toRight
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The middle object of the fork diagram of the Stacks entry.
The difference between this and `Equalizer.FirstObj P (ofArrows X π)` arises if the family of
arrows `π` contains duplicates. The `Presieve.ofArrows` doesn't see those.
 -/
CategoryTheory.Equalizer.Presieve.Arrows.FirstObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type w) → {I : Type t} → [Small.{w, t} I] → (I → C) → Type w
-- Mathlib.Algebra.Group.End
/-- `Multiplicative G` and `G` have isomorphic automorphism groups.  -/
MulAutMultiplicative : (G : Type u_3) → [inst : AddGroup G] → MulAut (Multiplicative G) ≃* Multiplicative (AddAut G)
-- Mathlib.Data.List.Rotate
List.rotate_reverse : ∀ {α : Type u} (l : List α) (n : ℕ), l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.isClosed_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsClosed (Metric.closedBall x ε)
-- Mathlib.Algebra.DirectSum.Finsupp
finsuppLEquivDirectSum_symm_lof : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι : Type u_1)
  [inst_3 : DecidableEq ι] (i : ι) (m : M),
  (finsuppLEquivDirectSum R M ι).symm ((DirectSum.lof R ι (fun x => M) i) m) = fun₀ | i => m
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a_1 : a ⟶ b) {X Y : Opposite.unop a ⟶ x}
  (x_1 : X ⟶ Y),
  ((CategoryTheory.Bicategory.yoneda.obj x).map a_1).toFunctor.map x_1 =
    CategoryTheory.Bicategory.whiskerLeft a_1.unop x_1
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
  Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atTop (nhds 1)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopLeft` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `x ∈ s`.  -/
MonoidHom.ofClosureMEqTopLeft : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        {s : Set M} →
          (f : M → N) → Submonoid.closure s = ⊤ → f 1 = 1 → (∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y) → M →* N
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mk.congr_simp : ∀ {α : Type u_6} [inst : LE α] (toProd toProd_1 : α × α) (e_toProd : toProd = toProd_1)
  (fst_le_snd : toProd.1 ≤ toProd.2),
  { toProd := toProd, fst_le_snd := fst_le_snd } = { toProd := toProd_1, fst_le_snd := ⋯ }
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_sdiff_self`. -/
Set.inter_diff_self : ∀ {α : Type u_1} (a b : Set α), a ∩ (b \ a) = ∅
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.inverse_apply : ∀ {A : Type u_10} {B : Type u_11} [inst : AddMonoid A] [inst_1 : AddMonoid B] (f : A →+ B) (g : B → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : B), (f.inverse g h₁ h₂) a = g a