mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Equiv.Prod
/-- Type product is right distributive with respect to type sum up to an equivalence.  -/
Equiv.sumProdDistrib : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (α ⊕ β) × γ ≃ α × γ ⊕ β × γ
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.mk : Lean.Elab.ElabInfo → Lean.LocalContext → Option Lean.Expr → Lean.Expr → Bool → Bool → Lean.Elab.TermInfo
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a ≍ b`.
It assumes `a` and `b` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkHEqProof : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Order.RelClasses
instReflGe : ∀ {α : Type u} [inst : Preorder α], Std.Refl fun x1 x2 => x2 ≤ x1
-- Std.Tactic.Do.Syntax
/-- Like `refine`, but operating on stateful `Std.Do.SPred` goals.
```lean
example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
  mintro ⟨HP, HQ, HR⟩
  mrefine ⟨HP, HR⟩

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mrefine ⟨⌜42⌝, H⟩
```
 -/
Lean.Parser.Tactic.mrefineError : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constToList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.toList t₁ = Std.DTreeMap.Raw.Const.toList t₂
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Given a `UpperSet` of `MulArchimedeanClass`,
all group elements belonging to these classes form a subsemigroup.
This is not yet a subgroup because it doesn't contain the identity if `s = ⊤`.  -/
MulArchimedeanClass.subsemigroup : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → UpperSet (MulArchimedeanClass M) → Subsemigroup M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)}, t.size ≤ (Std.DTreeMap.Const.insertMany t l).size
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_vsub_const_iff`. -/
Sbtw.vsub_const : ∀ {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] {x y z : P} (p : P), Sbtw R x y z → Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_neg : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R ≃+* S)
  (x : R), f (-x) = -f x
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.nontrivial : ∀ {R : Type u} [inst : CommSemiring R] (p : PrimeSpectrum R), Nontrivial R
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.State.mk.inj : ∀ {congrThms : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem} {simp : Lean.Meta.Simp.State}
  {lastTag : Lean.Name} {counters : Lean.Meta.Grind.Counters} {splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo}
  {ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo}
  {lawfulEqCmpMap reflCmpMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)}
  {anchors : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64}
  {instanceMap : Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem}
  {congrThms_1 : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem}
  {simp_1 : Lean.Meta.Simp.State} {lastTag_1 : Lean.Name} {counters_1 : Lean.Meta.Grind.Counters}
  {splitDiags_1 : Lean.PArray Lean.Meta.Grind.SplitDiagInfo}
  {ematchDiags_1 : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo}
  {lawfulEqCmpMap_1 reflCmpMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)}
  {anchors_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64}
  {instanceMap_1 : Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem},
  { congrThms := congrThms, simp := simp, lastTag := lastTag, counters := counters, splitDiags := splitDiags,
        ematchDiags := ematchDiags, lawfulEqCmpMap := lawfulEqCmpMap, reflCmpMap := reflCmpMap, anchors := anchors,
        instanceMap := instanceMap } =
      { congrThms := congrThms_1, simp := simp_1, lastTag := lastTag_1, counters := counters_1,
        splitDiags := splitDiags_1, ematchDiags := ematchDiags_1, lawfulEqCmpMap := lawfulEqCmpMap_1,
        reflCmpMap := reflCmpMap_1, anchors := anchors_1, instanceMap := instanceMap_1 } →
    congrThms = congrThms_1 ∧
      simp = simp_1 ∧
        lastTag = lastTag_1 ∧
          counters = counters_1 ∧
            splitDiags = splitDiags_1 ∧
              ematchDiags = ematchDiags_1 ∧
                lawfulEqCmpMap = lawfulEqCmpMap_1 ∧
                  reflCmpMap = reflCmpMap_1 ∧ anchors = anchors_1 ∧ instanceMap = instanceMap_1
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The type of morphisms in `ProfiniteGrp`.  -/
ProfiniteGrp.Hom : ProfiniteGrp.{u} → ProfiniteGrp.{u} → Type u
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.mul_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C), CategoryTheory.MonObj.mul = M.μ
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.prodMk_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] [MeasureTheory.SFinite ν] {f : α × β → X},
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    ∀ᵐ (x : α) ∂μ, MeasureTheory.AEStronglyMeasurable (fun y => f (x, y)) ν
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.comap_map : ∀ {α : Type u_1} {β : Type u_3} {f : α → β},
  Function.Injective f →
    ∀ (m : MeasureTheory.OuterMeasure α),
      (MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.map f) m) = m
-- Init.Data.List.Attach
List.getLast_attach : ∀ {α : Type u_1} {xs : List α} (h : xs.attach ≠ []), xs.attach.getLast h = ⟨xs.getLast ⋯, ⋯⟩
-- Init.Data.Nat.Bitwise.Lemmas
Nat.ge_two_pow_of_testBit : ∀ {i x : ℕ}, x.testBit i = true → x ≥ 2 ^ i
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instHasZeroObject : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.Grp C)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (self : CategoryTheory.Mon C) → CategoryTheory.MonObj self.X
-- Mathlib.Data.List.Cycle
List.next_getLast_eq_head_of_notMem_dropLast : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} (hl : l ≠ []),
  l.getLast hl ∉ l.dropLast → l.next (l.getLast hl) ⋯ = l.head hl
-- Mathlib.Data.Matrix.Mul
RingHom.map_matrix_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [inst : Fintype n]
  [inst_1 : NonAssocSemiring α] [inst_2 : NonAssocSemiring β] (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o)
  (f : α →+* β), f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The `V`-morphism from `X ⟶[V] Y` to `F.obj X ⟶[V] F.obj Y`, for all `X Y : C`  -/
CategoryTheory.EnrichedFunctor.map : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              (self : CategoryTheory.EnrichedFunctor V C D) → (X Y : C) → (X ⟶[V] Y) ⟶ self.obj X ⟶[V] self.obj Y
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupSeminormClass.toSeminormedGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : Group α] [inst_2 : GroupSeminormClass F α ℝ] (f : F)
  (x : α), ‖x‖ = f x
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
WfDvdMonoid.of_exists_prime_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α],
  (∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a) → WfDvdMonoid α
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_trans_trans : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (f : β ≃ α) (p : Equiv.Perm α) (g : α ≃ β),
  Equiv.Perm.sign (f.trans (Equiv.trans p g)) = Equiv.Perm.sign p * Equiv.Perm.sign (f.trans g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_false_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = true → t.isEmpty = false
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 3],
  W.j = ↑W.Δ'⁻¹ * W.b₂ ^ 6
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.isoMk_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : Algebra R X}
  {x_3 : Algebra R Y} (e : X ≃ₐ[R] Y), (CommAlgCat.isoMk e).hom = CommAlgCat.ofHom ↑e
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.comp_apply : ∀ {X Y T : AddSemigrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.le_traceDual_iff_map_le_one : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I J : Submodule B L},
  I ≤ Submodule.traceDual A K J ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A (I * J)) ≤ 1
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app_assoc : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂}
  (h : (DerivedCategory.singleFunctor C₂ 0).obj (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app X) h) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)) h
-- Mathlib.Logic.Equiv.Finset
Denumerable.isChain_cons_raise'_of_lt : ∀ (l : List ℕ) {m n : ℕ}, m < n → List.IsChain (fun x1 x2 => x1 < x2) (m :: Denumerable.raise' l n)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y y' : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F y y' → RingCat.Colimits.Relation F (x.add y) (x.add y')
-- Mathlib.Topology.Algebra.ConstMulAction
nhds_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → ∀ (x : α), nhds (c • x) = c • nhds x
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instUnique : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Unique A] → Unique (CStarMatrix m n A)
-- Lean.Meta.Tactic.Grind.Types
/-- Lookahead "case-splits".  -/
Lean.Meta.Grind.Split.State.lookaheads : Lean.Meta.Grind.Split.State → List Lean.Meta.Grind.SplitInfo
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The map `π₀.mk : X _⦋0⦌ ⟶ π₀ X` for all simplicial sets `X`,
as a natural transformation.  -/
SSet.toπ₀NatTrans : SSet.evaluation.obj (Opposite.op { len := 0 }) ⟶ SSet.π₀Functor
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.instHasRightResolutionsOppositeOpOpOfHasLeftResolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.HasLeftResolutions],
  Φ.op.HasRightResolutions
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtNormed_unit_length_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E}
  (n : ι), LinearIndependent 𝕜 (f ∘ Subtype.val) → ‖InnerProductSpace.gramSchmidtNormed 𝕜 f n‖ = 1
-- Mathlib.GroupTheory.DivisibleHull
/-- See `archimedeanClassOrderIso_symm_apply` for public API.  -/
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.aux_archimedeanClassMk_mk : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (m : M) (s : ℕ+),
  ArchimedeanClass.mk (DivisibleHull.mk m s) = (DivisibleHull.archimedeanClassOrderHom✝ M) (ArchimedeanClass.mk m)
-- Mathlib.Algebra.Group.Hom.Basic
/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial,
stated as an iff on the triviality of the kernel.
For the implication, see `injective_iff_map_eq_one`.  -/
injective_iff_map_eq_one' : ∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : Group G] [inst_1 : MulOneClass H] [inst_2 : FunLike F G H]
  [MonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 ↔ a = 1
-- Mathlib.Data.Finset.Image
Set.MapsTo.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β), Set.MapsTo f s t = ∀ ⦃x : α⦄, x ∈ s → f x ∈ t
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_pi_closedBall : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [inst_3 : (i : ι) → MetricSpace (α i)] (x : (i : ι) → α i)
  {r : ℝ}, 0 ≤ r → MeasureTheory.volume (Metric.closedBall x r) = ∏ i, MeasureTheory.volume (Metric.closedBall (x i) r)
-- Init.Control.Lawful.Instances
OptionT.run_bind : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {x : OptionT m α} (f : α → OptionT m β) [inst : Monad m],
  (x >>= f).run = Option.elimM x.run (pure none) fun x => (f x).run
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isOpen_induction : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {P : Set α → Prop},
  TopologicalSpace.IsTopologicalBasis B →
    (∀ b ∈ B, P b) → (∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)) → ∀ {s : Set α}, IsOpen s → P s
-- Mathlib.MeasureTheory.Measure.AddContent
/-- An `addContent C` on a `SetSemiring C` is monotone.  -/
MeasureTheory.addContent_mono : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} [inst_1 : PartialOrder G] [CanonicallyOrderedAdd G],
  MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → s ⊆ t → m s ≤ m t
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dCokernelSequence._auto_5),
  (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₂ = X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Pi.compRightL_apply : ∀ (R : Type u_1) [inst : Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)] {α : Type u_6} (f : α → ι)
  (v : (i : ι) → φ i) (i : α), (Pi.compRightL R φ f) v i = v (f i)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.refl_apply : ∀ (X : Type u_7) [inst : TopologicalSpace X], ↑(OpenPartialHomeomorph.refl X) = id
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_inj : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A B : Matrix m n R}, A.vec = B.vec ↔ A = B
-- Mathlib.Probability.Distributions.Bernoulli
/-- The **Bernoulli distribution** over an arbitrary measurable space `X`.
Given `x y : X` and `p : I` (`I` is the `unitInterval`),
it is the measure which gives mass `p` to `{x}` and `1 - p` to `{y}`.  -/
ProbabilityTheory.bernoulliMeasure : {X : Type u_1} → [inst : MeasurableSpace X] → X → X → ↑unitInterval → MeasureTheory.Measure X
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i))`.  -/
PiCountable.pseudoMetricSpace : {ι : Type u_2} →
  [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → PseudoMetricSpace (F i)] → PseudoMetricSpace ((i : ι) → F i)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) (isImage : CategoryTheory.Limits.IsImage F)
  (F_1 : CategoryTheory.Limits.MonoFactorisation f) (isImage_1 : CategoryTheory.Limits.IsImage F_1),
  ({ F := F, isImage := isImage } = { F := F_1, isImage := isImage_1 }) = (F = F_1 ∧ isImage ≍ isImage_1)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover),
  (∀ (i : 𝒰.toPreZeroHypercover.1), P (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i)) → P f
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonnegative.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)} (pf : Q(0 ≤ «$e»)),
  sizeOf (Mathlib.Meta.Positivity.Strictness.nonnegative pf) = 1 + sizeOf pα + sizeOf pf
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.map.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p p_1 : CategoryTheory.Functor 𝒳 𝒮) (e_p : p = p_1) {R S : 𝒮} {a b : 𝒳} (f f_1 : R ⟶ S) (e_f : f = f_1)
  (φ φ_1 : a ⟶ b) (e_φ : φ = φ_1) [inst_2 : p.IsCartesian f φ] {a' : 𝒳} (φ' φ'_1 : a' ⟶ b) (e_φ' : φ' = φ'_1)
  [inst_3 : p.IsHomLift f φ'],
  CategoryTheory.Functor.IsCartesian.map p f φ φ' = CategoryTheory.Functor.IsCartesian.map p_1 f_1 φ_1 φ'_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constGet!_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β] {k : α},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DHashMap.Raw.Const.get! m₁ k = Std.DHashMap.Raw.Const.get! m₂ k
-- Mathlib.MeasureTheory.Measure.Stieltjes
botSet_eq_singleton_of_isBot : ∀ {R : Type u_1} [inst : LinearOrder R] {x : R}, IsBot x → botSet = {x}
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.coe_injective : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} [Nontrivial α], Function.Injective Combinatorics.Subspace.toFun
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_injective : ∀ {α : Type u}, Function.Injective List.cyclicPermutations
-- Init.Data.Iterators.Basic
Std.IterStep.successor_skip : ∀ {α : Type u} {β : Type w} {it : α}, (Std.IterStep.skip it).successor = some it
-- Mathlib.Data.Fin.Basic
/-- `Fin.mk_zero` in `Lean` only applies in `Fin (n + 1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
 -/
Fin.mk_zero' : ∀ (n : ℕ) [inst : NeZero n], ⟨0, ⋯⟩ = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.δ_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n)
  (n' : ℤ) (hn' : n + 1 = n'),
  CochainComplex.HomComplex.δ m n (CochainComplex.mappingCocone.descCochain φ α β h) =
    (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCocone.fst φ)).comp
        (CochainComplex.HomComplex.δ m n α + m.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ +
      (CochainComplex.mappingCocone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯
-- Mathlib.Data.List.AList
AList.perm_replace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : AList β},
  s₁.entries.Perm s₂.entries → (AList.replace a b s₁).entries.Perm (AList.replace a b s₂).entries
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- There is some weak limit cone for `F`  -/
CategoryTheory.Limits.HasWeakLimit.exists_weakLimitCone : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} {C : Type u_3}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C} {F : CategoryTheory.Functor J C}
  [self : CategoryTheory.Limits.HasWeakLimit F], Nonempty (CategoryTheory.Limits.WeakLimitCone F)
-- Mathlib.Logic.Embedding.Set
/-- For disjoint `s t : Set α`, the natural injection from `↑s ⊕ ↑t` to `α`.  -/
Function.Embedding.sumSet : {α : Type u_1} → {s t : Set α} → Disjoint s t → ↑s ⊕ ↑t ↪ α
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isHexDigit_isAscii : ∀ {c : UInt8}, Std.Http.Internal.Char.isHexDigitByte c = true → Std.Http.Internal.Char.isAsciiByte c = true
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_ge_add : ∀ {α : Type u_5} {R : Type u_6} [inst : LinearOrder R] [inst_1 : Add R] {f : Filter α} [f.NeBot] [AddLeftMono R]
  [AddRightMono R] {u v : α → R},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
    Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f v → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f (u + v)
-- Init.MetaTypes
Lean.Meta.TransparencyMode.all.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.all = 1
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The linear isometry equivalence version of `TensorProduct.lid`.  -/
TensorProduct.lidIsometry : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → TensorProduct 𝕜 𝕜 E ≃ₗᵢ[𝕜] E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.alter t k f) k = f (Std.DTreeMap.Const.get? t k)
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_pos_iff_ne_top : ∀ (p : ENNReal) [Fact (1 ≤ p)], 0 < p.toReal ↔ p ≠ ⊤