mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.ext_iff : ∀ {H : Type u_1} {inst : NormedAddCommGroup H} {inst_1 : InnerProductSpace ℂ H} {x y : StandardSubspace H},
  x = y ↔ x.toClosedSubmodule = y.toClosedSubmodule
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- Reinterpret a `NonUnitalStarSubsemiring` as a `NonUnitalSubsemiring`.  -/
NonUnitalStarSubsemiring.toNonUnitalSubsemiring : {R : Type v} →
  [inst : NonUnitalNonAssocSemiring R] → [inst_1 : Star R] → NonUnitalStarSubsemiring R → NonUnitalSubsemiring R
-- Mathlib.Lean.Elab.InfoTree
/-- Finds the first result of `f ctx info children` which is `some a`, descending the
tree from the top. Merges and updates contexts as it descends the tree.

`f` is **only** evaluated on nodes when some context is present. An initial context should be
provided via the `ctx?` argument if invoking `findSome?` during a larger traversal of the infotree.
A failure to provide `ctx? := some ctx` when `t` is not the outermost `InfoTree` is thus likely to
cause `findSome?` to always return `none`.
 -/
Lean.Elab.InfoTree.findSome? : {α : Type} →
  (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Option α) →
    Lean.Elab.InfoTree → optParam (Option Lean.Elab.ContextInfo) none → Option α
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
CategoryTheory.Bicategory.rightZigzag.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.Bicategory.rightZigzag η ε =
    CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerLeft g η)
      (CategoryTheory.Bicategory.whiskerRight ε g)
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr.mk.injEq : ∀ (thm thm_1 : Lean.Meta.Grind.EMatchTheorem), ({ thm := thm } = { thm := thm_1 }) = (thm = thm_1)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtDTreeMap.maxEntry? : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Option ((a : α) × β a)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.freeLocus_eq_univ : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Module.Flat R M], Module.freeLocus R M = Set.univ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β}, m.WF → (m.modify k f).contains k' = m.contains k'
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.nonDegenerate_ext₂ : ∀ {p q n : ℕ}
  {z₁ z₂ :
    ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n)},
  (↑z₁).2 = (↑z₂).2 → autoParam (p + q = n) SSet.prodStdSimplex.nonDegenerate_ext₂._auto_1 → z₁ = z₂
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- Group-like elements in a bialgebra are stable under inverses, when they exist.  -/
isGroupLikeElem_iff_of_mul_eq_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {a b : A},
  a * b = 1 → b * a = 1 → (IsGroupLikeElem R a ↔ IsGroupLikeElem R b)
-- Mathlib.Order.Filter.Basic
Filter.mem_iInf_of_directed : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α},
  Directed (fun x1 x2 => x1 ≥ x2) f → ∀ [Nonempty ι] (s : Set α), s ∈ iInf f ↔ ∃ i, s ∈ f i
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods_eq_periods_of_neg_one_mem : ∀ {R : Type u_1} [inst : Ring R] {𝒢 : Subgroup (GL (Fin 2) R)}, -1 ∈ 𝒢 → 𝒢.strictPeriods = 𝒢.periods
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
CFC.sqrt_le_sqrt : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a b : A),
  a ≤ b → CFC.sqrt a ≤ CFC.sqrt b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.baseChange_neg : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).neg (⇑f ∘ P) = ⇑f ∘ (W'.baseChange A).neg P
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_subset_skeletonLT`. -/
Topology.CWComplex.cellFrontier_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n),
  Topology.RelCWComplex.cellFrontier n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.var.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {a a_1 : α}, FirstOrder.Language.var a = FirstOrder.Language.var a_1 → a = a_1
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The adjunction image-preimage adjunction for an open immersion of schemes.  -/
AlgebraicGeometry.Scheme.Hom.opensFunctorAdjunction : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [H : AlgebraicGeometry.IsOpenImmersion f] →
      AlgebraicGeometry.Scheme.Hom.opensFunctor f ⊣ TopologicalSpace.Opens.map f.base
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot'_reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι},
  P.coroot' ((P.reflectionPerm i) j) = P.coroot' j ∘ₗ ↑(P.reflection i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {combined lw rw : ℕ}
  {lhs : aig.RefVec lw} {rhs : aig.RefVec rw} {h : combined = rw + lw} {lw_1 rw_1 : ℕ} {lhs_1 : aig.RefVec lw_1}
  {rhs_1 : aig.RefVec rw_1} {h_1 : combined = rw_1 + lw_1},
  { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } =
      { lw := lw_1, rw := rw_1, lhs := lhs_1, rhs := rhs_1, h := h_1 } →
    lw = lw_1 ∧ rw = rw_1 ∧ lhs ≍ lhs_1 ∧ rhs ≍ rhs_1
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_eq_zero_iff : ∀ {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] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L}, FractionalIdeal.dual A K I = 0 ↔ I = 0
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_pos_eq : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = MeasureTheory.upcrossingsBefore a b f N ω
-- Mathlib.Algebra.Star.Basic
Int.instStarRing : StarRing ℤ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G),
  CategoryTheory.Functor.LaxMonoidal.ε G =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_le_iff_le_add'`. -/
le_add_of_sub_left_le : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a - b ≤ c → a ≤ b + c
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instInhabitedSemanticTokensState : Inhabited Lean.Server.FileWorker.SemanticTokensState
-- Mathlib.Data.List.DropRight
List.rtakeWhile_concat_pos : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α),
  p x = true → List.rtakeWhile p (l ++ [x]) = List.rtakeWhile p l ++ [x]
-- Mathlib.Topology.Spectral.Hom
SpectralMap.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : SpectralMap α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.Limits.Types.isConnected_iff_isColimit_pUnitCocone : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsConnected C ↔ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.pUnitCocone C))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instFunLike : (X : SemiNormedGrp₁) → (Y : SemiNormedGrp₁) → FunLike { f // f.NormNoninc } X.carrier Y.carrier
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- An atlas of charts, which are only `PartialEquiv`s  -/
ChartedSpaceCore.atlas : {H : Type u_5} → [inst : TopologicalSpace H] → {M : Type u_6} → ChartedSpaceCore H M → Set (PartialEquiv M H)
-- Mathlib.Order.Filter.Basic
Filter.neBot_of_le : ∀ {α : Type u} {f g : Filter α} [hf : f.NeBot], f ≤ g → g.NeBot
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.continuous_unop : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous MulOpposite.unop
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_zero' : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {n : ℕ}
  {ω : Ω}, MeasureTheory.upperCrossingTime a b f ⊥ n ω = ⊥
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ),
  MvPolynomial.coeff m 1 = if 0 = m then 1 else 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.push.sizeOf_spec : ∀ (k : Turing.PartrecToTM2.K') (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ')
  (q : Turing.PartrecToTM2.Λ'), sizeOf (Turing.PartrecToTM2.Λ'.push k s q) = 1 + sizeOf k + sizeOf q
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtype_apply : ∀ {α : Type u_9} {β : α → Type u_10} {γ : (a : α) → β a → Type u_11} (p : (a : α) × β a → Prop)
  [uniq : Unique { ab // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) (a_1 : { s // p ⟨s.fst, s.snd.fst⟩ }),
  (Equiv.sigmaSigmaSubtype p h) a_1 = cast ⋯ (↑a_1).snd.snd
-- Mathlib.ModelTheory.Syntax
/-- Places existential quantifiers on all in-scope bound variables of a bounded formula.  -/
FirstOrder.Language.BoundedFormula.exs : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.Formula α
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a closed subspace is a `1`-Lipschitz map.  -/
Submodule.lipschitzWith_orthogonalProjectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], LipschitzWith 1 ⇑K.orthogonalProjectionOnto
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_eq_one_iff_eq_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, b ≠ 0 → (a * b = 1 ↔ a = b⁻¹)
-- Init.Data.List.Perm
List.Perm.sizeOf_eq_sizeOf : ∀ {α : Type u_1} [inst : SizeOf α] {l₁ l₂ : List α}, l₁.Perm l₂ → sizeOf l₁ = sizeOf l₂
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V} (a b : PowerSeries R),
  (HahnSeries.SummableFamily.powerSeriesFamily x (a * b)).hsum =
    ((HahnSeries.SummableFamily.powerSeriesFamily x a).mul (HahnSeries.SummableFamily.powerSeriesFamily x b)).hsum
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instIsStableUnderCompositionMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J K : CategoryTheory.Precoverage C)
  [J.IsStableUnderComposition] [K.IsStableUnderComposition], (J ⊓ K).IsStableUnderComposition
-- Mathlib.Order.Filter.Basic
Filter.inter_eventuallyEq_left : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
-- Init.Data.Array.Lemmas
Array.back_eq_of_push_eq : ∀ {α : Type u_1} {a b : α} {xs ys : Array α}, xs.push a = ys.push b → a = b
-- Mathlib.Algebra.Torsor.Basic
Prod.snd_vadd : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (v : G × G') (p : P × P'), (v +ᵥ p).2 = v.2 +ᵥ p.2
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk'_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.toAddMon ⟶ B.toAddMon), (CategoryTheory.AddGrp.homMk' f).hom = f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_6.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_7 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t
-- Lean.Elab.BindersUtil
/-- Recall that
```
def typeSpec := leading_parser " : " >> termParser
def optType : Parser := optional typeSpec
```
 -/
Lean.Elab.Term.expandOptType : Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₄Toδ₃' : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, 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₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ),
  (c r).prev pq' = pq →
    ∀ (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq')
      (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ),
      n₁ = data.deg pq' →
        ∀ [X.HasSpectralSequence data],
          ¬(c r).Rel pq pq' →
            ∀
              (hn₁ :
                autoParam (n₀ + 1 = n₁)
                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₄Toδ₃'._auto_1)
              (hn₂ :
                autoParam (n₁ + 1 = n₂)
                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₄Toδ₃'._auto_3),
              CategoryTheory.IsIso (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonFunctor.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (D : Type u₂)
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D],
  CategoryTheory.Functor.mapMonFunctor C D =
    { obj := fun F => F.mapMon,
      map := fun {X Y} α => { app := fun A => CategoryTheory.Mon.Hom.mk' (α.hom.app A.X) ⋯ ⋯, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.List.Sigma
List.kerase_append_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  a ∉ l₁.keys → List.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
-- Init.Data.List.Sublist
List.singleton_sublist : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Sublist l ↔ a ∈ l
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquiv_apply : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a b : α) (g : ↑(⇑f ⁻¹' {f a})),
  ↑((f.fiberEquiv a b) g) = b * (a⁻¹ * ↑g)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.norm_integral_le_of_norm_le_const : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b C : ℝ} {f : ℝ → E},
  (∀ x ∈ Set.uIoc a b, ‖f x‖ ≤ C) → ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
-- Init.Data.String.PosRaw
String.Pos.Raw.unoffsetBy_le_self : ∀ {p q : String.Pos.Raw}, p.unoffsetBy q ≤ p
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- There is no hope of computing this, but we add the instance anyway to avoid fumbling with
`open scoped Classical`.  -/
Module.Free.instDecidableEqChooseBasisIndex : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [inst_3 : Module.Free R M] → DecidableEq (Module.Free.ChooseBasisIndex R M)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinsert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → Multiset.ndinsert a s = a ::ₘ s
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iInter₂ : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E]
  {f : (i : ι) → κ i → Set E}, (∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)) → Balanced 𝕜 (⋂ i, ⋂ j, f i j)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.inv_mul' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (u : G₀ˣ), (↑u)⁻¹ * ↑u = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β} {fallback : α}, cmp ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a * x) ⁻¹' Set.Iio b = Set.Iio (b / a)
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.norm_extendRCLike : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F), ‖fr.extendRCLike‖ = ‖fr‖
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).obj₃ = (t.truncGE a).obj ((t.truncLT b).obj j)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.mk.injEq : ∀ (cache : Lean.Meta.Simp.Cache) (congrCache : Lean.Meta.Simp.CongrCache) (dsimpCache : Lean.ExprStructMap Lean.Expr)
  (usedTheorems : Lean.Meta.Simp.UsedSimps) (numSteps : ℕ) (diag : Lean.Meta.Simp.Diagnostics)
  (cache_1 : Lean.Meta.Simp.Cache) (congrCache_1 : Lean.Meta.Simp.CongrCache)
  (dsimpCache_1 : Lean.ExprStructMap Lean.Expr) (usedTheorems_1 : Lean.Meta.Simp.UsedSimps) (numSteps_1 : ℕ)
  (diag_1 : Lean.Meta.Simp.Diagnostics),
  ({ cache := cache, congrCache := congrCache, dsimpCache := dsimpCache, usedTheorems := usedTheorems,
        numSteps := numSteps, diag := diag } =
      { cache := cache_1, congrCache := congrCache_1, dsimpCache := dsimpCache_1, usedTheorems := usedTheorems_1,
        numSteps := numSteps_1, diag := diag_1 }) =
    (cache = cache_1 ∧
      congrCache = congrCache_1 ∧
        dsimpCache = dsimpCache_1 ∧ usedTheorems = usedTheorems_1 ∧ numSteps = numSteps_1 ∧ diag = diag_1)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_fmod_self_right : ∀ (a b c : ℤ), (a * b - c).fmod b = (-c).fmod b
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_basis_open : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : Set α),
  (nhdsSetWithin s t).HasBasis (fun u => IsOpen u ∧ s ⊆ u) fun u => u ∩ t
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment.eq_1 : ∀ (b : Bool) (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b a =
    if b = true then a.addPosAssignment else a.addNegAssignment
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_zero_fun : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  ProbabilityTheory.cgf 0 μ t = Real.log (μ.real Set.univ)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sub_const_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable Y μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance X (fun ω => Y ω - c) μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.Data.Holor
Holor.holor_index_cons_decomp : ∀ {d : ℕ} {ds : List ℕ} (p : HolorIndex (d :: ds) → Prop) (t : HolorIndex (d :: ds)),
  (∀ (i : ℕ) (is : List ℕ) (h : ↑t = i :: is), p ⟨i :: is, ⋯⟩) → p t