mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.post : Lean.Meta.Sym.DSimp.Methods → Lean.Meta.Sym.DSimp.DSimproc
-- Init.PropLemmas
forall_not_of_not_exists : ∀ {α : Sort u_1} {p : α → Prop}, (¬∃ x, p x) → ∀ (x : α), ¬p x
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_neg : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → IsRelPrime (-x) (-y)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.homeoOfIso_apply : ∀ {X Y : CompactlyGenerated} (f : X ≅ Y) (a : ↑X.toTop),
  (CompactlyGenerated.homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_monic : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → (minpolyDiv R x).Monic
-- Init.Data.String.Basic
String.Pos.le_ofSlice : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos}, p₀ ≤ String.Pos.ofSlice pos
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.pow.match_1.splitter : (motive : Dyadic → Sort u_1) →
  (x : Dyadic) → (Unit → motive Dyadic.zero) → ((n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn)) → motive x
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.stalkFunctionFieldAlgebra : (X : AlgebraicGeometry.Scheme) →
  [inst : IrreducibleSpace ↥X] → (x : ↥X) → Algebra ↑(X.presheaf.stalk x) ↑X.functionField
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.coeff_sumAlgEquiv_symm_apply : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : MvPolynomial S₁ (MvPolynomial S₂ R)),
  ((MvPolynomial.sumAlgEquiv R S₁ S₂).symm a).coeff =
    Finsupp.mapDomain (⇑Finsupp.sumFinsuppAddEquivProdFinsupp.symm) ((AddMonoidAlgebra.curryAlgEquiv R).symm a).coeff
-- Mathlib.Order.Filter.NAry
Filter.map₂_right : ∀ {α : Type u_1} {β : Type u_3} {f : Filter α} {g : Filter β} [f.NeBot], Filter.map₂ (fun x y => y) f g = g
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.eval_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] {X Y : CategoryTheory.Functor C A} (α : X ⟶ Y)
  (f : CategoryTheory.Limits.FormalCoproduct C),
  ((CategoryTheory.Limits.FormalCoproduct.eval C A).map α).app f =
    CategoryTheory.Limits.Sigma.map fun i => α.app (f.obj i)
-- Mathlib.Order.Filter.Cocardinal
Filter.frequently_cocardinal_mem : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α},
  (∃ᶠ (x : α) in Filter.cocardinal α hreg, x ∈ s) ↔ c ≤ Cardinal.mk ↑s
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 0).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op
      ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op
-- Init.Core
/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never holds.  -/
Std.Irrefl : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.snd_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (p : Submodule R E) (p' : Submodule R F) (x : ↥(p.prod p')),
  ↑(LinearPMap.snd p p') x = (↑x).2
-- Lean.Data.Lsp.Basic
Lean.Lsp.Command.mk : String → String → Option (Array Lean.Json) → Lean.Lsp.Command
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRat.sizeOf_spec : ∀ {β : Type u} {α : Type v} [inst : SizeOf β] [inst_1 : SizeOf α] (id : ℕ) (c : β) (pivot : Std.Sat.Literal α)
  (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
  sizeOf (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) =
    1 + sizeOf id + sizeOf c + sizeOf pivot + sizeOf rupHints + sizeOf ratHints
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Eta-expanded form of `Continuous.const_smul` -/
Continuous.fun_const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α}, Continuous g → ∀ (c : M), Continuous fun i => c • g i
-- Lean.Data.KVMap
Lean.KVMap.set : {α : Type} → [Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → α → Lean.KVMap
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_mul_left : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {a b c d : M},
  Associated (a * b) (c * d) → Associated a c → a ≠ 0 → Associated b d
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E']
  {v v_1 : Module.Basis ι 𝕜 E} (e_v : v = v_1) (hv : Orthonormal 𝕜 ⇑v) {v' v'_1 : Module.Basis ι' 𝕜 E'}
  (e_v' : v' = v'_1) (hv' : Orthonormal 𝕜 ⇑v') (e e_1 : ι ≃ ι'), e = e_1 → hv.equiv hv' e = ⋯.equiv ⋯ e_1
-- Mathlib.GroupTheory.OrderOfElement
/-- Inverses of elements of finite additive order
have finite additive order.  -/
isOfFinAddOrder_neg_iff : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, IsOfFinAddOrder (-x) ↔ IsOfFinAddOrder x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q),
  (CochainComplex.HomComplex.Cochain.fromSingleMk f h).v p q h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom f
-- Mathlib.Data.List.Prime
/-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L`  -/
Prime.dvd_prod_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M} {L : List M}, Prime p → (p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_sub : ∀ {R : Type u_1} [inst : CommRing R] (p q : Polynomial R), ↑(p - q) = ↑p - ↑q
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.coe_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e.toPartialEquiv = ↑e
-- Mathlib.Data.Vector.Basic
List.Vector.ofFn.eq_1 : ∀ {α : Type u_1} (x_2 : Fin 0 → α), List.Vector.ofFn x_2 = List.Vector.nil
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.sum.map_inv : ∀ {α : Type u} [inst : AddGroup α] {x : FreeGroup α}, x⁻¹.sum = -x.sum
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Functor.map_conjAut : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X),
  F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_ofSupport : ∀ {V : Type u} {G : SimpleGraph V} {l : List V} (hne : l ≠ []) (hchain : List.IsChain G.Adj l),
  (SimpleGraph.Walk.ofSupport l hne hchain).support = l
-- Mathlib.Order.Basic
le_iff_eq_or_lt' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a ↔ a = b ∨ b < a
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- A ring homomorphism `R →+* S` is standard smooth if `S` is standard smooth as `R`-algebra.  -/
RingHom.IsStandardSmooth : {R : Type u} → {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compRight_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₂ ⟶ S₃), (h.compRight ψ).h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ.τ₁
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_eq_max_neg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a : α}, |a| = max a (-a)
-- Init.Data.String.Decode
String.utf8EncodeChar_eq_singleton : ∀ {c : Char}, c.utf8Size = 1 → String.utf8EncodeChar c = [c.val.toUInt8]
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.usedTheorems : Lean.Meta.Simp.Stats → Lean.Meta.Simp.UsedSimps
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `a / b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalDiv : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given `sq : F.PushoutObjObj f₁ f₂`, flipping the pushout square gives
`sq.flip : F.flip.PushoutObjObj f₂ f₁`.  -/
CategoryTheory.Functor.PushoutObjObj.flip : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} → {X₂ Y₂ : C₂} → {f₂ : X₂ ⟶ Y₂} → F.PushoutObjObj f₁ f₂ → F.flip.PushoutObjObj f₂ f₁
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.coeToGL_det : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup n R), Matrix.GeneralLinearGroup.det (Matrix.SpecialLinearGroup.toGL g) = 1
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsRootSystem.mk : ∀ {ι : 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},
  Submodule.span R (Set.range ⇑P.root) = ⊤ → Submodule.span R (Set.range ⇑P.coroot) = ⊤ → P.IsRootSystem
-- Mathlib.Order.BoundedOrder.Basic
Prod.instOrderTop.eq_1 : ∀ (α : Type u) (β : Type v) [inst : LE α] [inst_1 : LE β] [inst_2 : OrderTop α] [inst_3 : OrderTop β],
  Prod.instOrderTop α β = { toTop := inferInstance, le_top := ⋯ }
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The functor taking a monoid to its subgroup of units.  -/
MonCat.units : CategoryTheory.Functor MonCat GrpCat
-- Mathlib.Algebra.Lie.CartanExists
_private.Mathlib.Algebra.Lie.CartanExists.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly.congr_simp : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x x_1 : L),
  x = x_1 →
    ∀ (y y_1 : L),
      y = y_1 →
        LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y = LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x_1 y_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.StrongHomClass.realize_formula : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {α : Type u'}
  {F : Type u_4} [inst_2 : EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.Formula α) {v : α → M},
  φ.Realize (⇑g ∘ v) ↔ φ.Realize v
-- Mathlib.RingTheory.LocalRing.Module
/-- If `M` is a finitely presented module over a local ring `(R, 𝔪)` such that `m ⊗ M → M` is
injective, then `M` is free.
 -/
Module.free_of_maximalIdeal_rTensor_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.FinitePresentation R M],
  Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R))) → Module.Free R M
-- Init.Data.Array.Basic
Array.findIdx?_eq_map_findFinIdx?_val : ∀ {α : Type u} {xs : Array α} {p : α → Bool}, Array.findIdx? p xs = Option.map (fun x => ↑x) (Array.findFinIdx? p xs)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- A graph has edge-disjoint triangles if each edge belongs to at most one triangle.  -/
SimpleGraph.EdgeDisjointTriangles : {α : Type u_1} → SimpleGraph α → Prop
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_zero : ∀ {α : Type u_1} {𝕜 : Type u_3} (E : Type u_4) {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  (q : ENNReal) {r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)), f • 0 = 0
-- Std.Time.Zoned.Database.Windows
Std.Time.Database.WindowsDb.mk.sizeOf_spec : sizeOf { } = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : C} [inst_3 : CategoryTheory.AddMonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) M)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
          CategoryTheory.AddMonObj.add))
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom)
      CategoryTheory.AddMonObj.add
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Define `circleAverage f c R` as the average value of `f` on the circle with center `c` and radius
`R`. This is a real notion, which should not be confused with the complex path integral notion
defined in `circleIntegral` (integrating with respect to `dz`).
 -/
Real.circleAverage : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℂ → E) → ℂ → ℝ → E
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_of_comp_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : CategoryTheory.ShortComplex.QuasiIso φ]
  [hφφ' : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')],
  CategoryTheory.ShortComplex.QuasiIso φ'
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousWithinAt.rpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℝ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → f x ≠ 0 ∨ 0 < g x → ContinuousWithinAt (fun t => f t ^ g t) s x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_associator : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} {A₃ : Type u₁₀} {B₃ : Type u₁₁}
  {C₃ : Type u₁₂} [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A₃] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B₃]
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C₃] {F₃ : CategoryTheory.Functor A₃ B₃}
  {G₃ : CategoryTheory.Functor C₃ B₃} (X : Type u₁₃) [inst_12 : CategoryTheory.Category.{v₁₃, u₁₃} X]
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (φ : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂)
  (τ : CategoryTheory.Limits.CatCospanTransform F₂ G₂ F₃ G₃),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map (ψ.associator φ τ).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X (ψ.comp φ) τ).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ φ).hom
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj τ))
        (CategoryTheory.CategoryStruct.comp
          (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).associator
              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj φ)
              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj τ)).hom
          (CategoryTheory.CategoryStruct.comp
            (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft
              (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X φ τ).inv)
            (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ (φ.comp τ)).inv)))
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_iso_hom : ∀ {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' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (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₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).iso.hom =
    CategoryTheory.CategoryStruct.id
      (X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_comp_assoc : ∀ {X Y : TopCat} (f : X ⟶ Y) {Z : TopCat} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y TopCat.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f TopCat.I) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp TopCat.ι₁ h)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instCoeFunForall : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → CoeFun (M →ₚₗ[R] N) fun x => M → N
-- Mathlib.Algebra.GroupWithZero.Action.Defs
SMulWithZero.toSMulZeroClass : {M₀ : Type u_2} →
  {A : Type u_7} → {inst : Zero M₀} → {inst_1 : Zero A} → [self : SMulWithZero M₀ A] → SMulZeroClass M₀ A
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.BifibrantObject.localizerMorphism C).IsLocalizedEquivalence
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).val = s.val ∪ t.val
-- Lean.Environment
_private.Lean.Environment.0.Lean.readIRPartsOfMod.unsafe_impl_5 : Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match 0, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_1 recur
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Mon D)) (X : C),
  CategoryTheory.MonObj.mul.app X = CategoryTheory.MonObj.mul
-- Mathlib.Order.MinMax
min_choice : ∀ {α : Type u} [inst : LinearOrder α] (a b : α), min a b = a ∨ min a b = b
-- Std.Data.ExtTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtTreeMap.toList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → List (α × β)
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_ediv_zero : ∀ {a b r : ℤ}, Mathlib.Meta.NormNum.IsInt a r → Mathlib.Meta.NormNum.IsNat b 0 → Mathlib.Meta.NormNum.IsNat (a / b) 0
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_sub : ∀ {a b : ℤ} {hab₁ : Int64.minValue.toInt ≤ a - b} {hab₂ : a - b ≤ Int64.maxValue.toInt},
  Int64.ofIntLE (a - b) hab₁ hab₂ = Int64.ofInt a - Int64.ofInt b
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some '' Set.Ioo b a = Set.Ioo ↑b ↑a
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.leftUnitor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)