mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesFiniteLimits_sheafification : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [CategoryTheory.Limits.HasFiniteLimits D]
  [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms], CategoryTheory.Limits.PreservesFiniteLimits (J.sheafification D)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.pullback_obj_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {A B X Y : C} {f : Y ⟶ X} {i : A ⟶ X} [inst_2 : CategoryTheory.Mono i] {j : B ⟶ Y} [inst_3 : CategoryTheory.Mono j]
  {f' : B ⟶ A},
  CategoryTheory.IsPullback f' j i f →
    (CategoryTheory.Subobject.pullback f).obj (CategoryTheory.Subobject.mk i) = CategoryTheory.Subobject.mk j
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Earlier, this name was used by what is now called `MultilinearMap.map_update_smul_left`.  -/
MultilinearMap.map_update_smul : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R)
  (x : M₁ i), f (Function.update m i (c • x)) = c • f (Function.update m i x)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.zsmul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (n : ℤ), Function.Periodic f (n • c)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
CategoryTheory.Limits.colim.mapShortComplex_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
  {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone S.X₂) (c₃ : CategoryTheory.Limits.Cocone S.X₃) (f : c₁.pt ⟶ c₂.pt)
  (g : c₂.pt ⟶ c₃.pt)
  (hf :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
  (hg :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g = CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
  (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).g = g
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
/-- The Moebius function on a unique factorization monoid, defined to be
`((-1) ^ (factors a).card)` if `a` is squarefree and `0` otherwise.  -/
UniqueFactorizationMonoid.moebius : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → α → ℤ
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContinuousLinearMap.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_6} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (L : E →L[𝕜] F) {x : E}, ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) x
-- Init.Data.Fin.Lemmas
Fin.pred_mk : ∀ {n : ℕ} (i : ℕ) (h : i < n + 1) (w : ⟨i, h⟩ ≠ 0), ⟨i, h⟩.pred w = ⟨i - 1, ⋯⟩
-- Init.Data.List.Perm
List.Perm.pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {l l' : List α},
  l.Perm l' → List.Pairwise R l → (∀ {x y : α}, R x y → R y x) → List.Pairwise R l'
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantFormClass.slashInvariantForm : ∀ (Γ : outParam (Subgroup (GL (Fin 2) ℝ))) (k : outParam ℤ), SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.isPreimmersion_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsPreimmersion f ↔ AlgebraicGeometry.SurjectiveOnStalks f ∧ Topology.IsEmbedding ⇑f
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.lift.congr_simp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {H : Type u_2} [inst_1 : Group H] (f f_1 : G →* H)
  (e_f : f = f_1) (x x_1 : H) (e_x : x = x_1) (hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x),
  HNNExtension.lift f x hx = HNNExtension.lift f_1 x_1 ⋯
-- Mathlib.Order.RelClasses
Std.Refl.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Refl r], Std.Refl (Function.swap r)
-- Std.Time.Date.Unit.Week
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
 -/
Std.Time.Week.OfYear.Ordinal.ofFin : Fin 54 → Std.Time.Week.OfYear.Ordinal
-- Init.Data.Char.Basic
/-- The character's Unicode code point as a `Nat`.
 -/
Char.toNat : Char → ℕ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α} {fallback : β a}
  {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).getD a fallback = fallback
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_8 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w n : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (rhs : Std.Tactic.BVDecide.BVExpr n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhs.shiftLeft rhs with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_8 w n lhs rhs
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Multiset.smul_sum : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid N] [inst_1 : DistribSMul M N] {r : M} {s : Multiset N},
  r • s.sum = (Multiset.map (fun x => r • x) s).sum
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumradius of a simplex.  -/
Affine.Simplex.circumradius : {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 : ℕ} → Affine.Simplex ℝ P n → ℝ
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.Simps.symm_apply.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (h : α ≃+o β), OrderAddMonoidIso.Simps.symm_apply h = ⇑h.symm
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The exact short complex `X ⟶ Y ⟶ cokernel f` for any morphism `f : X ⟶ Y`.  -/
CategoryTheory.ShortComplex.cokernelSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → {X Y : C} → (X ⟶ Y) → CategoryTheory.ShortComplex C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a fallback : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.getKeyD a fallback =
    if compare k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  Q 2 = 0 → W'.addX P Q = (-(Q 0 * P 2)) ^ 2 * P 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_cons_of_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
  {h₁ : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false),
  Std.Internal.List.getValue a (⟨k, v⟩ :: l) h₁ = Std.Internal.List.getValue a l ⋯
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_eq_lcomp : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂),
  f.dualMap = LinearMap.lcomp R R f
-- Std.Data.DHashMap.Basic
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.DHashMap.forIn : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} →
        [Monad m] →
          {x : BEq α} → {x_1 : Hashable α} → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DHashMap α β → m δ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation : Type
-- Init.Data.BitVec.Lemmas
BitVec.ule_eq_not_ult : ∀ {w : ℕ} (x y : BitVec w), x.ule y = !y.ult x
-- Std.Time.Zoned.Database.TZdb
/-- A file path (the part after the leading `:`), absolute or relative to a zoneinfo directory.
 -/
Std.Time.Database.TZdb.TZSpec.filePath : String → Std.Time.Database.TZdb.TZSpec
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.mk.inj : ∀ {model : String} {speed : UInt64} {times : Std.Internal.UV.System.CPUTimes} {model_1 : String} {speed_1 : UInt64}
  {times_1 : Std.Internal.UV.System.CPUTimes},
  { model := model, speed := speed, times := times } = { model := model_1, speed := speed_1, times := times_1 } →
    model = model_1 ∧ speed = speed_1 ∧ times = times_1
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.restrictPreimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X},
  IsCoveringMapOn f s → ∀ (t : Set X), IsCoveringMapOn (t.restrictPreimage f) (Subtype.val ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObjIsoOfRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ GrpCat) (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X),
  CategoryTheory.yonedaGrpObjIsoOfRepresentableBy X F α =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        (let __Equiv := α.homEquiv;
          { toEquiv := __Equiv, map_mul' := ⋯ }).toGrpIso)
      ⋯
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f₁ f₂ : M ⟶ N), f₁.hom = f₂.hom → f₁ = f₂
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.mul_apply : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Mul (M i)] (f g : (i : ι) → M i) (i : ι), (f * g) i = f i * g i
-- Mathlib.Topology.Category.TopCat.Basic
/-- The constant morphism `X ⟶ Y` in `TopCat` given by `y : Y`.  -/
TopCat.const : {X Y : TopCat} → ↑Y → (X ⟶ Y)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_single : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i}, f.sum DFinsupp.single = f
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
instKrullDimLEOfNatNatOfIsDiscreteValuationRing : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], Ring.KrullDimLE 1 R
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
instIsKleinFourMultiplicativeOfIsAddKleinFour : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G], IsKleinFour (Multiplicative G)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
/-- $a^{-1}ba$ is a vector.  -/
CliffordAlgebra.invOf_ι_mul_ι_mul_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (a b : M) [inst_3 : Invertible ((CliffordAlgebra.ι Q) a)] [inst_4 : Invertible (Q a)],
  ⅟((CliffordAlgebra.ι Q) a) * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
    (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.edist_tmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x x' : E)
  (y y' : F), edist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The composition with the functor `p` is *equal* to the constant functor mapping to `S`.  -/
HasFibers.comp_const : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} [self : HasFibers p] (S : 𝒮),
  (HasFibers.ι S).comp p = (CategoryTheory.Functor.const (HasFibers.Fib p S)).obj S
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_sub_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] {p q : ℚ}, ↑p.den ≠ 0 → ↑q.den ≠ 0 → ↑(p - q) = ↑p - ↑q
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `extremalNumber (card V) H` is greater than `x` if and only if there exists a `H`-free simple
graph `G` with more than `x` edges.  -/
SimpleGraph.lt_extremalNumber_iff_of_nonneg : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] {R : Type u_3} [inst_1 : Semiring R] [inst_2 : LinearOrder R]
  [FloorSemiring R] (H : SimpleGraph W) {m : R},
  0 ≤ m → (m < ↑(SimpleGraph.extremalNumber (Fintype.card V) H) ↔ ∃ G x, H.Free G ∧ m < ↑G.edgeFinset.card)
-- Mathlib.Data.Vector.Mem
List.Vector.notMem_map_zero : ∀ {α : Type u_1} {β : Type u_2} (b : β) (v : List.Vector α 0) (f : α → β), b ∉ (List.Vector.map f v).toList
-- Mathlib.Data.List.Basic
List.reverse_surjective : ∀ {α : Type u}, Function.Surjective List.reverse
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelDown'.eq_1 : ∀ (α : Type u_1) [inst : AddRightCancelSemigroup α] [inst_1 : DecidableEq α] (a x x_1 : α),
  ComplexShape.instDecidableRelRelDown' α a x x_1 = id inferInstance
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.Hom.right.eq_1 : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (f : Y ⟶ X),
  CategoryTheory.Arrow.Hom.right f = f.right
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.functorialRightResolutions.Φ_functor_map_ι_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {ρ : CategoryTheory.Functor C₂ C₁} {i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor} [inst_2 : Φ.functor.Full]
  [inst_3 : Φ.functor.Faithful] (X₁ : C₁),
  Φ.functor.map ((CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι i).app X₁) = i.app (Φ.functor.obj X₁)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedEntry : Inhabited Lean.Parser.ParserExtension.Entry
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE.congr_simp : ∀ {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) (a b : ℤ) (h : a ≤ b),
  t.natTransTruncGEOfLE a b h = t.natTransTruncGEOfLE a b h
-- Init.Data.Vector.Basic
Vector.instNonempty : ∀ {α : Type u_1} {n : ℕ} [Nonempty α], Nonempty (Vector α n)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor_δ : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N)
  (m₁ m₂ : CategoryTheory.Discrete M),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.frobeniusAlgHom_apply : ∀ (K : Type u_1) (R : Type u_2) [inst : Field K] [inst_1 : Fintype K] [inst_2 : CommRing R] [inst_3 : Algebra K R]
  (x : R), (FiniteField.frobeniusAlgHom K R) x = x ^ Fintype.card K
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulRightInvariant] (g : G),
  MeasureTheory.Measure.QuasiMeasurePreserving (fun h => g / h) μ μ
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioo_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂)
-- Mathlib.LinearAlgebra.Prod
LinearMap.inr_eq_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
-- Mathlib.CategoryTheory.Sites.Spaces
Opens.mem_grothendieckTopology : ∀ (T : Type u) [inst : TopologicalSpace T] {U : TopologicalSpace.Opens T} {S : CategoryTheory.Sieve U},
  S ∈ (Opens.grothendieckTopology T) U ↔ ∀ x ∈ U, ∃ V f, S.arrows f ∧ x ∈ V
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_le_degree_of_subset_roots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {Z : Finset R},
  Z.val ⊆ p.roots → Z.card ≤ p.natDegree
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.tendsto_atTop_iff : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {f : γ → α}
  (e : α ≃o β), Filter.Tendsto (fun x => e (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.Topology.Algebra.Constructions
Topology.IsEmbedding.units_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : Monoid N] {f : M →* N}, Topology.IsEmbedding ⇑f → Topology.IsEmbedding ⇑(Units.map f)
-- Init.Data.UInt.Lemmas
/-- Note that on 32-bit machines we are doing a modulo by zero.  -/
UInt32.toUSize_mul : ∀ (a b : UInt32), (a * b).toUSize = a.toUSize * b.toUSize % 4294967296
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Opens.isDominant_ι : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens}, Dense ↑U → AlgebraicGeometry.IsDominant U.ι
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.comp_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal],
  CategoryTheory.Functor.OplaxMonoidal.η (F.comp G) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.η F))
      (CategoryTheory.Functor.OplaxMonoidal.η G)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instInhabited : Inhabited AddGrpCat
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly : Type
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) (j : J) {Z : C}
  (h : G.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom
      (CategoryTheory.CategoryStruct.comp (t.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app j) (CategoryTheory.CategoryStruct.comp (w.hom.app j) h)
-- Mathlib.Tactic.DeriveCountable
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkToNatMatch.mkAlts : Lean.Elab.Deriving.Context →
  Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (U : TopologicalSpace.Opens G),
  μ.innerContent U = ⨆ K, ⨆ (_ : ↑K ⊆ ↑U), μ K
-- Std.Sync.Broadcast
Std.Broadcast.Sync.Receiver.forIn : {α : Type} →
  {m : Type → Type u_1} →
    {β : Type} →
      [Inhabited α] →
        [Monad m] → [MonadLiftT BaseIO m] → Std.Broadcast.Sync.Receiver α → (α → β → m (ForInStep β)) → β → m β
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- A quadratic form composed with a `LinearEquiv` is isometric to itself.  -/
QuadraticMap.isometryEquivOfCompLinearEquiv : {R : Type u_2} →
  {M : Type u_4} →
    {M₁ : Type u_5} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module R N] → (Q : QuadraticMap R M N) → (f : M₁ ≃ₗ[R] M) → Q.IsometryEquiv (Q.comp ↑f)