mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.CochainComplexOpposite
ChainComplex.cochainComplexEquivalence.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  ChainComplex.cochainComplexEquivalence C =
    { functor := ComplexShape.embeddingUpIntDownInt.restrictionFunctor C,
      inverse := ComplexShape.embeddingDownIntUpInt.restrictionFunctor C,
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun K => HomologicalComplex.Hom.isoOfComponents (fun n => HomologicalComplex.XIsoOfEq K ⋯) ⋯) ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun K => HomologicalComplex.Hom.isoOfComponents (fun n => HomologicalComplex.XIsoOfEq K ⋯) ⋯) ⋯,
      functor_unitIso_comp := ⋯ }
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.preservesCoequalizer : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
  AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.one : ∀ (R : Type u_1) [inst : MulOneClass R] [inst_1 : StarMul R], IsStarProjection 1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.left_of_union : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f (s ∪ t) μ → MeasureTheory.IntegrableOn f s μ
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompNatTrans_assoc : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₃] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {F₁₃ : CategoryTheory.Functor C₁ C₃} {F₀₃ : CategoryTheory.Functor C₀ C₃} {G₁₀ : CategoryTheory.Functor C₁ C₀}
  {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₃₂ : CategoryTheory.Functor C₃ C₂} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  {G₃₁ : CategoryTheory.Functor C₃ C₁} {G₃₀ : CategoryTheory.Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁)
  (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀)
  (τ₁₂₃ : G₃₁ ⟶ G₃₂.comp G₂₁) (τ₀₁₃ : G₃₀ ⟶ G₃₁.comp G₁₀) (τ₀₂₃ : G₃₀ ⟶ G₃₂.comp G₂₀),
  CategoryTheory.CategoryStruct.comp τ₀₂₃ (G₃₂.whiskerLeft τ₀₁₂) =
      CategoryTheory.CategoryStruct.comp τ₀₁₃
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight τ₁₂₃ G₁₀)
          (G₃₂.associator G₂₁ G₁₀).hom) →
    CategoryTheory.CategoryStruct.comp (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃))
        (adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃) =
      CategoryTheory.CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃)
          (adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃))
-- Mathlib.Data.Setoid.Partition
/-- sends an index to an element of the corresponding set  -/
IndexedPartition.some : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → ι → α
-- Mathlib.Topology.Order
DiscreteTopology.mk : ∀ {α : Type u_2} [t : TopologicalSpace α], t = ⊥ → DiscreteTopology α
-- Mathlib.RingTheory.Algebraic.Pi
Polynomial.algebraMap_pi_eq_aeval : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra S T],
  ⇑(algebraMap (Polynomial R) (S → T)) = fun p z => (algebraMap S T) ((Polynomial.aeval z) p)
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_pow_of_isSquare : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] {x : R}, IsSquare x → ∀ {n : ℕ}, n ≠ 0 → ∃ r, x = r ^ n
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), pathComponentIn Set.univ x = pathComponent x
-- Mathlib.Data.List.Basic
List.head_eq_getElem_zero : ∀ {α : Type u} {l : List α} (hl : l ≠ []), l.head hl = l[0]
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLE.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3)
  (size : ℕ) (ky : α) (y : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the projection is smaller or equal to the norm of the original element.  -/
QuotientAddGroup.norm_mk_le_norm : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M}, ‖↑m‖ ≤ ‖m‖
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] {x x' y y' : C}
  (f : x ⟶ x') (g : y ⟶ y') {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj
        ((CategoryTheory.MonoidalCategory.tensor C).obj (x', y')) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x', y')) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
        h)
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions.id? : Lean.Lsp.StaticRegistrationOptions → Option String
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isMatch_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch p pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.denoteN ctx a.neg = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.comp_symm_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (f : β → α) (g : α → α), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.Functor.PreservesHomology.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_4 : F.PreservesZeroMorphisms], F.PreservesHomology = F_1.PreservesHomology
-- Mathlib.Data.Finset.Density
Finset.nnratCast_dens_mul_natCast_card : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : Semifield 𝕜] [CharZero 𝕜] (s : Finset α),
  ↑s.dens * ↑(Fintype.card α) = ↑s.card
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracket_const_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {x : E} {c : 𝕜},
  DifferentiableAt 𝕜 V x → VectorField.lieBracket 𝕜 (c • V) W x = c • VectorField.lieBracket 𝕜 V W x
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X)
  (R : CategoryTheory.Sieve ((CategoryTheory.Over.forget X).obj Y)),
  (RelIso.symm (CategoryTheory.Sieve.overEquiv Y)) R =
    CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.forget X) R
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreFunctor_obj_map_iso_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Core (CategoryTheory.Functor C D)) {X Y : CategoryTheory.Core C} (f : X ⟶ Y),
  (((CategoryTheory.coreFunctor C D).obj F).map f).iso.inv = F.of.map f.iso.inv
-- Lean.Elab.InfoTree.Types
Lean.Elab.ChoiceInfo.toElabInfo : Lean.Elab.ChoiceInfo → Lean.Elab.ElabInfo
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toList_take_zip : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂]
  [Std.Iterators.Productive α₁ Id] [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β₁} {it₂ : Std.Iter β₂} {n : ℕ},
  (Std.Iter.take n (it₁.zip it₂)).toList = (Std.Iter.take n it₁).toList.zip (Std.Iter.take n it₂).toList
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.cycle.eq_1 : ∀ (n : ℕ),
  SimpleGraph.cycleGraph.cycle n = SimpleGraph.Walk.cons ⋯ (SimpleGraph.cycleGraph.cycleCons✝ n (Fin.last (n + 2)))
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioi_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n), ∏ i > a.succ, f i = ∏ i > a, f i.succ
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommSum_addCommute : ∀ {α : Type u_3} [inst : AddMonoid α] (s : Multiset α) (comm : {x | x ∈ s}.Pairwise AddCommute) (y : α),
  (∀ x ∈ s, AddCommute y x) → AddCommute y (s.noncommSum comm)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddMonObj.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (zero zero_1 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (e_zero : zero = zero_1)
  (add add_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) (e_add : add = add_1)
  (zero_add :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight zero X) add =
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
  (add_zero :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X zero) add =
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
  (add_assoc :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight add X) add =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X add) add)),
  { zero := zero, add := add, zero_add := zero_add, add_zero := add_zero, add_assoc := add_assoc } =
    { zero := zero_1, add := add_1, zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.toFun.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c), ↑f = (someContDiffBumpBase E).toFun (f.rOut / f.rIn) ∘ fun x => f.rIn⁻¹ • (x - c)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β] (f : α → β),
  Finset.sup 0 f = f 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_norm : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] (f : α → F), MeasureTheory.eLpNorm (fun x => ‖f x‖) p μ = MeasureTheory.eLpNorm f p μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_k_eq_toPoly : ∀ (e : Lean.Grind.CommRing.Expr), e.toPoly_k = e.toPoly
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.comp_app : ∀ (J : Type u_1) [inst : LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) (x : SimplexCategoryᵒᵖ),
  (CategoryTheory.EnrichedCategory.comp i j k).app x =
    TypeCat.ofHom fun x_1 => (CategoryTheory.Functor.prod' x_1.1 x_1.2).comp (i.compFunctor j k)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {K : CategoryTheory.GrothendieckTopology C},
  J ≤ K →
    ∀ {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G),
      CategoryTheory.Presheaf.IsLocallySurjective J f → CategoryTheory.Presheaf.IsLocallySurjective K f
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.independent_maxGenEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M), iSupIndep f.maxGenEigenspace
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_equivProd_symm_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R), ((QuaternionAlgebra.equivProd c₁ c₂ c₃).symm a).imK = a.2.2.2
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
      _auto_153✝)
  (unit :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
          (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
        CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
      _auto_155✝)
  (tensor :
    autoParam
      (∀ (X Y : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
            (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
            (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
      _auto_157✝)
  (X : C), (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).inv.hom.hom.app X = (e X).inv
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_le_untop₀_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] {a b : WithTop α},
  a ≠ ⊤ → b ≠ ⊤ → (a.untop₀ ≤ b.untop₀ ↔ a ≤ b)
-- Mathlib.NumberTheory.Pell
/-- `Pell.Solution₁ d` is the type of solutions to the Pell equation `x^2 - d*y^2 = 1`.
We define this in terms of elements of `ℤ√d` of norm one.
 -/
Pell.Solution₁ : ℤ → Type
-- Mathlib.CategoryTheory.Sites.Plus
/-- The natural transformation from the identity functor to `plus`.  -/
CategoryTheory.GrothendieckTopology.toPlusNatTrans : {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.plusFunctor D
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.isHomogeneous_C_mul_X_pow : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (r : R) (i : σ) (n : ℕ),
  (MvPolynomial.C r * MvPolynomial.X i ^ n).IsHomogeneous n
-- Lean.Meta.Tactic.Assert
/-- Convert the given goal `Ctx |- target` into `Ctx, (hs[0].userName : hs[0].type) ... |-target`.
It assumes `hs[i].val` has type `hs[i].type`.  -/
Lean.MVarId.assertHypotheses : Lean.MVarId → Array Lean.Meta.Hypothesis → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Algebra.Group.Invertible.Basic
invOf_pow : ∀ {α : Type u} [inst : Monoid α] (m : α) [inst_1 : Invertible m] (n : ℕ) [inst_2 : Invertible (m ^ n)],
  ⅟(m ^ n) = ⅟m ^ n
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.toOption : Lean.Name → Thunk Lean.MessageData → Array Lean.MessageData → Option Lean.MessageData
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_bot_inj : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : DiscreteTopology X] {x y : X}, ⊥.proj x = ⊥.proj y ↔ x = y
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.abs_norm_eq_max_natAbs_neg : ∀ (n : ℕ), ‖![1, -(↑n + 1)]‖ = ↑n + 1
-- Lean.Util.Trace
Lean.instInhabitedTraceState.default : Lean.TraceState
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.toDual_def : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b : B.Nondegenerate) {m n : V},
  ((B.toDual b) m) n = (B m) n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospanMapIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape}
  (d : CategoryTheory.Limits.MulticospanIndex J C) (F : CategoryTheory.Functor C D)
  (X : CategoryTheory.Limits.WalkingMulticospan J),
  (d.multicospanMapIso F).inv.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (d.left a))
      | CategoryTheory.Limits.WalkingMulticospan.right a => CategoryTheory.Iso.refl (F.obj (d.right a))).inv
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.HasLeftDerivedFunctor.mk : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_2} H] {F : CategoryTheory.Functor C H}
  {W : CategoryTheory.MorphismProperty C}, W.Q.HasRightKanExtension F → F.HasLeftDerivedFunctor W
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.degreewiseEpiWithInjectiveKernel_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CochainComplex.degreewiseEpiWithInjectiveKernel (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀)
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} {l : Filter β},
  (∀ x ∈ s, f x = g x) → Filter.Tendsto f (nhdsWithin a s) l → Filter.Tendsto g (nhdsWithin a s) l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mk.injEq : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (fst : A) (snd : C) (iso : F.obj fst ≅ G.obj snd)
  (fst_1 : A) (snd_1 : C) (iso_1 : F.obj fst_1 ≅ G.obj snd_1),
  ({ fst := fst, snd := snd, iso := iso } = { fst := fst_1, snd := snd_1, iso := iso_1 }) =
    (fst = fst_1 ∧ snd = snd_1 ∧ iso ≍ iso_1)
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.localRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Flat →
    ∀ (P : Ideal S) [inst_2 : P.IsPrime] (Q : Ideal R) [inst_3 : Q.IsPrime] (hQP : Q = Ideal.comap f P),
      (Localization.localRingHom Q P f hQP).Flat
-- Std.Time.Format.Modifier
Std.Time.OffsetO.noConfusionType : Sort v✝ → Std.Time.OffsetO → Std.Time.OffsetO → Sort v✝
-- Mathlib.Logic.Small.Defs
Shrink.rec.eq_1 : ∀ {α : Type u_1} [inst : Small.{w, u_1} α] {F : Shrink.{w, u_1} α → Sort v} (h : (X : α) → F ((equivShrink α) X))
  (X : Shrink.{w, u_1} α), Shrink.rec h X = ⋯ ▸ h ((equivShrink α).symm X)
-- Init.Data.Array.Find
Array.findSome?_replicate_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isNone = true → Array.findSome? f (Array.replicate n a) = none
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq_assoc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₂.HasTensor X₃]
  [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j)
  (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) {Z : C}
  (h_1 :
    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ i₁)
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h'))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) i₁
          i₂₃ j ⋯)
        h_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.rightUnitor_hom_app_apply : ∀ (K : SSet) {Δ : SimplexCategoryᵒᵖ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj K (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet)).obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (K.obj Δ)).hom) x = x.1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₁ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₃))