mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- The distance defines a metric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`.  -/
metricSpaceOfNormedAddCommGroupOfAddTorsor : (V : Type u_6) → (P : Type u_7) → [inst : NormedAddCommGroup V] → [AddTorsor V P] → MetricSpace P
-- Init.Data.Vector.Count
Vector.count_le_size : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a : α} {xs : Vector α n}, Vector.count a xs ≤ n
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.empty : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α], DirSupInaccOn D ∅
-- Lean.Meta.Hint
/-- Converts an array of diff actions into corresponding JSON interpretable by `tryThisDiffWidget`.
 -/
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.mkDiffJson : Array (Lean.Diff.Action × String) → Lean.Json
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- If we augment the universal cover of the classifying space of `G` as a simplicial set by the
map from `Fin 1 → G` to the terminal object in `Type u`, then apply the free functor
`Type u ⥤ ModuleCat.{u} k`, the resulting augmented simplicial `k`-module has an extra
degeneracy.  -/
classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmentedToModule : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] → (classifyingSpaceUniversalCover.compForgetAugmented.toModule k G).ExtraDegeneracy
-- Mathlib.Data.Nat.Bits
Nat.bit1_bits : ∀ (n : ℕ), (2 * n + 1).bits = true :: n.bits
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.range_toSubsemiring : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.range.toSubsemiring = (↑φ).rangeS
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_congr : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊣⊢ₛ P') → (Q ⊣⊢ₛ Q') → P ∧ Q ⊣⊢ₛ P' ∧ Q'
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_cthickening_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  x ∈ Metric.cthickening δ s ↔ Metric.infEDist x s ≤ ENNReal.ofReal δ
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.add_mem_iff_right : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, x ∈ p → (x + y ∈ p ↔ y ∈ p)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.eraseIdx.eq_def : ∀ {α : Type u} (xs : Array α) (i : ℕ) (h : i < xs.size),
  xs.eraseIdx i h =
    if h' : i + 1 < xs.size then
      let xs' := xs.swap (i + 1) i h' h;
      xs'.eraseIdx (i + 1) ⋯
    else xs.pop
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.addCommGroupIsoToAddEquiv.eq_1 : ∀ {X Y : AddCommGrpCat} (i : X ≅ Y),
  i.addCommGroupIsoToAddEquiv = (AddCommGrpCat.Hom.hom i.hom).toAddEquiv (AddCommGrpCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Sqrt
DifferentiableWithinAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  DifferentiableWithinAt ℝ f s x → f x ≠ 0 → DifferentiableWithinAt ℝ (fun y => √(f y)) s x
-- Batteries.Data.Float.Lemmas
Float.toBits.eq_1 : ∀ (a : Float), a.toBits = a.toModel.toBits
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) This new cocone is used to construct the coalgebra structure  -/
CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) →
            CategoryTheory.Limits.Cocone (D.comp T.forget) → CategoryTheory.Limits.Cocone (D.comp T.forget)
-- Mathlib.Data.Nat.Bitwise
Nat.and_two_pow : ∀ (n i : ℕ), n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.norm_fst_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.fst‖ ≤ ‖x‖
-- Init.Data.Array.Lemmas
Array.isEmpty_reverse : ∀ {α : Type u_1} {xs : Array α}, xs.reverse.isEmpty = xs.isEmpty
-- Init.Data.Array.DecidableEq
Array.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Array α)
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- Two vertices are related in the zigzag setoid if there is a
zigzag of arrows from one to the other.  -/
Quiver.zigzagSetoid : (V : Type u_1) → [Quiver V] → Setoid V
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_exp_eq_re_add_toIocMod : ∀ (x : ℂ), Complex.log (Complex.exp x) = ↑x.re + ↑(toIocMod Real.two_pi_pos (-Real.pi) x.im) * Complex.I
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumClique.isMaximalClique : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (s : Finset α), G.IsMaximumClique s → Maximal G.IsClique ↑s
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk.sizeOf_spec : ∀ {R : Type u} {a b : R} [inst : SizeOf R] (re im : R), sizeOf { re := re, im := im } = 1 + sizeOf re + sizeOf im
-- Mathlib.Analysis.Normed.Group.Uniform
dist_mul_self_right : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b : E), dist a (b * a) = ‖b‖
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int64
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'}, HasStrictFDerivAt c c' x → ∀ (d : 𝔸'), HasStrictFDerivAt (fun y => c y * d) (d • c') x
-- Init.Data.List.Nat.Range
List.zipIdx_append : ∀ {α : Type u_1} {xs ys : List α} {k : ℕ}, (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.length)
-- Init.Data.BitVec.Bitblast
BitVec.msb_abs : ∀ {w : ℕ} {x : BitVec w}, x.abs.msb = (decide (x = BitVec.intMin w) && decide (0 < w))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∉ t → t.getKey! a = default
-- Mathlib.Analysis.Convex.Between
affineSegment.lift : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [ZeroLEOneClass R] (R' : Type u_6) [inst_6 : Ring R']
  [inst_7 : PartialOrder R'] [inst_8 : Module R' V] [inst_9 : Module R' R] [IsScalarTower R' R V] [SMulPosMono R' R]
  (x y : P), affineSegment R' x y ⊆ affineSegment R x y
-- Mathlib.Algebra.Homology.TotalComplex
/-- The horizontal differential in the total complex.  -/
HomologicalComplex₂.D₁ : {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₁₂] →
                      [DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁₂ i₁₂' : I₁₂) →
                            K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass R S M],
  IsScalarTower S (Module.End R M) (Module.End R M)
-- Init.Data.Int.DivMod.Lemmas
Int.sign_ediv : ∀ (a b : ℤ), (a / b).sign = if 0 ≤ a ∧ a < ↑b.natAbs then 0 else a.sign * b.sign
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsLeftAdjoint.mk : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction f g), CategoryTheory.Bicategory.IsLeftAdjoint f
-- Mathlib.RingTheory.SimpleRing.Defs
isSimpleRing_iff : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R], IsSimpleRing R ↔ IsSimpleOrder (TwoSidedIdeal R)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coeCLM_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (f : H), (RKHS.coeCLM 𝕜) f = ⇑f
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.coe_of : ∀ (R : Type u) [inst : AddCommGroup R], ↑(AddCommGrpCat.of R) = R
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a < x` and `x < b`. Basically `Set.Ioo a b` as a
multiset.  -/
Multiset.Ioo : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Multiset α
-- Lean.Parser.Types
Lean.Parser.mkAtom : Lean.SourceInfo → String → Lean.Syntax
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioc_disjoint_Ioi_same : ∀ {α : Type v} [inst : Preorder α] {a b : α}, Disjoint (Set.Ioc a b) (Set.Ioi b)
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of
the Schur complement.  -/
Matrix.det_fromBlocks₁₁ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
  (D : Matrix n n α) [inst_5 : Invertible A], (Matrix.fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- A presheaf is separated for a topology if it is separated for every sieve in the topology.  -/
CategoryTheory.Presieve.IsSeparated : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → CategoryTheory.Functor Cᵒᵖ (Type w) → Prop
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
convergence (in distribution) of `ProbabilityMeasure`s on `X` implies convergence (in
distribution) of the push-forwards of these measures by `f`.  -/
MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] [inst_2 : TopologicalSpace Ω]
  [inst_3 : OpensMeasurableSpace Ω] [inst_4 : TopologicalSpace Ω'] [inst_5 : BorelSpace Ω'] {ι : Type u_3}
  {L : Filter ι} (νs : ι → MeasureTheory.ProbabilityMeasure Ω) (ν : MeasureTheory.ProbabilityMeasure Ω),
  Filter.Tendsto νs L (nhds ν) →
    ∀ {f : Ω → Ω'} (f_cont : Continuous f), Filter.Tendsto (fun i => (νs i).map ⋯) L (nhds (ν.map ⋯))
-- Init.Data.BitVec.Basic
/-- Returns a bitvector of size `n` where all bits are `1`.  -/
BitVec.allOnes : (n : ℕ) → BitVec n
-- Lean.CoreM
/-- Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for
`logSnapshotTask` tasks, which are reported as part of the returned tree. The given cancellation
token, if any, should be stored in a `SnapshotTask` for the server to trigger it when the result is
no longer needed.
 -/
Lean.Core.wrapAsyncAsSnapshot : {α : Type} →
  (α → Lean.CoreM Unit) →
    Option IO.CancelToken →
      autoParam String Lean.Core.wrapAsyncAsSnapshot._auto_1 → Lean.CoreM (α → BaseIO Lean.Language.SnapshotTree)
-- Lean.Meta.Tactic.Grind.Arith.IsRelevant
Lean.Meta.Grind.Arith.isSupportedType : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.Integrable.simpleFunc_mul' : ∀ {X : Type u_6} {f : X → ℝ} {m m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X},
  m ≤ m0 → ∀ (g : MeasureTheory.SimpleFunc X ℝ), MeasureTheory.Integrable f μ → MeasureTheory.Integrable (⇑g * f) μ
-- Mathlib.Topology.EMetricSpace.Defs
/-- The extended pseudometric induced by a function taking values in a pseudoemetric space.
See note [reducible non-instances].  -/
PseudoEMetricSpace.induced : {α : Type u_2} → {β : Type u_3} → (α → β) → PseudoEMetricSpace β → PseudoEMetricSpace α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.isEmpty : ∀ {V : Type u} {G : SimpleGraph V} [IsEmpty V], IsEmpty G.ConnectedComponent
-- Mathlib.Data.List.Zip
List.rightInverse_unzip_zip : ∀ {α : Type u} {β : Type u_1}, Function.RightInverse List.unzip (Function.uncurry List.zip)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLECancellable_coe : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddLeftReflectLE α] (a : α), AddLECancellable ↑a
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id._auto_1) {Z : C}
  (h : X.opcycles f (CategoryTheory.CategoryStruct.id i₁) n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f (CategoryTheory.CategoryStruct.id i₁) f ⋯ n₁)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) =
    h
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_smul`. -/
SkewMonoidAlgebra.ofFinsupp_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (a : S) (b : G →₀ k),
  { coeff := a • b } = a • { coeff := b }
-- Mathlib.RingTheory.TensorProduct.Finite
RingHom.Finite.tensorProductMap : ∀ {R : Type u_1} {S : Type u_2} {S' : Type u_3} {T : Type u_4} {T' : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing T] [inst_3 : CommRing S'] [inst_4 : CommRing T'] [inst_5 : Algebra R S] [inst_6 : Algebra R T]
  [inst_7 : Algebra R S'] [inst_8 : Algebra R T'] {f : S →ₐ[R] S'},
  f.Finite → ∀ {g : T →ₐ[R] T'}, g.Finite → (Algebra.TensorProduct.map f g).Finite
-- Mathlib.LinearAlgebra.Matrix.FiniteDimensional
LinearMap.finiteDimensional : ∀ {K : Type u_1} [inst : Field K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module K W] [FiniteDimensional K W],
  FiniteDimensional K (V →ₗ[K] W)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ) (x : E), HasFDerivAt (↑z) 0 x
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b c : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c)
  (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).mapComp f g).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop f.unop X).hom
-- Mathlib.Algebra.Order.Field.Basic
min_div_div_right_of_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α},
  c ≤ 0 → ∀ (a b : α), min (a / c) (b / c) = max a b / c
-- Mathlib.Algebra.Group.Action.Basic
AddAction.toPerm.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α),
  AddAction.toPerm a = { toFun := fun x => a +ᵥ x, invFun := fun x => -a +ᵥ x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- `closedBall x ε` is the set of all points `y` with `dist y x ≤ ε`  -/
Metric.closedBall : {α : Type u} → [PseudoMetricSpace α] → α → ℝ → Set α
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousConstSMul.mk : ∀ {Γ : Type u_1} {T : Type u_2} [inst : TopologicalSpace T] [inst_1 : SMul Γ T],
  (∀ (γ : Γ), Continuous fun x => γ • x) → ContinuousConstSMul Γ T
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The canonical map from `P` to its sheafification, as a natural transformation.
*Note:* We only show this is a sheaf under additional hypotheses on `D`.  -/
CategoryTheory.GrothendieckTopology.toSheafification : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', 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] →
              CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ J.sheafification D
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
/-- The type of nondegenerate simplices which do not belong to
a given subcomplex of a simplicial set.  -/
SSet.Subcomplex.N : {X : SSet} → X.Subcomplex → Type u
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.prevn.eq_2 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw) (i : ℕ), x.prevn i.succ x_1 = x.prevn i (x.prev x_1)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_mul_omega_eq_mk : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R],
  QuadraticAlgebra.omega * QuadraticAlgebra.omega = { re := a, im := b }
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Antitone fun x => Set.Iio (f x)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_sub_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocDiv hp (a - ↑m * p) b = toIocDiv hp a b + ↑m
-- Mathlib.Algebra.Group.Basic
zsmul_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (n : ℤ), n • 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D) (c c' : C),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom =
    (CategoryTheory.Functor.OplaxMonoidal.δ F c c').app d
-- Mathlib.CategoryTheory.Limits.ColimitLimit
/-- The map `colimit_limit_to_limit_colimit` realized as a map of cones.  -/
CategoryTheory.Limits.colimitLimitToLimitColimitCone : {J : Type u₁} →
  {K : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} J] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                  [inst_5 : CategoryTheory.Limits.HasLimit G] →
                    CategoryTheory.Limits.colim.mapCone (CategoryTheory.Limits.limit.cone G) ⟶
                      CategoryTheory.Limits.limit.cone (G.comp CategoryTheory.Limits.colim)
-- Mathlib.GroupTheory.Rank
/-- The minimum number of generators of an additive group.  -/
AddGroup.rank : (G : Type u_1) → [inst : AddGroup G] → [h : AddGroup.FG G] → ℕ
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A family of orthonormal vectors with the correct cardinality forms a basis.  -/
basisOfOrthonormalOfCardEqFinrank : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            [inst_3 : Fintype ι] →
              [Nonempty ι] → {v : ι → E} → Orthonormal 𝕜 v → Fintype.card ι = Module.finrank 𝕜 E → Module.Basis ι 𝕜 E
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaPDF_eq : ∀ (α β x : ℝ),
  ProbabilityTheory.betaPDF α β x =
    ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / ProbabilityTheory.beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0)
-- Mathlib.CategoryTheory.Comma.Basic
/-- We can interpret the commutative square constituting a morphism in the comma category as a
natural transformation between the functors `fst ⋙ L` and `snd ⋙ R` from the comma category
to `T`, where the components are given by the morphism that constitutes an object of the comma
category.  -/
CategoryTheory.Comma.natTrans : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (CategoryTheory.Comma.fst L R).comp L ⟶ (CategoryTheory.Comma.snd L R).comp R
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_anti₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 0 < a → a ≤ 1 → Antitone fun n => a ^ n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertMany_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} {l : List (α × β)}
  {k : α} {v : β},
  Std.DTreeMap.Raw.Const.insertMany t ((k, v) :: l) = Std.DTreeMap.Raw.Const.insertMany (t.insert k v) l
-- Mathlib.CategoryTheory.EpiMono
/-- Every split mono is a mono.  -/
CategoryTheory.IsSplitMono.mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f],
  CategoryTheory.Mono f
-- Mathlib.GroupTheory.Index
Subgroup.index_map_equiv : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (e : G ≃* G'),
  (Subgroup.map (↑e) H).index = H.index
-- Mathlib.Data.Set.Lattice
Set.iUnion_singleton_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), ⋃ x, {f x} = Set.range f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospanMapIso.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (a : J.R) (h_1 : (a : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a))
  (h_2 : (a : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)),
  (match CategoryTheory.Limits.WalkingMulticospan.right a with
    | CategoryTheory.Limits.WalkingMulticospan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMulticospan.right a => h_2 a) =
    h_2 a
-- Init.Data.List.Sublist
List.IsSuffix.ne_nil : ∀ {α : Type u_1} {xs ys : List α}, xs <:+ ys → xs ≠ [] → ys ≠ []
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommAddMonObj.add_comm'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj M]
  {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ M M).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h