mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (z : F.obj a ⊕ G.obj a),
  (CategoryTheory.FunctorToTypes.binaryCoproductEquiv F G a).symm z =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a)) z
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.dec.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (n n_1 : ℕ),
      n = n_1 →
        ∀ (check check_1 : Bool),
          check = check_1 →
            ∀ (persistent persistent_1 : Bool),
              persistent = persistent_1 →
                ∀ (objs? objs?_1 : Option ℕ),
                  objs? = objs?_1 →
                    ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
                      k = k_1 →
                        ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
                          Lean.Compiler.LCNF.Code.dec fvarId n check persistent objs? k h =
                            Lean.Compiler.LCNF.Code.dec fvarId_1 n_1 check_1 persistent_1 objs?_1 k_1 h
-- Mathlib.CategoryTheory.Monad.Basic
/-- The data of a comonad on C consists of an endofunctor G together with natural transformations
`ε : G ⟶ 𝟭 C` and `δ : G ⟶ G ⋙ G` satisfying three equations:
- `δ_X ≫ G δ_X = δ_X ≫ δ_(GX)` (coassociativity)
- `δ_X ≫ ε_(GX) = 1_X` (left counit)
- `δ_X ≫ G ε_X = 1_X` (right counit)
 -/
CategoryTheory.Comonad : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type (max u₁ v₁)
-- Mathlib.Combinatorics.Colex
/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small.  -/
Finset.Colex.forall_lt_mono : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} {a : α},
  toColex s ≤ toColex t → (∀ b ∈ t, b < a) → ∀ b ∈ s, b < a
-- Mathlib.RingTheory.Congruence.Defs
RingCon.sub : ∀ {S : Type u_2} [inst : AddGroup S] [inst_1 : Mul S] (t : RingCon S) {a b c d : S}, t a b → t c d → t (a - c) (b - d)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinfOfTrivial_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  (groupHomology.H1CoresCoinfOfTrivial A S).g = groupHomology.map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1
-- Std.Data.ByteSlice
/-- The empty byte slice.

This empty byte slice is backed by an empty byte array.
 -/
ByteSlice.empty : ByteSlice
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpId_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ),
  (CategoryTheory.Functor.leftOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- A morphism `k : W ⟶ X` satisfying `k ≫ f = k ≫ g` factors through the weak equalizer of
`f` and `g` via `weakEqualizer.lift : W ⟶ weakEqualizer f g`.  -/
CategoryTheory.Limits.weakEqualizer.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] →
          {W : C} →
            (k : W ⟶ X) →
              CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
                (W ⟶ CategoryTheory.Limits.weakEqualizer f g)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- a family of objects which cover the terminal object  -/
SheafOfModules.QuasicoherentData.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → (self : M.QuasicoherentData) → self.I → C
-- Mathlib.Data.Sigma.Order
Sigma.instLE_mathlib : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → LE (α i)] → LE ((i : ι) × α i)
-- Mathlib.RingTheory.Localization.AsSubring
Localization.mem_range_mapToFractionRing_iff : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] (B : Type u_3) [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (hS : S ≤ nonZeroDivisors A) (x : K),
  x ∈ (Localization.mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩
-- Mathlib.Topology.Instances.TrivSqZeroExt
/-- `TrivSqZeroExt.fst` as a continuous linear map.  -/
TrivSqZeroExt.fstCLM : (R : Type u_3) →
  (M : Type u_4) →
    [inst : TopologicalSpace R] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : CommSemiring R] →
          [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → StrongDual R (TrivSqZeroExt R M)
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- The conditional (Lebesgue) expectation `P⁻[X|mΩ]` is defined uniquely as an `mΩ`-measurable
function up to `P`-ae equality by its (Lebesgue) integral over all `mΩ`-measurable sets.  -/
MeasureTheory.ae_eq_condLExp : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {Y : Ω → ENNReal} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal),
  Measurable Y →
    (∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P) → Y =ᵐ[P] P⁻[X | mΩ]
-- Init.System.ST
ST.Prim.Ref.ptrEq : {σ α : Type} → ST.Ref σ α → ST.Ref σ α → ST σ Bool
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_ne_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.injectiveDimension X ≠ ⊤ ↔ ∃ n, CategoryTheory.HasInjectiveDimensionLE X n
-- Lean.Elab.Tactic.ElabTerm
/-- Elaborates `stx` and collects the `MVarId`s of any holes that were created during elaboration.

With `allowNaturalHoles := false` (the default), any new natural holes (`_`) which cannot
be synthesized during elaboration cause `elabTermWithHoles` to fail. (Natural goals appearing in
`stx` which were created prior to elaboration are permitted.)

Unnamed `MVarId`s are renamed to share the tag `parentTag?` (or the main goal's tag if `parentTag?` is `none`).
If multiple unnamed goals are encountered, `tagSuffix` is appended to this tag along with a numerical index.

Note:
* Previously-created `MVarId`s which appear in `stx` are not returned.
* All parts of `elabTermWithHoles` operate at the current `MCtxDepth`, and therefore may assign
metavariables.
* When `allowNaturalHoles := true`, `stx` is elaborated under `withAssignableSyntheticOpaque`,
meaning that `.syntheticOpaque` metavariables might be assigned during elaboration. This is a
consequence of the implementation.  -/
Lean.Elab.Tactic.elabTermWithHoles : Lean.Syntax →
  Option Lean.Expr →
    Lean.Name →
      optParam Bool false → optParam (Option Lean.Name) none → Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)
-- Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
instHasExtModuleCatOfSmall : ∀ (R : Type u) [inst : Ring R] [Small.{v, u} R], CategoryTheory.HasExt (ModuleCat R)
-- Mathlib.Logic.Relation
Relation.instTransReflTransGen_1 : {α : Type u_1} → {r : α → α → Prop} → Trans (Relation.ReflTransGen r) r (Relation.ReflTransGen r)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.mk.inj : ∀ {α : Type u} {inst : Group α} {toTopologicalSpace : TopologicalSpace α} {toIsTopologicalGroup : IsTopologicalGroup α}
  {toTopologicalSpace_1 : TopologicalSpace α} {toIsTopologicalGroup_1 : IsTopologicalGroup α},
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalGroup := toIsTopologicalGroup_1 } →
    toTopologicalSpace = toTopologicalSpace_1
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.image_mem_nhds : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ {s : Set X}, s ∈ nhds x → ↑e '' s ∈ nhds (↑e x)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_pow_eq_monomial : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.X ^ n = (Polynomial.monomial n) 1
-- Std.Data.TreeMap.DecidableEquiv
Std.TreeMap.instDecidableEquivOfTransCmpOfLawfulEqCmpOfLawfulBEq : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] → [inst : BEq β] → [LawfulBEq β] → {t₁ t₂ : Std.TreeMap α β cmp} → Decidable (t₁.Equiv t₂)
-- Mathlib.RingTheory.EuclideanDomain
EuclideanDomain.span_gcd : ∀ {α : Type u_1} [inst : EuclideanDomain α] [inst_1 : DecidableEq α] (x y : α),
  Ideal.span {EuclideanDomain.gcd x y} = Ideal.span {x, y}
-- Mathlib.Order.Category.BddDistLat
BddDistLat.mk.sizeOf_spec : ∀ (toDistLat : DistLat) [isBoundedOrder : BoundedOrder ↑toDistLat],
  sizeOf { toDistLat := toDistLat, isBoundedOrder := isBoundedOrder } = 1 + sizeOf toDistLat + sizeOf isBoundedOrder
-- Mathlib.CategoryTheory.Sites.Canonical
/-- The yoneda functor into the sheaf category is fully faithful  -/
CategoryTheory.GrothendieckTopology.yonedaFullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) → [inst_1 : J.Subcanonical] → J.yoneda.FullyFaithful
-- Aesop.Tree.Data
Aesop.TreeSpec.mk : (Goal Rapp MVarCluster : Type) →
  (Aesop.GoalData Rapp MVarCluster → Goal) →
    (Goal → Aesop.GoalData Rapp MVarCluster) →
      (Aesop.RappData Goal MVarCluster → Rapp) →
        (Rapp → Aesop.RappData Goal MVarCluster) →
          (Aesop.MVarClusterData Goal Rapp → MVarCluster) →
            (MVarCluster → Aesop.MVarClusterData Goal Rapp) → Aesop.TreeSpec
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- The Jacobi sum of two multiplicative characters on a nontrivial finite commutative ring `F`
can be written as a sum over `F \ {0,1}`.  -/
jacobiSum_eq_sum_sdiff : ∀ {F : Type u_1} {R : Type u_2} [inst : CommRing F] [Nontrivial F] [inst_2 : Fintype F] [inst_3 : DecidableEq F]
  [inst_4 : CommRing R] (χ ψ : MulChar F R), jacobiSum χ ψ = ∑ x ∈ Finset.univ \ {0, 1}, χ x * ψ (1 - x)
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_zero : ∀ {α : Type u_1} (s : Finset α), Finset.powersetCard 0 s = {∅}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey? k' = some k
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_setOfPred_prime`. -/
schnirelmannDensity_setOf_prime : schnirelmannDensity (Set.ofPred Nat.Prime) = 0
-- Mathlib.Data.Fintype.Card
/-- Note: this lemma is specifically about `Fintype.ofSubsingleton`. For a statement about
arbitrary `Fintype` instances, use either `Fintype.card_le_one_iff_subsingleton` or
`Fintype.card_unique`.  -/
Fintype.card_ofSubsingleton : ∀ {α : Type u_1} (a : α) [inst : Subsingleton α], Fintype.card α = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.mk.sizeOf_spec : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (SSet.stdSimplex.obj { len := 1 }) ⟶ Y)
  (h₀ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₀ h = f.map) SSet.RelativeMorphism.Homotopy.h₀._autoParam)
  (h₁ : autoParam (CategoryTheory.CategoryStruct.comp SSet.ι₁ h = g.map) SSet.RelativeMorphism.Homotopy.h₁._autoParam)
  (rel :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.ι (SSet.stdSimplex.obj { len := 1 })) h =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.SemiCartesianMonoidalCategory.fst A.toSSet (SSet.stdSimplex.obj { len := 1 }))
          (CategoryTheory.CategoryStruct.comp φ B.ι))
      SSet.RelativeMorphism.Homotopy.rel._autoParam),
  sizeOf { h := h, h₀ := h₀, h₁ := h₁, rel := rel } = 1 + sizeOf h + sizeOf h₀ + sizeOf h₁ + sizeOf rel
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β}, (∀ᵐ (a : α) ∂μ, κ a = η a) → μ.bind ⇑κ = μ.bind ⇑η
-- Mathlib.Order.LatticeIntervals
Set.Iic.coe_inf : ∀ {α : Type u_1} {a : α} [inst : SemilatticeInf α] {x y : ↑(Set.Iic a)}, ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofScientific_im : ∀ {K : Type u_1} [inst : RCLike K] (m : ℕ) (s : Bool) (e : ℕ), RCLike.im (OfScientific.ofScientific m s e) = 0
-- Batteries.Data.AssocList
Batteries.AssocList.length_nil : ∀ {α : Type u_1} {β : Type u_2}, Batteries.AssocList.nil.length = 0
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.ext_iff : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst_1 : Monoid G} {M N : Action V G}
  {x y : M.Hom N}, x = y ↔ x.hom = y.hom
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      (Std.DHashMap.Internal.toListModel (↑(m₁.inter m₂)).buckets).Perm
        (List.filter (fun p => Std.Internal.List.containsKey p.fst (Std.DHashMap.Internal.toListModel (↑m₂).buckets))
          (Std.DHashMap.Internal.toListModel (↑m₁).buckets))
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coe_mk' : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier)
  (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
  (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
  (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier),
  ↑(TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right) = carrier
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mk.inj : ∀ {α : Type u_1} {inst : CompleteLattice α} {toSublattice : Sublattice α}
  {sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier}
  {sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier}
  {toSublattice_1 : Sublattice α}
  {sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier}
  {sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier},
  { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' } =
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 } →
    toSublattice = toSublattice_1
-- Init.TacticsExtra
/-- Rewrites with the given rules, normalizing casts prior to each step.
 -/
Lean.Parser.Tactic.tacticRw_mod_cast___ : Lean.ParserDescr
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `C` and `g` tends to `atTop` then `f + g` tends to `atTop`.  -/
Filter.Tendsto.add_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_triple : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {w x y z : M},
  w ∈ Submodule.span R {x, y, z} ↔ ∃ a b c, a • x + b • y + c • z = w
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F),
  ContinuousAlternatingMap.alternatizeUncurryFin (↑↑(ContinuousAlternatingMap.constOfIsEmptyLIE 𝕜 E F (Fin 0)) ∘SL f) =
    (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F 0) f
-- Lean.Util.PPExt
Lean.ppGoal : Lean.PPContext → Lean.MVarId → BaseIO Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_desc_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {P : C} (p : (b : J) → f b ⟶ P) (j : J) {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc p) h) =
    CategoryTheory.CategoryStruct.comp (p j) h
-- Mathlib.Control.Fold
Traversable.foldr_toList : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (f : α → β → β) (xs : t α) (x : β),
  Traversable.foldr f x xs = List.foldr f x (Traversable.toList xs)
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The higher derived functors vanish on injective objects.  -/
CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) (X : C)
  [CategoryTheory.Injective X], CategoryTheory.Limits.IsZero ((F.rightDerived (n + 1)).obj X)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {Z : D} (h : F.obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0)
          (CategoryTheory.CategoryStruct.comp (Q.fromLeftDerivedZero' F) h) =
        CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (CategoryTheory.CategoryStruct.comp (F.map f) h)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasSum.update : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α} {a₁ : α} [L.LeAtTop],
  HasSum f a₁ L → ∀ (b : β) [inst_4 : DecidableEq β] (a : α), HasSum (Function.update f b a) (a - f b + a₁) L
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.ιPi.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right],
  CategoryTheory.Limits.Multiequalizer.ιPi I =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.isoEqualizer I).hom
      (CategoryTheory.Limits.equalizer.ι I.fstPiMap I.sndPiMap)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The difference between two points (reversed) lies in their `vectorSpan`.  -/
vsub_rev_mem_vectorSpan_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), p₂ -ᵥ p₁ ∈ vectorSpan k {p₁, p₂}
-- Lean.Meta.Match.Basic
/-- Indices of previous alternatives that this alternative expects a not-that-proofs.
(When producing a splitter, and in the future also for source-level overlap hypotheses.)
 -/
Lean.Meta.Match.Alt.notAltIdxs : Lean.Meta.Match.Alt → Array ℕ
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.useWHNFCache : Lean.Expr → Lean.MetaM Bool
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.cons : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  (startPos middlePos endPos : s.Pos),
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos middlePos →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat middlePos endPos →
      String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIco : ∀ {α : Type u_1} {f : ℤ → α} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [ContinuousAdd α] [T2Space α],
  Summable f (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => -f ↑N) Filter.atTop (nhds 0) →
      ∑'[SummationFilter.symmetricIco ℤ] (b : ℤ), f b = ∑'[SummationFilter.symmetricIcc ℤ] (b : ℤ), f b
-- Mathlib.Algebra.Group.Opposite
AddOpposite.addCommute_unop : ∀ {α : Type u_1} [inst : Add α] {x y : αᵃᵒᵖ}, AddCommute (AddOpposite.unop x) (AddOpposite.unop y) ↔ AddCommute x y
-- Mathlib.RingTheory.Finiteness.Basic
Ideal.fg_top : ∀ (R : Type u_1) [inst : Semiring R], ⊤.FG
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Triplet.mk.sizeOf_spec : ∀ {n : ℤ} (p q : ℤ) (hpq : p + n = q), sizeOf { p := p, q := q, hpq := hpq } = 1 + sizeOf p + sizeOf q + sizeOf hpq
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] [inst_4 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β}
  {it₂ it₂' : Std.IterM m γ} {b : γ},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    (Std.IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.yield (Std.IterM.flatMapAfterM f it₁ (some it₂')) b)
-- Std.Time.Date.ValidDate
/-- Transforms a tuple of a `Month` and a `Day` into a `Day.Ordinal.OfYear`.
 -/
Std.Time.ValidDate.dayOfYear : {leap : Bool} → Std.Time.ValidDate leap → Std.Time.Day.Ordinal.OfYear leap
-- Mathlib.Algebra.Order.Ring.Abs
abs_unit_intCast : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a : ℤˣ), |↑↑a| = 1
-- Init.Data.Dyadic.Basic
Dyadic.instOfNat : (n : ℕ) → OfNat Dyadic n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM_eq_toList_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toList =
    (Std.IterM.mapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toList