BridgelandStability Comparator Manual

1. Overview🔗

Repository: https://github.com/mattrobball/BridgelandStability

Trusted base: open trusted_base.lean in the Lean 4 Web Editor

This manual presents the comparator view of the formalization. It was generated mechanically from the trusted formalization base walk rooted at the comparator target theorem in BridgelandStability.NumericalStabilityManifold. The formalization covers 57 declarations across 10 modules.

1.1. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first`🔗

Theorem | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- For any nonzero object, there exists an HN filtration with nonzero first factor.
Proved by repeatedly dropping zero first factors; terminates since `n` decreases
and some factor must be nonzero (by `exists_nonzero_factor`). -/
lemma HNFiltration.exists_nonzero_first (s : Slicing C) {E : C} (hE : ¬IsZero E) :
    ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃

Show proof

:= byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
  obtain ⟨F⟩ := s.hn_exists EC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
  suffices hmain : ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m →
      ∃ (H : HNFiltration C s.P E) (hn : 0 < H.n),
        ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ from
    hmain F.n F le_rflC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
  intro mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕ⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
  induction m with
  | zero =>zeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ 0 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    intro G hGnzeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
    exact absurd (G.zero_isZero (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ G.n = 0 liaAll goals completed! 🐙)) hE
  | succ m ih =>succC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m + 1 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    intro G hGnsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
    have hGn0 : 0 < G.n := G.n_pos C hEsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    by_cases hfirst : IsZero (G.triangle ⟨0, hGn0⟩).obj₃posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:¬IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
    ·posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ -- First factor is zero; drop it and recurse
      have hn1 : 1 < G.n := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
        by_contra hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:¬1 < G.n⊢ False; push Not at hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1⊢ False
        have : ∀ (i : Fin G.n), IsZero (G.triangle i).obj₃ := fun i ↦ byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ IsZero (G.triangle i).obj₃
          have : i = ⟨0, hGn0⟩ := Fin.ext (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ ↑i = ↑⟨0, hGn0⟩ liaAll goals completed! 🐙)C:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1i:Fin G.nthis:i = ⟨0, hGn0⟩⊢ IsZero (G.triangle i).obj₃
          subst thisC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1⊢ IsZero (G.triangle ⟨0, hGn0⟩).obj₃; exact hfirstC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃h:G.n ≤ 1this:∀ (i : Fin G.n), IsZero (G.triangle i).obj₃⊢ False
        exact absurd ((G.exists_nonzero_factor C hE).elim fun i hi ↦ absurd (this i) hi) idposC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃hn1:1 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
      have hdrop : (G.dropFirst C hn1 hfirst).n ≤ m := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨0, hn⟩).obj₃
        change G.n - 1 ≤ mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃hn1:1 < G.n⊢ G.n - 1 ≤ m; liaposC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:IsZero (G.triangle ⟨0, hGn0⟩).obj₃hn1:1 < G.nhdrop:(dropFirst C G hn1 hfirst).n ≤ m⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃
      exact ih (G.dropFirst C hn1 hfirst) hdropAll goals completed! 🐙
    ·negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhfirst:¬IsZero (G.triangle ⟨0, hGn0⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨0, hn⟩).obj₃ exact ⟨G, hGn0, hfirst⟩All goals completed! 🐙

1.2. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last`🔗

Theorem | BridgelandStability.Slicing.Defs | Source | Open Issue

/-- For any nonzero object, there exists an HN filtration with nonzero last factor.
Proved by repeatedly dropping zero last factors. -/
lemma HNFiltration.exists_nonzero_last (s : Slicing C) {E : C} (hE : ¬IsZero E) :
    ∃ (F : HNFiltration C s.P E) (hn : 0 < F.n),
      ¬IsZero (F.triangle ⟨F.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Ehn:0 < F.n⊢ F.n - 1 < F.n liaAll goals completed! 🐙⟩).obj₃

Show proof

:= byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
  obtain ⟨F⟩ := s.hn_exists EC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
  suffices hmain : ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m →
      ∃ (H : HNFiltration C s.P E) (hn : 0 < H.n),
        ¬IsZero (H.triangle ⟨H.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕG:HNFiltration C s.P EH:HNFiltration C s.P Ehn:0 < H.n⊢ H.n - 1 < H.n liaAll goals completed! 🐙⟩).obj₃ from
    hmain F.n F le_rflC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (m : ℕ) (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
  intro mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕ⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
  induction m with
  | zero =>zeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P E⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ 0 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    intro G hGnzeroC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
    exact absurd (G.zero_isZero (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P EG:HNFiltration C s.P EhGn:G.n ≤ 0⊢ G.n = 0 liaAll goals completed! 🐙)) hE
  | succ m ih =>succC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃⊢ ∀ (G : HNFiltration C s.P E), G.n ≤ m + 1 → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    intro G hGnsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
    have hGn0 : 0 < G.n := G.n_pos C hEsuccC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
    by_cases hlast : IsZero (G.triangle ⟨G.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.n⊢ G.n - 1 < G.n liaAll goals completed! 🐙⟩).obj₃
    ·posC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃ have hn1 : 1 < G.n := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
        by_contra hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:¬1 < G.n⊢ False; push Not at hC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1⊢ False
        have : ∀ (i : Fin G.n), IsZero (G.triangle i).obj₃ := fun i ↦ byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ IsZero (G.triangle i).obj₃
          have : i = ⟨G.n - 1, byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ G.n - 1 < G.n liaAll goals completed! 🐙⟩ := Fin.ext (byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.n⊢ ↑i = ↑⟨G.n - 1, ⋯⟩ liaAll goals completed! 🐙)C:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1i:Fin G.nthis:i = ⟨G.n - 1, ⋯⟩⊢ IsZero (G.triangle i).obj₃
          subst thisC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1⊢ IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃; exact hlastC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃h:G.n ≤ 1this:∀ (i : Fin G.n), IsZero (G.triangle i).obj₃⊢ False
        exact absurd ((G.exists_nonzero_factor C hE).elim fun i hi ↦ absurd (this i) hi) idposC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃hn1:1 < G.n⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
      have hdrop : (G.dropLast C hn1 hlast).n ≤ m := byC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero E⊢ ∃ F, ∃ (hn : 0 < F.n), ¬IsZero (F.triangle ⟨F.n - 1, ⋯⟩).obj₃
        change G.n - 1 ≤ mC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃hn1:1 < G.n⊢ G.n - 1 ≤ m; liaposC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃hn1:1 < G.nhdrop:(dropLast C G hn1 hlast).n ≤ m⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃
      exact ih (G.dropLast C hn1 hlast) hdropAll goals completed! 🐙
    ·negC:Type uinst✝⁵:Category.{v, u} Cinst✝⁴:HasZeroObject Cinst✝³:HasShift C ℤinst✝²:Preadditive Cinst✝¹:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝:Pretriangulated Cs:Slicing CE:ChE:¬IsZero EF:HNFiltration C s.P Em:ℕih:∀ (G : HNFiltration C s.P E), G.n ≤ m → ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃G:HNFiltration C s.P EhGn:G.n ≤ m + 1hGn0:0 < G.nhlast:¬IsZero (G.triangle ⟨G.n - 1, ⋯⟩).obj₃⊢ ∃ H, ∃ (hn : 0 < H.n), ¬IsZero (H.triangle ⟨H.n - 1, ⋯⟩).obj₃ exact ⟨G, hGn0, hlast⟩All goals completed! 🐙

1.3. `CategoryTheory.Triangulated.trianglePresentation_isAdditive`🔗

Theorem | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue

@[instance]
theorem trianglePresentation_isAdditive {A : Type*} [AddCommGroup A] (f : C → A)
    [IsTriangleAdditive f] :
    (trianglePresentation C).IsAdditive f

Show proof

where
  additive := fun ⟨T, hT⟩ => IsTriangleAdditive.additive T hT

1.4. `CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels`🔗

Theorem | BridgelandStability.IntervalCategory.QuasiAbelian | Source | Open Issue

@[instance]
theorem Slicing.intervalCat_hasKernels (s : Slicing C) :
    HasKernels (s.IntervalCat C a b)

Show proof

:=
  ⟨fun {X Y} f ↦ Slicing.intervalCat_hasKernel (C := C) (s := s)
    (a := a) (b := b) (X := X) (Y := Y) f⟩

1.5. `CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels`🔗

Theorem | BridgelandStability.IntervalCategory.QuasiAbelian | Source | Open Issue

@[instance]
theorem Slicing.intervalCat_hasCokernels (s : Slicing C) :
    HasCokernels (s.IntervalCat C a b)

Show proof

:=
  ⟨fun {X Y} f ↦ Slicing.intervalCat_hasCokernel (C := C) (s := s)
    (a := a) (b := b) (X := X) (Y := Y) f⟩

1.6. `CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive`🔗

Theorem | BridgelandStability.EulerForm.Basic | Source | Open Issue

theorem eulerFormObj_contravariant_triangleAdditive (E : C) :
    IsTriangleAdditive (fun F ↦ eulerFormObj k C E F)

Show proof

where
  additive := fun T hT ↦ byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
    simp only [eulerFormObj]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    let F : C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`letI : F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤ⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`letI : F.IsHomological := linearCoyonedaObjIsHomological (k := k) (C := C) Ek:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    let δ_lin : (n : ℤ) → ((E ⟶ T.obj₃⟦n⟧) →ₗ[k] (E ⟶ T.obj₁⟦(n + 1)⟧)) := fun n ↦
      Linear.rightComp k E (T.mor₃⟦n⟧' ≫
        (shiftFunctorAdd' C 1 n (n + 1) (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···n:ℤ⊢ 1 + n = n + 1 liaAll goals completed! 🐙)).inv.app T.obj₁)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    let r : ℤ → ℤ := fun n ↦ Module.finrank k (LinearMap.range (δ_lin n))k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    have hδ_eq : ∀ n : ℤ, ((F.homologySequenceδ T n (n + 1) rfl).hom) = δ_lin n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro nk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)n:ℤ⊢ ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin n
      ext xk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)n:ℤx:↑((F.shift n).obj T.obj₃)⊢ (ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯)) x = (δ_lin n) x
      exact
        (CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply
          (C := C) (T := T) (n₀ := n) (n₁ := n + 1) (h := rfl) (A := Opposite.op E) x)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin n⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    have h_ker_f_aux : ∀ m : ℤ,
        Module.finrank k (LinearMap.ker (((F.shift (m + 1)).map T.mor₁).hom)) = r m := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro mk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤ⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m
      let f_succ : (E ⟶ T.obj₁⟦m + 1⟧) →ₗ[k] (E ⟶ T.obj₂⟦m + 1⟧) :=
        ((F.shift (m + 1)).map T.mor₁).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m
      have h_exact₁ : LinearMap.range (δ_lin m) = LinearMap.ker f_succ := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        rw [← hδ_eq mk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)⊢ (ModuleCat.Hom.hom (F.homologySequenceδ T m (m + 1) ⋯)).range = f_succ.ker]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)⊢ (ModuleCat.Hom.hom (F.homologySequenceδ T m (m + 1) ⋯)).range = f_succ.ker
        exact ShortComplex.Exact.moduleCat_range_eq_ker
          (F.homologySequence_exact₁ T hT m (m + 1) rfl)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)h_exact₁:(δ_lin m).range = f_succ.ker⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m
      simp only [r]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nm:ℤf_succ:(E ⟶ (shiftFunctor C (m + 1)).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C (m + 1)).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)h_exact₁:(δ_lin m).range = f_succ.ker⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = ↑(Module.finrank k ↥(δ_lin m).range)
      exact_mod_cast
        congrArg (fun V : Submodule k (E ⟶ T.obj₁⟦m + 1⟧) => Module.finrank k V) h_exact₁.symmk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r m⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    have hrank : ∀ n : ℤ,
        (Module.finrank k (E ⟶ T.obj₂⟦n⟧) : ℤ) =
        Module.finrank k (E ⟶ T.obj₁⟦n⟧) + Module.finrank k (E ⟶ T.obj₃⟦n⟧) -
          r (n - 1) - r n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      intro nk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤ⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      let f_n : (E ⟶ T.obj₁⟦n⟧) →ₗ[k] (E ⟶ T.obj₂⟦n⟧) := ((F.shift n).map T.mor₁).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      let g_n : (E ⟶ T.obj₂⟦n⟧) →ₗ[k] (E ⟶ T.obj₃⟦n⟧) := ((F.shift n).map T.mor₂).homk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have hexact_B : LinearMap.range f_n = LinearMap.ker g_n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        exact
          (ShortComplex.Exact.moduleCat_range_eq_ker
            (F.homologySequence_exact₂ T hT n))k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.ker⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`haveI : Module.Finite k (E ⟶ T.obj₂⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₂⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_mid := finrank_mid_of_exact k f_n g_n hexact_Bk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`haveI : Module.Finite k (E ⟶ T.obj₁⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₁⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝²:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝¹:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`haveI : Module.Finite k (E ⟶ T.obj₃⟦n⟧) := IsFiniteType.finite_dim (k := k) E (T.obj₃⟦n⟧)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_ker_f : Module.finrank k (LinearMap.ker f_n) = r (n - 1) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        change Module.finrank k (LinearMap.ker (((F.shift n).map T.mor₁).hom)) = r (n - 1)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift n).map T.mor₁)).ker) = r (n - 1)
        have hn : n = (n - 1) + 1 := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃ liak:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)hn:n = n - 1 + 1⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift n).map T.mor₁)).ker) = r (n - 1)
        rw [hnk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)hn:n = n - 1 + 1⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (n - 1 + 1)).map T.mor₁)).ker) = r (n - 1 + 1 - 1)]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)hn:n = n - 1 + 1⊢ ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (n - 1 + 1)).map T.mor₁)).ker) = r (n - 1 + 1 - 1)
        simpa using h_ker_f_aux (n - 1)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_ker_δ : Module.finrank k (LinearMap.ker (δ_lin n)) =
          Module.finrank k (LinearMap.range g_n) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have h_exact₃ : LinearMap.range g_n = LinearMap.ker (δ_lin n) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
          rw [← hδ_eq nk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)⊢ g_n.range = (ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯)).ker]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)⊢ g_n.range = (ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯)).ker
          exact ShortComplex.Exact.moduleCat_range_eq_ker
            (F.homologySequence_exact₃ T hT n (n + 1) rfl)k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_exact₃:g_n.range = (δ_lin n).ker⊢ Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range
        simpa using
          congrArg (fun V : Submodule k (E ⟶ T.obj₃⟦n⟧) => Module.finrank k V) h_exact₃.symmk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_f : (Module.finrank k (LinearMap.range f_n) : ℤ) =
          Module.finrank k (E ⟶ T.obj₁⟦n⟧) - r (n - 1) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have := f_n.finrank_range_add_finrank_kerk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝⁴:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝³:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝²:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangethis:Module.finrank k ↥f_n.range + Module.finrank k ↥f_n.ker = Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)⊢ ↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)
        liak:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      have h_g : (Module.finrank k (LinearMap.range g_n) : ℤ) =
          Module.finrank k (E ⟶ T.obj₃⟦n⟧) - r n := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        have h1 := (δ_lin n).finrank_range_add_finrank_kerk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)⊢ ↑(Module.finrank k ↥g_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - r n
        have h2 := h_ker_δk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)h2:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range⊢ ↑(Module.finrank k ↥g_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - r n
        simp only [r] at h2 ⊢k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h1:Module.finrank k ↥(δ_lin n).range + Module.finrank k ↥(δ_lin n).ker =
  Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)h2:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.range⊢ ↑(Module.finrank k ↥g_n.range) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - ↑(Module.finrank k ↥(δ_lin n).range)
        liak:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝³:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝²:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mn:ℤf_n:(E ⟶ (shiftFunctor C n).obj T.obj₁) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₂ := ModuleCat.Hom.hom ((F.shift n).map T.mor₁)g_n:(E ⟶ (shiftFunctor C n).obj T.obj₂) →ₗ[k] E ⟶ (shiftFunctor C n).obj T.obj₃ := ModuleCat.Hom.hom ((F.shift n).map T.mor₂)hexact_B:f_n.range = g_n.kerthis✝¹:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₂)h_mid:↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k ↥f_n.range) + ↑(Module.finrank k ↥g_n.range)this✝:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₁)this:Module.Finite k (E ⟶ (shiftFunctor C n).obj T.obj₃)h_ker_f:↑(Module.finrank k ↥f_n.ker) = r (n - 1)h_ker_δ:Module.finrank k ↥(δ_lin n).ker = Module.finrank k ↥g_n.rangeh_f:↑(Module.finrank k ↥f_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) - r (n - 1)h_g:↑(Module.finrank k ↥g_n.range) = ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) - r n⊢ ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
      r (n - 1) -
    r n
      linarithk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r n⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    have hr : (Function.support r).Finite := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
      refine Set.Finite.subset
        ((IsFiniteType.finite_support (k := k) E T.obj₁).image fun m : ℤ ↦ m - 1) ?_k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r n⊢ Function.support r ⊆ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      intro n hnk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support r⊢ n ∈ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      have hnonzero : (r n : ℤ) ≠ 0 := hnk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0⊢ n ∈ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      have hnontrivial : Nontrivial (E ⟶ T.obj₁⟦n + 1⟧) := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
        by_contra htrivk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ False
        Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`haveI : Subsingleton (E ⟶ T.obj₁⟦n + 1⟧) := not_nontrivial_iff_subsingleton.mp htrivk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ False
        have hδ : δ_lin n = 0 := byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormObj k C E T.obj₂ = eulerFormObj k C E T.obj₁ + eulerFormObj k C E T.obj₃
          ext xk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)x:E ⟶ (shiftFunctor C n).obj T.obj₃⊢ (δ_lin n) x = 0 x
          exact Subsingleton.elim _ _k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)hδ:δ_lin n = 0⊢ False
        apply hnonzerok:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝¹:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis✝:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0htriv:¬Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)this:Subsingleton (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)hδ:δ_lin n = 0⊢ r n = 0
        simp [r, hδ]k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0hnontrivial:Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ n ∈ (fun m => m - 1) '' {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}
      exact ⟨n + 1, hnontrivial, byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nn:ℤhn:n ∈ Function.support rhnonzero:r n ≠ 0hnontrivial:Nontrivial (E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁)⊢ (fun m => m - 1) (n + 1) = n simpAll goals completed! 🐙⟩k:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) +
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃))
    exact eulerSum_of_rank_identity (k := k) (C := C) E
      (a := fun n ↦ T.obj₁⟦n⟧)
      (b := fun n ↦ T.obj₂⟦n⟧)
      (c := fun n ↦ T.obj₃⟦n⟧)
      (r := r)
      hrank
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₁)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₁All goals completed! 🐙)
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₂)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₂All goals completed! 🐙)
      (byk:Type winst✝⁸:Field kC:Type uinst✝⁷:Category.{v, u} Cinst✝⁶:HasZeroObject Cinst✝⁵:HasShift C ℤinst✝⁴:Preadditive Cinst✝³:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝²:Pretriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:CT:Triangle ChT:T ∈ distinguishedTrianglesF:C ⥤ ModuleCat k := (linearCoyoneda k C).obj (Opposite.op E)this✝:F.ShiftSequence ℤ := Functor.ShiftSequence.tautological F ℤthis:F.IsHomological := ···δ_lin:(n : ℤ) → (E ⟶ (shiftFunctor C n).obj T.obj₃) →ₗ[k] E ⟶ (shiftFunctor C (n + 1)).obj T.obj₁ := fun n => Linear.rightComp k E ((shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n (n + 1) ⋯).inv.app T.obj₁)r:ℤ → ℤ := fun n => ↑(Module.finrank k ↥(δ_lin n).range)hδ_eq:∀ (n : ℤ), ModuleCat.Hom.hom (F.homologySequenceδ T n (n + 1) ⋯) = δ_lin nh_ker_f_aux:∀ (m : ℤ), ↑(Module.finrank k ↥(ModuleCat.Hom.hom ((F.shift (m + 1)).map T.mor₁)).ker) = r mhrank:∀ (n : ℤ),
  ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₂)) =
    ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₁)) + ↑(Module.finrank k (E ⟶ (shiftFunctor C n).obj T.obj₃)) -
        r (n - 1) -
      r nhr:(Function.support r).Finite⊢ {n | Nontrivial (E ⟶ (shiftFunctor C n).obj T.obj₃)}.Finite simpa using IsFiniteType.finite_support (k := k) E T.obj₃All goals completed! 🐙)
      hr

1.7. `CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive`🔗

Theorem | BridgelandStability.EulerForm.Basic | Source | Open Issue

/-- The outer function `E ↦ eulerFormInner E` is triangle-additive, so the Euler
form descends to a bilinear form on `K₀`. -/
@[instance]
theorem eulerFormInner_isTriangleAdditive
    [(shiftFunctor C (1 : ℤ)).Linear k] :
    IsTriangleAdditive (eulerFormInner k C)

Show proof

where
  additive T hT := byk:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTriangles⊢ eulerFormInner k C T.obj₂ = eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃
    apply K₀.hom_extk:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTriangles⊢ ∀ (X : C), (eulerFormInner k C T.obj₂) (K₀.of C X) = (eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃) (K₀.of C X); intro Fk:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:C⊢ (eulerFormInner k C T.obj₂) (K₀.of C F) = (eulerFormInner k C T.obj₁ + eulerFormInner k C T.obj₃) (K₀.of C F)
    simp only [AddMonoidHom.add_apply, eulerFormInner, K₀.lift_of]k:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:C⊢ eulerFormObj k C T.obj₂ F = eulerFormObj k C T.obj₁ F + eulerFormObj k C T.obj₃ F
    Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`letI := eulerFormObj_covariant_triangleAdditive (k := k) (C := C) Fk:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:Linear k Cinst✝¹:IsFiniteType k Cinst✝:Functor.Linear k (shiftFunctor C 1)T:Triangle ChT:T ∈ distinguishedTrianglesF:Cthis:IsTriangleAdditive fun E => eulerFormObj k C E F := ···⊢ eulerFormObj k C T.obj₂ F = eulerFormObj k C T.obj₁ F + eulerFormObj k C T.obj₃ F
    exact IsTriangleAdditive.additive (f := fun E ↦ eulerFormObj k C E F) T hTAll goals completed! 🐙

1.8. `CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent`🔗

Theorem | BridgelandStability.NumericalStabilityManifold | Source | Open Issue

/-- **Bridgeland's Corollary 1.3** for numerical stability conditions. Each connected
component of `Stab_N(D)` is a complex manifold of dimension `rk(N(D))`.

This is a specialization of the generic class-map theorem to
`v = numericalQuotientMap k C`, which is surjective by definition. -/
@[informal "Corollary 1.3" "complex manifold conclusion only; local homeomorphism is in componentTopologicalLinearLocalModel" complete]
theorem NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent
    (k : Type w) [Field k]
    [Linear k C] [IsFiniteType k C]
    [(shiftFunctor C (1 : ℤ)).Linear k]
    [NumericallyFinite k C]
    (cc : StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)) :
    ∃ (E : Type u) (_ : NormedAddCommGroup E) (_ : NormedSpace ℂ E)
      (_ : FiniteDimensional ℂ E)
      (_ : ChartedSpace E (NumericalComponent (k := k) C cc)),
      IsManifold (𝓘(ℂ, E)) (⊤ : WithTop ℕ∞)
        (NumericalComponent (k := k) C cc)

Show proof

:= byC:Type uinst✝¹¹:Category.{v, u} Cinst✝¹⁰:HasZeroObject Cinst✝⁹:HasShift C ℤinst✝⁸:Preadditive Cinst✝⁷:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁶:Pretriangulated Cinst✝⁵:IsTriangulated Ck:Type winst✝⁴:Field kinst✝³:Linear k Cinst✝²:IsFiniteType k Cinst✝¹:Functor.Linear k (shiftFunctor C 1)inst✝:NumericallyFinite k Ccc:StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)⊢ ∃ E x x_1, ∃ (_ : FiniteDimensional ℂ E), ∃ x_3, IsManifold 𝓘(ℂ, E) ⊤ (NumericalComponent k C cc)
  Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`haveI : Fact (Function.Surjective (numericalQuotientMap k C)) :=
    ⟨QuotientAddGroup.mk'_surjective (eulerFormRad k C)⟩C:Type uinst✝¹¹:Category.{v, u} Cinst✝¹⁰:HasZeroObject Cinst✝⁹:HasShift C ℤinst✝⁸:Preadditive Cinst✝⁷:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁶:Pretriangulated Cinst✝⁵:IsTriangulated Ck:Type winst✝⁴:Field kinst✝³:Linear k Cinst✝²:IsFiniteType k Cinst✝¹:Functor.Linear k (shiftFunctor C 1)inst✝:NumericallyFinite k Ccc:StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)this:Fact (Function.Surjective ⇑(numericalQuotientMap k C))⊢ ∃ E x x_1, ∃ (_ : FiniteDimensional ℂ E), ∃ x_3, IsManifold 𝓘(ℂ, E) ⊤ (NumericalComponent k C cc)
  simpa [NumericalComponent] using
    StabilityCondition.WithClassMap.existsComplexManifoldOnConnectedComponent C ccAll goals completed! 🐙

1.9. Declaration census🔗

Every constant in the transitive closure of the target theorem's type. Auxiliary declarations are resolved to their user-facing parent.

132 raw constants: 57 user-facing, 0 auxiliary.

K0Presentation — user
CategoryTheory.IsStrict — user
CategoryTheory.IsStrictArtinianObject — user
CategoryTheory.IsStrictMono — user
CategoryTheory.IsStrictNoetherianObject — user
CategoryTheory.StrictSubobject — user
CategoryTheory.isStrictArtinianObject — user
CategoryTheory.isStrictNoetherianObject — user
K0Presentation.IsAdditive — user
K0Presentation.K0 — user
K0Presentation.lift — user
K0Presentation.mk — constructor → K0Presentation
K0Presentation.obj₁ — projection → K0Presentation
K0Presentation.obj₂ — projection → K0Presentation
K0Presentation.obj₃ — projection → K0Presentation
K0Presentation.subgroup — user
CategoryTheory.IsStrictMono.mk — constructor → CategoryTheory.IsStrictMono
CategoryTheory.Subobject.IsStrict — user
CategoryTheory.Triangulated.HNFiltration — user
CategoryTheory.Triangulated.IsFiniteType — user
CategoryTheory.Triangulated.IsTriangleAdditive — user
CategoryTheory.Triangulated.K₀ — user
CategoryTheory.Triangulated.NumericalComponent — user
CategoryTheory.Triangulated.NumericalK₀ — user
CategoryTheory.Triangulated.NumericallyFinite — user
CategoryTheory.Triangulated.PostnikovTower — user
CategoryTheory.Triangulated.Slicing — user
CategoryTheory.Triangulated.basisNhd — user
CategoryTheory.Triangulated.cl — user
CategoryTheory.Triangulated.eulerForm — user
CategoryTheory.Triangulated.eulerFormInner — user
CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive — user
CategoryTheory.Triangulated.eulerFormObj — user
CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive — user
CategoryTheory.Triangulated.eulerFormRad — user
CategoryTheory.Triangulated.numericalQuotientMap — user
CategoryTheory.Triangulated.slicingDist — user
CategoryTheory.Triangulated.stabSeminorm — user
CategoryTheory.Triangulated.trianglePresentation — user
CategoryTheory.Triangulated.trianglePresentation_isAdditive — user
K0Presentation.IsAdditive.additive — projection → K0Presentation.IsAdditive
K0Presentation.IsAdditive.mk — constructor → K0Presentation.IsAdditive
K0Presentation.instAddCommGroupK0._proof_1 — internal → K0Presentation.instAddCommGroupK0
K0Presentation.instAddCommGroupK0._proof_2 — internal → K0Presentation.instAddCommGroupK0
K0Presentation.lift._abel_5 — internal → K0Presentation.lift
K0Presentation.lift._proof_1 — internal → K0Presentation.lift
K0Presentation.lift._simp_3 — internal → K0Presentation.lift
K0Presentation.lift._simp_4 — internal → K0Presentation.lift
K0Presentation.lift.match_1 — user
CategoryTheory.Subobject.IsStrict._proof_1 — internal → CategoryTheory.Subobject.IsStrict
CategoryTheory.Subobject.IsStrict._proof_2 — internal → CategoryTheory.Subobject.IsStrict
CategoryTheory.Subobject.IsStrict._proof_3 — internal → CategoryTheory.Subobject.IsStrict
CategoryTheory.Subobject.IsStrict._proof_4 — internal → CategoryTheory.Subobject.IsStrict
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first — user
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last — user
CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.φ — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.IsFiniteType.mk — constructor → CategoryTheory.Triangulated.IsFiniteType
CategoryTheory.Triangulated.IsTriangleAdditive.mk — constructor → CategoryTheory.Triangulated.IsTriangleAdditive
CategoryTheory.Triangulated.K₀.instAddCommGroup — user
CategoryTheory.Triangulated.K₀.lift — user
CategoryTheory.Triangulated.K₀.of — user
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup — user
CategoryTheory.Triangulated.NumericallyFinite.mk — constructor → CategoryTheory.Triangulated.NumericallyFinite
CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.factor — user
CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap — user
CategoryTheory.Triangulated.Slicing.IntervalCat — user
CategoryTheory.Triangulated.Slicing.IsLocallyFinite — user
CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels — user
CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels — user
CategoryTheory.Triangulated.Slicing.intervalProp — user
CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.phiMinus — user
CategoryTheory.Triangulated.Slicing.phiPlus — user
CategoryTheory.Triangulated.StabilityCondition.WithClassMap — user
CategoryTheory.Triangulated.numericalQuotientMap._proof_1 — internal → CategoryTheory.Triangulated.numericalQuotientMap
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last._proof_1 — internal → CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_1 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_12 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_14 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_16 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_4 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_8 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_10 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_11 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_18 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_19 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_20 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_21 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_22 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_23 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_3 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_6 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_7 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_1 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_12 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_14 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_16 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_4 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_8 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_10 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_11 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_18 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_19 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_20 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_21 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_22 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_23 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_3 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_6 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_7 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.Z — projection → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge — user
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.mk — constructor → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.slicing — projection → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap
CategoryTheory.Triangulated.Slicing.IsLocallyFinite.mk — constructor → CategoryTheory.Triangulated.Slicing.IsLocallyFinite
CategoryTheory.Triangulated.Slicing.phiMinus._proof_1 — internal → CategoryTheory.Triangulated.Slicing.phiMinus
CategoryTheory.Triangulated.Slicing.phiMinus._proof_2 — internal → CategoryTheory.Triangulated.Slicing.phiMinus
CategoryTheory.Triangulated.Slicing.phiPlus._proof_1 — internal → CategoryTheory.Triangulated.Slicing.phiPlus
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component — user
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex — user
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.mk — constructor → CategoryTheory.Triangulated.StabilityCondition.WithClassMap
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.toWithClassMap — projection → CategoryTheory.Triangulated.StabilityCondition.WithClassMap
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace — user
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace._proof_1 — internal → CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace 13 raw constants: 4 user-facing, 0 auxiliary.
CategoryTheory.Triangulated.HNFiltration — user
CategoryTheory.Triangulated.PostnikovTower — user
CategoryTheory.Triangulated.Slicing — user
CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.factor — user
CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing 14 raw constants: 5 user-facing, 0 auxiliary.
CategoryTheory.Triangulated.HNFiltration — user
CategoryTheory.Triangulated.PostnikovTower — user
CategoryTheory.Triangulated.Slicing — user
CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.factor — user
CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last._proof_1 — internal → CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last 10 raw constants: 4 user-facing, 0 auxiliary.
K0Presentation — user
K0Presentation.IsAdditive — user
K0Presentation.mk — constructor → K0Presentation
K0Presentation.obj₁ — projection → K0Presentation
K0Presentation.obj₂ — projection → K0Presentation
K0Presentation.obj₃ — projection → K0Presentation
CategoryTheory.Triangulated.IsTriangleAdditive — user
CategoryTheory.Triangulated.trianglePresentation — user
K0Presentation.IsAdditive.mk — constructor → K0Presentation.IsAdditive
CategoryTheory.Triangulated.IsTriangleAdditive.mk — constructor → CategoryTheory.Triangulated.IsTriangleAdditive 16 raw constants: 6 user-facing, 0 auxiliary.
CategoryTheory.Triangulated.HNFiltration — user
CategoryTheory.Triangulated.PostnikovTower — user
CategoryTheory.Triangulated.Slicing — user
CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.φ — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.factor — user
CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.Slicing.IntervalCat — user
CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.intervalProp — user
CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing 16 raw constants: 6 user-facing, 0 auxiliary.
CategoryTheory.Triangulated.HNFiltration — user
CategoryTheory.Triangulated.PostnikovTower — user
CategoryTheory.Triangulated.Slicing — user
CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.HNFiltration.φ — projection → CategoryTheory.Triangulated.HNFiltration
CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.factor — user
CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower
CategoryTheory.Triangulated.Slicing.IntervalCat — user
CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing
CategoryTheory.Triangulated.Slicing.intervalProp — user
CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing 5 raw constants: 3 user-facing, 0 auxiliary.
CategoryTheory.Triangulated.IsFiniteType — user
CategoryTheory.Triangulated.IsTriangleAdditive — user
CategoryTheory.Triangulated.eulerFormObj — user
CategoryTheory.Triangulated.IsFiniteType.mk — constructor → CategoryTheory.Triangulated.IsFiniteType
CategoryTheory.Triangulated.IsTriangleAdditive.mk — constructor → CategoryTheory.Triangulated.IsTriangleAdditive 47 raw constants: 17 user-facing, 0 auxiliary.
K0Presentation — user
K0Presentation.IsAdditive — user
K0Presentation.K0 — user
K0Presentation.lift — user
K0Presentation.mk — constructor → K0Presentation
K0Presentation.obj₁ — projection → K0Presentation
K0Presentation.obj₂ — projection → K0Presentation
K0Presentation.obj₃ — projection → K0Presentation
K0Presentation.subgroup — user
CategoryTheory.Triangulated.IsFiniteType — user
CategoryTheory.Triangulated.IsTriangleAdditive — user
CategoryTheory.Triangulated.K₀ — user
CategoryTheory.Triangulated.eulerFormInner — user
CategoryTheory.Triangulated.eulerFormObj — user
CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive — user
CategoryTheory.Triangulated.trianglePresentation — user
CategoryTheory.Triangulated.trianglePresentation_isAdditive — user
K0Presentation.IsAdditive.additive — projection → K0Presentation.IsAdditive
K0Presentation.IsAdditive.mk — constructor → K0Presentation.IsAdditive
K0Presentation.instAddCommGroupK0._proof_1 — internal → K0Presentation.instAddCommGroupK0
K0Presentation.instAddCommGroupK0._proof_2 — internal → K0Presentation.instAddCommGroupK0
K0Presentation.lift._abel_5 — internal → K0Presentation.lift
K0Presentation.lift._proof_1 — internal → K0Presentation.lift
K0Presentation.lift._simp_3 — internal → K0Presentation.lift
K0Presentation.lift._simp_4 — internal → K0Presentation.lift
K0Presentation.lift.match_1 — user
CategoryTheory.Triangulated.IsFiniteType.mk — constructor → CategoryTheory.Triangulated.IsFiniteType
CategoryTheory.Triangulated.IsTriangleAdditive.mk — constructor → CategoryTheory.Triangulated.IsTriangleAdditive
CategoryTheory.Triangulated.K₀.instAddCommGroup — user
CategoryTheory.Triangulated.K₀.lift — user
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_1 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_12 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_14 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_16 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_4 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_8 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_10 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_11 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_18 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_19 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_20 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_21 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_22 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_23 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_3 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_6 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup
CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_7 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

1.10. Dependency graph🔗

Click a node to navigate to its declaration.

1. Overview🔗

1.1. CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first🔗

1.2. CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last🔗

1.3. CategoryTheory.Triangulated.trianglePresentation_isAdditive🔗

1.4. CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels🔗

1.5. CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels🔗

1.6. CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive🔗

1.7. CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive🔗

1.8. CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent🔗

1.9. Declaration census🔗

1.10. Dependency graph🔗

1.1. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first`🔗

1.2. `CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last`🔗

1.3. `CategoryTheory.Triangulated.trianglePresentation_isAdditive`🔗

1.4. `CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels`🔗

1.5. `CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels`🔗

1.6. `CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive`🔗

1.7. `CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive`🔗

1.8. `CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent`🔗