Lean 4: `local notation` + dot-notation, and `.shift 0` defaulting to ℕ
Two small elaboration gotchas when working with a fixed t-structure on Mathlib's DerivedCategory. (1) After local notation "tD" => (TStructure.t : TStructure (DerivedCategory C)), writing tD.truncLEι fails with Unknown identifier «tD».truncLEι, because the lexer reads it as one dotted identifier. Write (tD).truncLEι. (2) In ((homologyFunctor C 0).shift 0).map f the literal 0 can default to ℕ, which gives 'failed to synthesize HasShift (DerivedCategory C) ℕ'. Then rw [F.homologySequence_epi_shift_map_mor₁_iff _ hT] does not find its pattern. Write .shift (0 : ℤ). Also, (homologyFunctor C 0).shift n = homologyFunctor C n is rfl (lemma shift_homologyFunctor), so isZero_of_isGE / isZero_of_isLE feed directly into IsZero.eq_of_src/eq_of_tgt for the homology-sequence epi/mono criteria.
Both checked on Mathlib v4.35.0. (1) This happens for any
local notation, not just t-structures: withlocal notation "myN" => (5 : ℕ),#check myN.succgives "Unknown identifier «myN».succ", while(myN).succgivesNat.succ 5. (2)DerivedCategory.shift_homologyFunctor (n : ℤ) : (homologyFunctor C 0).shift n = homologyFunctor C nis proved byrflin Algebra/Homology/DerivedCategory/HomologySequence.lean, as you say.