mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.hexagon_reverse : ∀ {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.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V)
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (H : CategoryTheory.Functor C V) [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_10 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_11 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_12 :
    CategoryTheory.MonoidalCategory.DayConvolution H (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)]
  [inst_13 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_14 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution H F) G]
  [inst_15 : CategoryTheory.MonoidalCategory.DayConvolution H G]
  [inst_16 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution H G)]
  [inst_17 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_18 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F H) G],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.braiding
            (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).hom
        (CategoryTheory.MonoidalCategory.DayConvolution.associator H F G).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F)
        (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.associator F H G).inv
        (CategoryTheory.MonoidalCategory.DayConvolution.map
          (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom (CategoryTheory.CategoryStruct.id G)))
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instOfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {a : WithTop ℕ∞} [IsManifold I ⊤ M], IsManifold I a M
-- Batteries.Tactic.GeneralizeProofs
/-- The recursion depth, for how many times `visit` is called from within `visitProof.  -/
Batteries.Tactic.GeneralizeProofs.AContext.depth : Batteries.Tactic.GeneralizeProofs.AContext → ℕ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorIso_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y X' Y' : C}
  (f : X ≅ Y) (g : X' ≅ Y'),
  CategoryTheory.MonoidalCategory.tensorIso f g =
    CategoryTheory.MonoidalCategory.whiskerRightIso f X' ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y g
-- Mathlib.Tactic.ITauto
/-- `(p: (x: A) ⊢ B) ⊢ A → B`  -/
Mathlib.Tactic.ITauto.Proof.intro : Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.logOrderIso_symm : ENNReal.logOrderIso.symm = EReal.expOrderIso
-- Init.Grind.Ring.Basic
/-- In every ring there is a canonical map from the integers to the ring.  -/
Lean.Grind.Ring.intCast : {α : Type u} → [self : Lean.Grind.Ring α] → IntCast α
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimTargetInfo.expr : Lean.Elab.Tactic.ElimTargetInfo✝ → Lean.Expr
-- Init.Data.Option.Coe
optionCoe : {α : Type u} → Coe α (Option α)
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.none.sizeOf_spec : ∀ {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)}, sizeOf Mathlib.Tactic.FieldSimp.DenomCondition.none = 1
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.sum.match_1.eq_2 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (u v : W)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_1 : V ⊕ W) → motive x x_1),
  (match Sum.inr u, Sum.inr v with
    | Sum.inl u, Sum.inl v => h_1 u v
    | Sum.inr u, Sum.inr v => h_2 u v
    | x, x_1 => h_3 x x_1) =
    h_2 u v
-- Init.Data.Array.Count
Array.count_pos_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, 0 < Array.count a xs ↔ a ∈ xs
-- Init.Data.List.Basic
/-- Two lists are permutations of each other if they contain the same elements, each occurring the same
number of times but not necessarily in the same order.

One list can be proven to be a permutation of another by showing how to transform one into the other
by repeatedly swapping adjacent elements.

`List.isPerm` is a Boolean equivalent of this relation.
 -/
List.Perm : {α : Type u} → List α → List α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f b) =
    CategoryTheory.CategoryStruct.id (f b)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_eq_bot : ∀ {M : Type u_2} [inst : Mul M] {S : Subsemigroup Mᵐᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.parser.sizeOf_spec : ∀ (catName declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : ℕ),
  sizeOf (Lean.Parser.ParserExtension.Entry.parser catName declName leading p prio) =
    1 + sizeOf catName + sizeOf declName + sizeOf leading + sizeOf p + sizeOf prio
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₃.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.δ (CategoryTheory.CategoryStruct.comp f.f₃.τ₁ h) =
    CategoryTheory.CategoryStruct.comp f.f₀.τ₃ (CategoryTheory.CategoryStruct.comp S₂.δ h)
-- Mathlib.Topology.Order.Lattice
continuous_sup : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Max L] [ContinuousSup L], Continuous fun p => p.1 ⊔ p.2
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- Category structure on a strict bicategory  -/
CategoryTheory.StrictBicategory.category : (B : Type u) →
  [inst : CategoryTheory.Bicategory B] → [CategoryTheory.Bicategory.Strict B] → CategoryTheory.Category.{v, u} B
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑m).size ≤ (↑(m.insert k v)).size
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.algebraMap_pow_isUnit : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] (n : ℕ), IsUnit ((algebraMap R S) x ^ n)
-- Mathlib.Tactic.ContinuousFunctionalCalculus
/-- A tactic used to automatically discharge goals relating to the continuous functional calculus,
specifically whether the element satisfies the predicate.  -/
cfcTac : Lean.ParserDescr
-- Mathlib.CategoryTheory.Yoneda
/-- The Yoneda embedding is faithful.  -/
CategoryTheory.Yoneda.yoneda_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.yoneda.Faithful
-- Mathlib.Order.Filter.Prod
Filter.mem_prod_top : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {s : Set (α × β)}, s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinable₁Singleton : ZFSet.Definable₁ fun x => {x}
-- Mathlib.Algebra.GroupWithZero.Range
/-- The map sending a pair of nonzero `r s : A` to the element `(v r)⁻¹ * (v s)`
of `ValueGroup₀ v`.  -/
MonoidWithZeroHom.ValueGroup₀.mk : {A : Type u_1} →
  {B : Type u_2} →
    [inst : MonoidWithZero A] →
      [inst_1 : CommGroupWithZero B] → (f : A →*₀ B) → [DecidablePred fun b => b = 0] → A → A → f.ValueGroup₀
-- Mathlib.Topology.UniformSpace.Basic
uniformity_hasBasis_closed : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsClosed V) id
-- Mathlib.RingTheory.RingInvo
instInhabitedRingInvo : (R : Type u_2) → [inst : CommRing R] → Inhabited (RingInvo R)
-- Batteries.Data.String.Lemmas
String.firstDiffPos.eq_1 : ∀ (a b : String), a.firstDiffPos b = String.firstDiffPos.loop a b (a.rawEndPos.min b.rawEndPos) 0
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂AssociatorHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
              [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
                [inst_3 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] →
                  Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.associator f g h).hom
-- Mathlib.Order.Interval.Set.Basic
/-- If `a ≤ b`, then `(b, +∞) ⊆ [a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in dense linear orders, use `Ioi_subset_Ici_iff`.  -/
Set.Ioi_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ioi a ⊆ Set.Ici b
-- Init.Data.List.Lemmas
List.replace_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [LawfulBEq α] {l : List α}, a ∉ l → l.replace a b = l
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonResolveSupport : Lean.FromJson Lean.Lsp.ResolveSupport
-- Lean.Elab.App
/-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general.  -/
Lean.Elab.Term.LValResolution.projIdx : Lean.Name → ℕ → Lean.Elab.Term.LValResolution
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_strictMono_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f → StrictMono (FirstOrder.Language.Substructure.map f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.bin.injEq : ∀ {w : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinOp)
  (rhs lhs_1 : Std.Tactic.BVDecide.BVExpr w) (op_1 : Std.Tactic.BVDecide.BVBinOp)
  (rhs_1 : Std.Tactic.BVDecide.BVExpr w),
  (lhs.bin op rhs = lhs_1.bin op_1 rhs_1) = (lhs = lhs_1 ∧ op = op_1 ∧ rhs = rhs_1)
-- Mathlib.Topology.AlexandrovDiscrete
nhdsKer_eq_iff_isOpen : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α}, nhdsKer s = s ↔ IsOpen s
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.liftPath.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p p_1 : E → X}
  (e_p : p = p_1) (cov : IsCoveringMap p) (γ γ_1 : C(↑unitInterval, X)) (e_γ : γ = γ_1) (e e_1 : E) (e_e : e = e_1)
  (γ_0 : γ 0 = p e), cov.liftPath γ e γ_0 = ⋯.liftPath γ_1 e_1 ⋯
-- Mathlib.Order.BooleanAlgebra.Basic
/-- See also `inf_sdiff_assoc`.  -/
sdiff_inf_right_comm : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y z : α), x \ z ⊓ y = (x ⊓ y) \ z
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_pos_iff : ∀ (n : ISize), 0 < n.toNatClampNeg ↔ 0 < n
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_fmod_iff_fmod_sub_eq_zero : ∀ {m n k : ℤ}, m.fmod n = k.fmod n ↔ (m - k).fmod n = 0
-- Mathlib.Logic.Function.Defs
/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`.  -/
Function.IsFixedPt.eq : ∀ {α : Type u₁} {f : α → α} {x : α}, Function.IsFixedPt f x → f x = x
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The *uncurried* composition morphism
  `x ⊗ (hom(x, y) ⊗ hom(y, z)) ⟶ (x ⊗ hom(x, y)) ⊗ hom(y, z) ⟶ y ⊗ hom(y, z) ⟶ z`.
The `C`-composition morphism will be defined as the adjoint transpose of this map.  -/
CategoryTheory.MonoidalClosed.compTranspose : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x y z : C) →
        [inst_2 : CategoryTheory.Closed x] →
          [inst_3 : CategoryTheory.Closed y] →
            CategoryTheory.MonoidalCategoryStruct.tensorObj x
                (CategoryTheory.MonoidalCategoryStruct.tensorObj (x ⟹ y) (y ⟹ z)) ⟶
              z
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.eval_ite : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {d l r : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred},
  Std.Tactic.BVDecide.BVLogicalExpr.eval assign (d.ite l r) =
    bif Std.Tactic.BVDecide.BVLogicalExpr.eval assign d then Std.Tactic.BVDecide.BVLogicalExpr.eval assign l
    else Std.Tactic.BVDecide.BVLogicalExpr.eval assign r
-- Init.Omega.IntList
/-- Division of an `IntList` by a integer.  -/
Lean.Omega.IntList.sdiv : Lean.Omega.IntList → ℤ → Lean.Omega.IntList
-- Std.Http.Protocol.H1.Parser
/-- Returns `true` if `c` is a valid reason-phrase byte (`HTAB / SP / VCHAR`, strict ASCII-only).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.isReasonPhraseByte : UInt8 → Bool
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The profinite completion of `G` as a projective limit.  -/
ProfiniteAddGrp.ProfiniteCompletion.completion : AddGrpCat → ProfiniteAddGrp.{u}
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- If `it` plausibly yields in its immediate next step, the successor iterator being `it'`, and
if `step` is a plausible `n`-th output step of `it'`, then `step` is a plausible `n + 1`-th
output step of `it`.
 -/
Std.IterM.IsPlausibleNthOutputStep.yield : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {n : ℕ} {it it' : Std.IterM m β} {out : β}
  {step : Std.IterStep (Std.IterM m β) β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) →
    Std.IterM.IsPlausibleNthOutputStep n it' step → Std.IterM.IsPlausibleNthOutputStep (n + 1) it step
-- Lean.Elab.Command
Lean.Elab.Command.withFreshMacroScope : {α : Type} → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The logarithmic embedding of the units (seen as an `Additive` group).  -/
NumberField.Units.logEmbedding : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Additive (NumberField.RingOfIntegers K)ˣ →+ NumberField.Units.dirichletUnitTheorem.logSpace K
-- Mathlib.FieldTheory.PurelyInseparable.Basic
Field.Emb.cardinal_separableClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  Cardinal.mk (Field.Emb F ↥(separableClosure F E)) = Cardinal.mk (Field.Emb F E)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide around a point (except possibly at a single point `y`), then it is
equivalent to be differentiable within one or the other set.  -/
mdifferentiableWithinAt_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M}
  (y : M), s =ᶠ[nhdsWithin x {y}ᶜ] t → (MDiffAt[s] f x ↔ MDiffAt[t] f x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superpose_cert.eq_1 : ∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.superpose_cert k₁ m₁ p₁ k₂ m₂ p₂ p =
    ((Lean.Grind.CommRing.Poly.mulMon_k k₁ m₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂)).beq' p
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- In the definition of `(Γ₀.obj K).obj Δ` as a direct sum indexed by `A : Splitting.IndexSet Δ`,
the summand `summand K Δ A` is `K.X A.1.len`.  -/
AlgebraicTopology.DoldKan.Γ₀.Obj.summand : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ChainComplex C ℕ → (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ → C
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
/-- If `A` is a right `B`-localizing triangulated subcategory in the sense of Verdier,
then the induced functor between the localizations with respect to `(B.inverseImage A.ι).trW`
and `B.trW` is fully faithful.  -/
CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fullyFaithful : {C : Type u_1} →
  {D₁ : Type u_3} →
    {D₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} D₁] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D₂] →
            (A B : CategoryTheory.ObjectProperty C) →
              [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
                [inst_4 : CategoryTheory.HasShift C ℤ] →
                  [inst_5 : CategoryTheory.Preadditive C] →
                    [inst_6 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_7 : CategoryTheory.Pretriangulated C] →
                        [CategoryTheory.IsTriangulated C] →
                          [inst_9 : A.IsTriangulated] →
                            [B.IsTriangulated] →
                              [B.IsClosedUnderIsomorphisms] →
                                [A.IsVerdierRightLocalizing B] →
                                  {L₁ : CategoryTheory.Functor A.FullSubcategory D₁} →
                                    {L₂ : CategoryTheory.Functor C D₂} →
                                      {F : CategoryTheory.Functor D₁ D₂} →
                                        [L₁.IsLocalization (B.inverseImage A.ι).trW] →
                                          [L₂.IsLocalization B.trW] → (L₁.comp F ≅ A.ι.comp L₂) → F.FullyFaithful
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N)
  (e_x : x = x_1) {d : ℕ} (hd : x.dim = d) (a a_1 : Fin (d + 1)),
  a = a_1 → SSet.prodStdSimplex.pairingCore.IsIndex x hd a = SSet.prodStdSimplex.pairingCore.IsIndex x_1 ⋯ a_1
-- Lean.Server.References
/-- Adds `ref` to the `RefInfo` corresponding to `ref.ident` in `self`. See `RefInfo.addRef`.  -/
Lean.Server.ModuleRefs.addRef : Lean.Server.ModuleRefs → Lean.Server.Reference → Lean.Server.ModuleRefs
-- Mathlib.Order.SuccPred.CompleteLinearOrder
exists_eq_iInf_of_not_isPredPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLinearOrder α] {f : ι → α},
  ¬Order.IsPredPrelimit (⨅ i, f i) → ∃ i, f i = ⨅ i, f i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.min?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.add_assoc : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (x y z : OreLocalization S X), x + y + z = x + (y + z)
-- Mathlib.Topology.Algebra.UniformConvergence
instSMulCommClassUniformOnFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [inst : SMul M β] [inst_1 : SMul N β]
  [SMulCommClass M N β], SMulCommClass M N (UniformOnFun α β 𝔖)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_int_mul_two_pi_mul_I : ∀ (n : ℤ), Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.posSemidef_add : ∀ {m : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [AddLeftMono R]
  {A B : Matrix m m R}, A.PosSemidef → B.PosDef → (A + B).PosDef
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- Return the `apply` tactic that performs the application.  -/
_private.Mathlib.Tactic.ClickSuggestions.ApplyAt.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax : Mathlib.Tactic.ClickSuggestions.ApplyAtLemma → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Lean.TSyntax `tactic)
-- Lean.Data.Json.Parser
Lean.Json.Parser.natCoreNumDigits : ℕ → ℕ → Std.Internal.Parsec.String.Parser (ℕ × ℕ)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- Copy an additive subsemigroup replacing `carrier` with a set that is equal to it.  -/
AddSubsemigroup.copy : {M : Type u_1} → [inst : Add M] → (S : AddSubsemigroup M) → (s : Set M) → s = ↑S → AddSubsemigroup M
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unfoldRule.inj : ∀ {r r_1 : Aesop.UnfoldRule}, Aesop.BaseRuleSetMember.unfoldRule r = Aesop.BaseRuleSetMember.unfoldRule r_1 → r = r_1
-- Mathlib.Data.Num.ZNum
ZNum.abs_toZNum : ∀ (n : Num), n.toZNum.abs = n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, a ∈ t)
-- Init.Data.Array.Zip
Array.map_fst_zip : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β}, as.size ≤ bs.size → Array.map Prod.fst (as.zip bs) = as
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.srangeRestrict_surjective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  Function.Surjective ⇑(NonUnitalRingHom.srangeRestrict f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictDerivAt.const_cpow : ∀ {f : ℂ → ℂ} {f' x c : ℂ},
  HasStrictDerivAt f f' x → c ≠ 0 ∨ f x ≠ 0 → HasStrictDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x
-- Mathlib.Order.Filter.Ker
Filter.ker_surjective : ∀ {α : Type u_2}, Function.Surjective Filter.ker
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_neg : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)), f • -g = -(f • g)
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.eq_1 : ∀ {α : Type u} (s : Set α), s.Infinite = ¬s.Finite
-- Init.Data.Float.Model.Unpacked.Operations.OfScientific
/-- Computes `m * 10 ^ e`.  -/
Float.Model.UnpackedFloat.ofScientific : Float.Model.Format → ℕ → ℤ → Float.Model.UnpackedFloat