mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The structure `IsPresentationCore` can be shrunk to a lower universe.  -/
Module.Relations.Solution.IsPresentationCore.down : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} → solution.IsPresentationCore → solution.IsPresentationCore
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : (CategoryTheory.ShortComplex C)ᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.opFunctor C).map φ = CategoryTheory.ShortComplex.opMap φ.unop
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : CategoryTheory.Limits.HasCokernel S.f],
  (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_ne_zero_iff_ne_and_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.instNonUnitalAlgEquivClass : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B], NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app app_1 : (X : C) → F.obj X ≅ G.obj X) (e_app : app = app_1)
  (naturality :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
        CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)),
  CategoryTheory.NatIso.ofComponents app naturality = CategoryTheory.NatIso.ofComponents app_1 ⋯
-- Mathlib.Analysis.Calculus.Taylor
taylorWithinEval.eq_1 : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ),
  taylorWithinEval f n s x₀ x = (PolynomialModule.eval x) (taylorWithin f n s x₀)
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntUSizeUintNumBits : Lean.Grind.ToInt USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- Expand the definition of `proximity f a` in case where `a₀ = ⊤`.
 -/
ValueDistribution.proximity_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E},
  ValueDistribution.proximity f ⊤ = Real.circleAverage (fun x => ‖f x‖.posLog) 0
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- A map into `WeakDual 𝕜 F` over `𝕜` (with `RCLike 𝕜`) is continuous if the real parts of all
the evaluation maps `a ↦ g a y` are continuous for each `y : F`.  -/
WeakDual.continuous_of_continuous_eval_re : ∀ {α : Type u_4} {𝕜 : Type u_5} {F : Type u_7} [inst : TopologicalSpace α] [inst_1 : RCLike 𝕜] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : TopologicalSpace F] {g : α → WeakDual 𝕜 F},
  (∀ (x : F), Continuous fun a => RCLike.re ((g a) x)) → Continuous g
-- Lean.Message
Lean.MessageData.ofGoal.injEq : ∀ (a a_1 : Lean.MVarId), (Lean.MessageData.ofGoal a = Lean.MessageData.ofGoal a_1) = (a = a_1)
-- Init.Try
/-- Helper internal tactic for implementing the tactic `try?`.  -/
Lean.Parser.Tactic.attemptAll : Lean.ParserDescr
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_self_add_one : ∀ {x : ℕ}, (↑x).bmod (x + 1) = if x = 0 then 0 else -1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_sdiff_Ico_left : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Finset.Ico a b \ Finset.Ico a c = Finset.Ico (max a c) b
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mk : Array Lean.Import → String.Pos.Raw → Bool → Option String → Bool → Bool → Bool → Bool → Lean.ParseImports.State
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k}, (cmp (t.insert k v).minKey! k).isLE = true
-- Init.Data.Slice.List.Basic
Std.Slice.Internal.ListSliceData.mk : {α : Type u} → List α → Option ℕ → Std.Slice.Internal.ListSliceData α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get? (m₁ ∪ m₂) k =
          (Std.DTreeMap.Raw.Const.get? m₂ k).or (Std.DTreeMap.Raw.Const.get? m₁ k)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_eq_true : ∀ {α : Type u} [inst : Ring α] {a b : α} {z : ℤ},
  Mathlib.Meta.NormNum.IsInt a z → Mathlib.Meta.NormNum.IsInt b z → a = b
-- Mathlib.Algebra.Group.Graph
MonoidHom.coe_graph : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (f : G →* H), ↑f.graph = {x | f x.1 = x.2}
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce_of_not_pos : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m},
  ↑A 1 0 = 0 →
    ¬0 < ↑A 0 0 →
      FixedDetMatrices.reduce A = ModularGroup.T ^ (-(-↑A 0 1 / -↑A 1 1)) • ModularGroup.S • ModularGroup.S • A
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s` is also open
in `t` (`t` is finer than `s`).  -/
GroupTopology.instPartialOrder : {α : Type u} → [inst : Group α] → PartialOrder (GroupTopology α)
-- Mathlib.Algebra.Category.CommBialgCat
instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite : {R : Type u} → [inst : CommRing R] → (A : (CommAlgCat R)ᵒᵖ) → [CategoryTheory.MonObj A] → Bialgebra R ↑(Opposite.unop A)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.localization_base : ∀ {R : Type u_2} {Rₘ : Type u_4} {Sₘ : Type u_5} [inst : CommRing R] [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
  (M : Submonoid R) [inst_3 : Algebra R Sₘ] [inst_4 : Algebra R Rₘ] [inst_5 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [IsLocalization M Rₘ] [Algebra.FormallyEtale R Sₘ], Algebra.FormallyEtale Rₘ Sₘ
-- Lean.DocString.Types
/-- A quotation.
 -/
Lean.Doc.Block.blockquote : {i : Type u} → {b : Type v} → Array (Lean.Doc.Block i b) → Lean.Doc.Block i b
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr₂.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} (motive : List α → List β → γ → Sort u_3) (x : α) (xr : List α) (y : β)
  (yr : List β) (c : γ) (h_1 : (x : List β) → (c : γ) → motive [] x c) (h_2 : (x : List α) → (c : γ) → motive x [] c)
  (h_3 : (x : α) → (xr : List α) → (y : β) → (yr : List β) → (c : γ) → motive (x :: xr) (y :: yr) c),
  (match x :: xr, y :: yr, c with
    | [], x, c => h_1 x c
    | x, [], c => h_2 x c
    | x :: xr, y :: yr, c => h_3 x xr y yr c) =
    h_3 x xr y yr c
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.iso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    CategoryTheory.CategoryStruct.comp P.iso.inv ((CategoryTheory.projectiveResolutions C).map f) =
      CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) Q.iso.inv
-- Mathlib.Topology.Connected.Basic
/-- The preimage of a connected component is the union of the connected components at the points
of that preimage.  -/
Continuous.preimage_connectedComponent : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → ∀ (y : β), f ⁻¹' connectedComponent y = ⋃ x ∈ f ⁻¹' connectedComponent y, connectedComponent x
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_bot' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a : WithBot α), a * ⊥ = if a = 0 then 0 else ⊥
-- Init.Data.BitVec.Lemmas
BitVec.toFin_shiftLeft : ∀ {w n : ℕ} (x : BitVec w), (x <<< n).toFin = Fin.ofNat (2 ^ w) (x.toNat <<< n)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ X₄ : C} →
      (f₁₂ : X₁ ⟶ X₂) →
        (f₁₃ : X₁ ⟶ X₃) →
          (f₂₄ : X₂ ⟶ X₄) →
            (f₃₄ : X₃ ⟶ X₄) →
              CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄ →
                CategoryTheory.Square C
-- Mathlib.Tactic.CategoryTheory.CancelIso
/-- `cancelIso` simplifies the composition of a morphism and its inverse,
given an expression of the form `f ≫ g`.

Assuming `f` is not a composition (as `Category.assoc` is tagged `@[simp]`),
if `g` is not a composition itself, it checks whether `f` is inverse to `g`
by checking if `f` has an `IsIso` instance and then by running `push inv` on `inv f` and on `g`.
If the check succeeds, then `f ≫ g` is rewritten to `𝟙 _`.

If `g` is of the form `h ≫ k`, the procedure instead checks if `f` and `h` are inverses to each
other, and the procedure rewrites `f ≫ h ≫ k` to `k` if that is the case.
This special case is useful as `f ≫ (h ≫ k)` is in simp-normal form and does not
contain `f ≫ g` directly as a subterm.

For instance, the simproc will successfully rewrite expressions such as
`F.map (G.map (inv (H.map (e.hom)))) ≫ F.map (G.map (H.map (e.inv)))` to `𝟙 _`
because `CategoryTheory.Functor.map_inv` is a `@[push ←]` lemma, and
`CategoryTheory.IsIso.Iso.inv_hom` is a `@[push]` lemma.

This procedure is mostly intended as a post-procedure: it will work better if `f` and `g`
have already been traversed beforehand.  -/
cancelIso : Lean.Meta.Simp.Simproc
-- Mathlib.NumberTheory.Rayleigh
/-- Let `0 < r ∈ ℝ` and `j ∈ ℤ`. Then either `j ∈ B_r` or `B_r` jumps over `j`.  -/
_private.Mathlib.NumberTheory.Rayleigh.0.Beatty.hit_or_miss : ∀ {r : ℝ} {j : ℤ}, r > 0 → j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1
-- Init.Data.List.Pairwise
List.Pairwise.imp_mem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l ↔ List.Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l
-- Mathlib.SetTheory.Ordinal.Basic
/-- The cardinality of a set is an upper-bound for the cardinality of the order type of the set's
mex (minimum excluded value). See `not_lt_enum_ord_mk_min_compl` for the `α` version.  -/
Ordinal.card_typein_min_le_mk : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {s : Set α} (hs : sᶜ.Nonempty),
  ((Ordinal.typein r).toRelEmbedding (⋯.min sᶜ hs)).card ≤ Cardinal.mk ↑s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p))
  (k : ℤ),
  p = Lean.Grind.CommRing.Poly.num k →
    (match p with
      | Lean.Grind.CommRing.Poly.num k => h_1 k
      | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) ≍
      h_1 k
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.inf_mul : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] (I J K_1 : FractionalIdeal (nonZeroDivisors A) K), (I ⊓ J) * K_1 = I * K_1 ⊓ J * K_1
-- Mathlib.Algebra.Prime.Defs
Irreducible.prime_of_isPrimal : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {a : M}, Irreducible a → IsPrimal a → Prime a
-- Init.Grind.Attr
/-- The `⇐` modifier instructs `grind` to select a multi-pattern by traversing the conclusion, and then
all the hypotheses from right to left.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
Lean.Parser.Attr.grindRL : Lean.ParserDescr
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left : F.left = G.left) (right : F.right = G.right),
  F.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom left)
        (CategoryTheory.CategoryStruct.comp G.hom (CategoryTheory.eqToHom ⋯)) →
    F = G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termW' : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
/-- Given a family of modules `N` indexed by a type `ι₁ ⊕ ι₂`,
a multilinear map from the modules `N (.inl i₁)` to `N₁` and
a multilinear map from the modules `N (.inr i₁)` to `N₂`, this
is the induced multilinear map from all the modules `N i` to `N₁ ⊗ N₂`.  -/
MultilinearMap.domCoprodDep : {R : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      [inst : CommSemiring R] →
        {N₁ : Type u_6} →
          [inst_1 : AddCommMonoid N₁] →
            [inst_2 : Module R N₁] →
              {N₂ : Type u_7} →
                [inst_3 : AddCommMonoid N₂] →
                  [inst_4 : Module R N₂] →
                    {N : ι₁ ⊕ ι₂ → Type u_8} →
                      [inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] →
                        [inst_6 : (i : ι₁ ⊕ ι₂) → Module R (N i)] →
                          MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁ →
                            MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂ → MultilinearMap R N (TensorProduct R N₁ N₂)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Aesop.Index.Forward
/-- Merge two indices.  -/
Aesop.ForwardIndex.merge : Aesop.ForwardIndex → Aesop.ForwardIndex → Aesop.ForwardIndex
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- If `P` is separated, then `P⁺` is a sheaf.  -/
CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
  (∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))),
      (∀ (I : S.Arrow),
          (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x =
            (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) →
        x = y) →
    CategoryTheory.Presheaf.IsSheaf J (J.plusObj P)
-- Mathlib.Data.Sym.Sym2
/-- For a set `s : Set α`, `s.sym2` is the set of all unordered pairs of elements from `s`.
 -/
Set.sym2 : {α : Type u_1} → Set α → Set (Sym2 α)
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity.val_mkOfPowEq_coe : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M) {n : ℕ} [inst_1 : NeZero n] (h : ζ ^ n = 1),
  ↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ
-- Mathlib.Data.Matrix.Mul
not_injective_dotProduct_right : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α),
  ¬Function.Injective fun x => x ⬝ᵥ a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (D : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Sheaf J RingCat) [Small.{v, u₂} D],
  CategoryTheory.Limits.HasLimitsOfShape D (SheafOfModules R)
-- Init.Data.UInt.Lemmas
UInt16.toNat_add : ∀ (a b : UInt16), (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 16
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listSum_map_zero : ∀ {α : Type u_1} {n : ℤ} {l : List α} {f : α → ℤ}, (∀ x ∈ l, f x ≡ 0 [ZMOD n]) → (List.map f l).sum ≡ 0 [ZMOD n]
-- Mathlib.Topology.Bases
/-- The sets from `s` cover the whole space.  -/
TopologicalSpace.IsTopologicalBasis.sUnion_eq : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)}, TopologicalSpace.IsTopologicalBasis s → ⋃₀ s = Set.univ
-- Lean.Declaration
Lean.RecursorRule.mk : Lean.Name → ℕ → Lean.Expr → Lean.RecursorRule
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂),
  K.D₂ c₁₂ i₁₂ i₁₂' =
    K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun x x_1 =>
      match x, x_1 with
      | (i₁, i₂), x => K.d₂ c₁₂ i₁ i₂ i₁₂'
-- Mathlib.Data.Set.Prod
/-- Three functions between the three pairs of spaces $X_i, Y_i, Z_i$ that are compatible
induce a function $X_1 \times_{Y_1} Z_1 \to X_2 \times_{Y_2} Z_2$.  -/
Function.mapPullback : {X₁ : Type u_1} →
  {X₂ : Type u_2} →
    {Y₁ : Sort u_3} →
      {Y₂ : Sort u_4} →
        {Z₁ : Type u_5} →
          {Z₂ : Type u_6} →
            {f₁ : X₁ → Y₁} →
              {g₁ : Z₁ → Y₁} →
                {f₂ : X₂ → Y₂} →
                  {g₂ : Z₂ → Y₂} →
                    (mapX : X₁ → X₂) →
                      (mapY : Y₁ → Y₂) →
                        (mapZ : Z₁ → Z₂) →
                          f₂ ∘ mapX = mapY ∘ f₁ →
                            g₂ ∘ mapZ = mapY ∘ g₁ → Function.Pullback f₁ g₁ → Function.Pullback f₂ g₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if compare a k = Ordering.eq then some b else none)
              l).or
          (Std.DTreeMap.Internal.Impl.Const.get? t k)
-- Mathlib.Algebra.Lie.Quotient
/-- The quotient of a Lie module by a Lie submodule, is a Lie module.  -/
LieSubmodule.Quotient.lieQuotientLieModule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M], LieModule R L (M ⧸ N)
-- Mathlib.Data.DFinsupp.BigOperators
AddMonoidHom.dfinsuppSumAddHom_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : AddZeroClass R]
  [inst_2 : AddCommMonoid S] [inst_3 : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S)
  (r : R), ((DFinsupp.sumAddHom g) f) r = (DFinsupp.sumAddHom fun i => (AddMonoidHom.eval r).comp (g i)) f
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.mul_fromCols : ∀ {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R] [inst_1 : Fintype n]
  (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R), A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)
-- Mathlib.Order.Disjoint
Codisjoint.sup_lt_right_of_left_ne_bot : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → a ≠ ⊤ → a ⊓ b < b
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Is the expression a `<`-like comparison of `Nat` expressions  -/
Lean.Elab.WF.GuessLex.isNatCmp : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_union : ∀ {R : Type u} [inst : CommSemiring R] (s s' : Set R),
  PrimeSpectrum.zeroLocus (s ∪ s') = PrimeSpectrum.zeroLocus s ∩ PrimeSpectrum.zeroLocus s'
-- Mathlib.Order.Hom.Basic
OrderIso.symm_apply_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {x : α} {y : β},
  e.symm y < x ↔ y < e x
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_finsuppSum : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  (f : ι →₀ N) (g : ι → N → M →₀ R), MonoidAlgebra.ofCoeff (f.sum g) = f.sum fun i n => MonoidAlgebra.ofCoeff (g i n)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.Context.mk : (Lean.MVarId → Lean.MetaM Bool) → (Lean.MVarId → Lean.MetaM Unit) → Mathlib.Tactic.GCongr.Context
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.entry.sizeOf_spec : ∀ {α : Type u} {β : Type v} {σ : Type w} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ] (key : α) (val : β),
  sizeOf (Lean.PersistentHashMap.Entry.entry key val) = 1 + sizeOf key + sizeOf val
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.zero_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M}, v.MutuallySingular 0
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Minute.Offset
-- Init.Data.Range.Polymorphic.UInt
USize.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? USize
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.getClassName : Lean.Elab.DerivingClassView → Lean.CoreM Lean.Name
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.empty_equiv_iff_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, Std.TreeSet.Raw.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.Algebra.Polynomial.Identities
/-- `x^n - y^n` can be expressed as `z * (x - y)` for some `z` in the ring.
 -/
Polynomial.powSubPowFactor : {R : Type u} → [inst : CommRing R] → (x y : R) → (i : ℕ) → { z // x ^ i - y ^ i = z * (x - y) }
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.a : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.HourMarker