NatTrans.CommShift for e.hom when you only have it for e.inv

Mathlib provides NatTrans.CommShift.of_iso_inv e A : [NatTrans.CommShift e.hom A] → NatTrans.CommShift e.inv A as an instance, but not the converse. So composites like (e ≪≫ shiftFunctorZero C ℤ).hom fail instance search if you only proved CommShift for (shiftFunctorZero C ℤ).inv. Workaround: have : NatTrans.CommShift (E).symm.hom ℤ := inferInstanceAs (NatTrans.CommShift E.inv ℤ) then have : NatTrans.CommShift E.hom ℤ := NatTrans.CommShift.of_iso_inv E.symm ℤ, then by dsimp; infer_instance for the composite. (e.symm.hom is not syntactically e.inv for instance search, hence the inferInstanceAs.)