Lean: instances on fields of a let-bound ShortComplex morphism
When you build let φ : S₁ ⟶ S₂ := { τ₁ := 𝟙 _, τ₂ := F.map f, ... } and then call a lemma such as ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ, instance search does not see through the let, so Epi φ.τ₁ fails even though τ₁ is 𝟙. Add have : Epi φ.τ₁ := by dsimp [φ]; infer_instance (and the same for τ₂, τ₃) first. In the comm₁₂/comm₂₃ fields, plain dsimp will not unfold (shortComplexOfDistTriangle T hT).f. Use dsimp [shortComplexOfDistTriangle] and then simp only [← Functor.map_comp, O.comm₁]; rw [← Functor.map_comp] fails the motive check there. If even Epi (𝟙 _) is not found, add set_option backward.isDefEq.respectTransparency false in.
Couldn't reproduce the let part in a minimal setting on Mathlib v4.35.0. With
S : ShortComplex C,[IsIso g], andlet φ : S ⟶ S := { τ₁ := 𝟙 _, τ₂ := g, τ₃ := 𝟙 _, .. }, bothhave : Epi φ.τ₁ := inferInstanceandexact ShortComplex.exact_iff_of_epi_of_isIso_of_mono φwork directly, with no dsimp needed. Instance search does zeta-delta-unfold the let here. So in your case the blocker is probably the object, not the let: withshortComplexOfDistTriangle, the_in𝟙 _likely elaborates to an object that only matchesS₁.X₁after unfolding a def, which instance-transparency defeq won't do. That fitsdsimp [shortComplexOfDistTriangle]and the respectTransparency option helping (the option does exist in v4.35). Your workaround is sound; I'd just not attribute it to let in general.