mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Stated for readability of `δ₀_apply`.  -/
groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{max u u_1, u, u} k G)},
  X.ShortExact →
    ∀ {y : ↑X.X₂} {x : G → ↑X.X₁},
      ⇑(Rep.Hom.hom X.f) ∘ x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ X.X₂)) y →
        x ∈ groupCohomology.cocycles₁ X.X₁
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_rii : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.toList
-- Mathlib.Order.Hom.Lattice
SupHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β), f.comp (SupHom.id α) = f
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
EuclideanGeometry.preimage_inversion_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c y : P} {R : ℝ},
  R ≠ 0 →
    y ≠ c →
      EuclideanGeometry.inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c y) =
        Metric.sphere (EuclideanGeometry.inversion c R y) (R ^ 2 / dist y c) \ {c}
-- Mathlib.Topology.Order.Basic
exists_Icc_mem_subset_of_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  s ∈ nhds a → ∃ b c, a ∈ Set.Icc b c ∧ Set.Icc b c ∈ nhds a ∧ Set.Icc b c ⊆ s
-- Mathlib.Data.Set.BoolIndicator
Set.mem_iff_boolIndicator : ∀ {α : Type u_1} (s : Set α) (x : α), x ∈ s ↔ s.boolIndicator x = true
-- Init.Data.Order.Ord
Std.OrientedCmp.gt_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.lt → cmp b a = Ordering.gt
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instCoeHeadKeysArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → CoeHead (RBTree.RBMap.Keys α β cmp) (Array α)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.mk.injEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (inner inner_1 : Std.ExtHashMap α Unit),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Data.Nat.Pairing
Nat.pairEquiv_apply : ⇑Nat.pairEquiv = Function.uncurry Nat.pair
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod_mrange : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)},
  MonoidHom.mrange (MonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ i, MonoidHom.mrange (ϕ i)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_empty : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.real ∅ = 0
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_self_mul_conjTranspose : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : PartialOrder R] [inst_4 : StarRing R] [StarOrderedRing R] (A : Matrix m n R),
  (A * A.conjTranspose).rank = A.rank
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_inf : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Opens α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toRingEquiv_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), (Matrix.reindexAlgEquiv R A e).toRingEquiv = Matrix.reindexRingEquiv A e
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
/-- The canonical isomorphism between
`w.structuredArrowDownwards Y₁ ⋙ w'.structuredArrowDownwards (R₁.obj Y₁)` and
`(w ≫ᵥ w').structuredArrowDownwards Y₁.`  -/
CategoryTheory.TwoSquare.structuredArrowDownwardsComp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [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} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        {H₁ : CategoryTheory.Functor C₁ D₁} →
                          {L₁ : CategoryTheory.Functor C₁ C₂} →
                            {R₁ : CategoryTheory.Functor D₁ D₂} →
                              {H₂ : CategoryTheory.Functor C₂ D₂} →
                                (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) →
                                  {L₂ : CategoryTheory.Functor C₂ C₃} →
                                    {R₂ : CategoryTheory.Functor D₂ D₃} →
                                      {H₃ : CategoryTheory.Functor C₃ D₃} →
                                        (w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃) →
                                          (Y₁ : D₁) →
                                            (w.structuredArrowDownwards Y₁).comp
                                                (w'.structuredArrowDownwards (R₁.obj Y₁)) ≅
                                              (w.vComp w').structuredArrowDownwards Y₁
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instSetLike : SetLike ZFSet.{u} ZFSet.{u}
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable;
a version for the region together with the graph of the lower function.  -/
nullMeasurableSet_region_between_co : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        (m₁.diff! m₂).getKey! k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then default else m₁.getKey! k
-- Lean.Util.PPExt
Lean.FormatWithInfos.fmt : Lean.FormatWithInfos → Std.Format
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_support_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support.dropLast ++ [v] = p.support
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_compl_add_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ.restrict sᶜ + μ.restrict s = μ
-- Lean.Structure
/-- A descriptor for a structure, for constructing a `StructureInfo` via `Lean.registerStructure`.
 -/
Lean.StructureDescr : Type
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by `c`'.  -/
Con.sSup_eq_conGen : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), sSup S = conGen fun x y => ∃ c ∈ S, c x y
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove the maximum element from the tree, or do nothing if it is already empty.

```
eraseMax {1, 2, 3} = {1, 2}
eraseMax ∅ = ∅
```  -/
Ordnode.eraseMax : {α : Type u_1} → Ordnode α → Ordnode α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.alter! k f t).maxKey! = k ↔
          (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.nonempty : ∀ (self : NonemptyFinLinOrd), Nonempty ↑self.toLinOrd
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.pre : Mathlib.Tactic.Order.OrderType
-- Init.Data.Vector.Erase
Vector.eraseIdx_append_of_length_le : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {k : ℕ} (hk : n ≤ k) (xs' : Vector α m) (h : k < n + m),
  (xs ++ xs').eraseIdx k h = Vector.cast ⋯ (xs ++ xs'.eraseIdx (k - n) ⋯)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear maps.  -/
ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} {s : Set E} {l : F →L[ℝ] G},
  ContDiffWithinAt ℝ 2 f s x →
    UniqueDiffOn ℝ s →
      InnerProductSpace.laplacianWithin (⇑l ∘ f) s =ᶠ[nhdsWithin x s] ⇑l ∘ InnerProductSpace.laplacianWithin f s
-- Mathlib.Order.KrullDimension
/-- The coheight of the first element in a series is larger or equal to the length of the series.
 -/
Order.length_le_coheight_head : ∀ {α : Type u_1} [inst : Preorder α] {p : LTSeries α}, ↑p.length ≤ Order.coheight (RelSeries.head p)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_himp_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] {s : Finset ι},
  s.Nonempty → ∀ (f : ι → α) (a : α), (s.sup fun b => a ⇨ f b) = a ⇨ s.sup f
-- Mathlib.Order.Category.Lat
/-- The underlying lattices.  -/
Lat.carrier : Lat → Type u_1
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.eventually_filterAt_integrableOn : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) {E : Type u_2} [inst_1 : NormedAddCommGroup E] (x : α) {f : α → E},
  MeasureTheory.LocallyIntegrable f μ → ∀ᶠ (a : Set α) in v.filterAt x, MeasureTheory.IntegrableOn f a μ
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Roo.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Roo.HasRcoIntersection α}
  [self : Std.Roo.LawfulRcoIntersection α] {a : α} {r : Std.Roo α} {s : Std.Rco α},
  a ∈ Std.Roo.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Lean.Elab.DefView
/-- Number of parameters before `:`, it also includes auto-implicit parameters automatically added by Lean.  -/
Lean.Elab.DefViewElabHeaderData.numParams : Lean.Elab.DefViewElabHeaderData → ℕ
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend.f_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) {i' : ι'} {i : ι} (hi : e.f i = i'),
  ComplexShape.Embedding.liftExtend.f φ i' =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).inv
      (CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e hi).inv)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keyAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ} {fallback : α}, t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f).getKey? k = if (f t[k]?).isSome = true then some k else none
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeSupportEqEquiv_apply_coe : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (x : { f // f.support = s }) (i : ↥s),
  ↑((DFinsupp.subtypeSupportEqEquiv s) x i) = ↑x ↑i
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2 : Lean.ConstructorVal →
  Bool →
    Array Lean.Expr →
      Lean.Expr →
        (Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Expr)) →
          ℕ → Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_toArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toArray.size = m.size
-- Init.Data.List.Erase
List.erase_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∉ l → l.erase a = l
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `Relation.SymmGen.of_antisymmRel_of_symmGen`. -/
AntisymmRel.trans_symmGen : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    Relation.SymmGen (fun x1 x2 => x1 ≤ x2) b c → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg.eq_1 : ∀ (i : Int32), i.toNatClampNeg = i.toInt.toNat
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Loopless.loops_eq_empty : ∀ {α : Type u_1} {M : Matroid α} [self : M.Loopless], M.loops = ∅
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- `[(exp, coef)]` is `Sorted` when `coef` is `Sorted`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.cons_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl} {f : ℝ → ℝ},
  coef.Sorted →
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil)
        f).Sorted
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.ext : ∀ (x y : PSet.{u_1}), x.Equiv y ↔ x ⊆ y ∧ y ⊆ x
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorSemiring.ceil a` computes the least natural `n` such that `a ≤ (n : α)`.  -/
FloorSemiring.ceil : {α : Type u_4} → {inst : Semiring α} → {inst_1 : PartialOrder α} → [self : FloorSemiring α] → α → ℕ
-- Mathlib.Order.Antichain
IsGreatest.antichain_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α],
  IsGreatest s a → (IsAntichain (fun x1 x2 => x1 ≤ x2) s ↔ s = {a})
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_mul_zero : ∀ {h : ℝ} {f g : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ContinuousAt (Function.Periodic.cuspFunction h g) 0 →
      Function.Periodic.cuspFunction h (f * g) 0 =
        Function.Periodic.cuspFunction h f 0 * Function.Periodic.cuspFunction h g 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.stronglyMeasurable_one : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : One β],
  MeasureTheory.StronglyMeasurable 1
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_symm : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {f g : α → β}, f =ᵐ[μ] g → g =ᵐ[μ] f
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandler.mk.injEq : ∀ (ref : Lean.Syntax) (key : Lean.Name) (kind : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind) (body : Lean.Term)
  (projFn? struct? : Option Lean.Name) (ref_1 : Lean.Syntax) (key_1 : Lean.Name)
  (kind_1 : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind) (body_1 : Lean.Term)
  (projFn?_1 struct?_1 : Option Lean.Name),
  ({ ref := ref, key := key, kind := kind, body := body, projFn? := projFn?, struct? := struct? } =
      { ref := ref_1, key := key_1, kind := kind_1, body := body_1, projFn? := projFn?_1, struct? := struct?_1 }) =
    (ref = ref_1 ∧ key = key_1 ∧ kind = kind_1 ∧ body = body_1 ∧ projFn? = projFn?_1 ∧ struct? = struct?_1)
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι)
  (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv._auto_3),
  (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv =
    CategoryTheory.CategoryStruct.comp (X.EIsoH (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv
-- Lean.Server.References
/-- Identifier of this reference.  -/
Lean.Server.Reference.ident : Lean.Server.Reference → Lean.Lsp.RefIdent
-- Mathlib.Data.TypeVec
TypeVec.toSubtype.eq_2 : ∀ (n : ℕ) (x_5 : TypeVec.{u} n.succ) (x_6 : x_5.Arrow (TypeVec.repeat n.succ Prop))
  (x_7 : { x // TypeVec.ofRepeat (x_6 Fin2.fz x) }), TypeVec.toSubtype x_6 Fin2.fz x_7 = x_7
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.eq_4 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1))
  (n : ℕ) (h_1 : (x : ℕ → C) → (x_2 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_2 0 0)
  (h_2 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1)
  (h_3 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → motive x f 0 l.succ)
  (h_4 : (x : ℕ → C) → (x_2 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_2 n.succ 0)
  (h_5 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ),
  (match x, x_1, n.succ, 0 with
    | x, x_2, 0, 0 => h_1 x x_2
    | x, f, 0, 1 => h_2 x f
    | x, f, 0, l.succ => h_3 x f l
    | x, x_2, n.succ, 0 => h_4 x x_2 n
    | x, f, k.succ, l.succ => h_5 x f k l) =
    h_4 x x_1 n
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.toFinsupp_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (f : SkewMonoidAlgebra k G) (g : G), f.coeff g = f.coeff g
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- If we repeat a row of a matrix, we get a matrix of determinant zero.  -/
Matrix.det_updateRow_eq_zero : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {M : Matrix n n R}
  {i j : n}, i ≠ j → (M.updateRow j (M i)).det = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves finite colimits, then `F : C ⥤ Dᵒᵖ` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F.leftOp],
  CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The `n`-th derivative of a function along a set, defined inductively by saying that the `n+1`-th
derivative of `f` is the derivative of the `n`-th derivative of `f` along this set, together with
an uncurrying step to see it as a multilinear map in `n+1` variables..
 -/
iteratedFDerivWithin : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (n : ℕ) → (E → F) → Set E → E → E [×n]→L[𝕜] F
-- Mathlib.Data.Set.Image
Set.isCompl_range_inl_range_inr : ∀ {α : Type u_1} {β : Type u_2}, IsCompl (Set.range Sum.inl) (Set.range Sum.inr)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.factorThruImage f
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
/-- After postcomposition with the fully faithful functor `G`,
`lift F G Φ hΦ` becomes isomorphic to `F`.  -/
CategoryTheory.SingleFunctors.liftPostcompIso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{u_5, u_1} C] →
        [inst_1 : CategoryTheory.Category.{u_6, u_2} D] →
          [inst_2 : CategoryTheory.Category.{u_7, u_3} E] →
            {A : Type u_4} →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    (F : CategoryTheory.SingleFunctors C E A) →
                      (G : CategoryTheory.Functor D E) →
                        [inst_6 : G.CommShift A] →
                          [inst_7 : G.Full] →
                            [inst_8 : G.Faithful] →
                              (Φ : A → CategoryTheory.Functor C D) →
                                (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a) → (F.lift G Φ hΦ).postcomp G ≅ F
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_inv_naturality : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i).op (K.opcyclesOpIso i).inv =
    CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).inv
      (HomologicalComplex.opcyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.fst_iConvexComb : ∀ {I : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {X : Type u_3} {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (w : Convexity.StdSimplex R I) (f : I → X × Y),
  (Convexity.iConvexComb w f).1 = Convexity.iConvexComb w fun i => (f i).1
-- Mathlib.LinearAlgebra.Charpoly.Basic
/-- The characteristic polynomial of `f : M →ₗ[R] M`.  -/
LinearMap.charpoly : {R : Type u} →
  {M : Type v} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [Module.Free R M] → [Module.Finite R M] → (M →ₗ[R] M) → Polynomial R
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.upperSet_le_upper : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : TopologicalSpace α} [Topology.IsUpperSet α] [Topology.IsUpper α], t₁ ≤ t₂
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of the reverse direction of `Finset.sup_le_iff`. -/
Finset.sup_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
  (∀ b ∈ s, f b ≤ a) → s.sup f ≤ a