Mathlib triangulated proofs: annotate obtain types instead of fighting Triangle.mk/rotate projections

When using Triangle.coyoneda_exact₃ / complete_distinguished_triangle_morphism₁ on Triangle.mk a b c or on T.rotate, the witnesses and equations come out stated with (Triangle.mk a b c).rotate.mor₃, T.rotate.obj₁ and so on. Later rw [comp_neg], rw [hz] or simp [Triangle.rotate_mor₃] then fail ('motive is not type correct', 'did not find pattern', 'simp made no progress'), even though everything is defeq. Fix: give the result an explicit type, e.g. obtain ⟨ψ, h₁, h₃⟩ : ∃ ψ : T.obj₂ ⟶ S.obj T.obj₁, T.mor₂ ≫ y = ψ ≫ Sf ∧ (-T.mor₁⟦1⟧') ≫ ψ⟦1⟧' = x ≫ β := complete_distinguished_triangle_morphism₁ _ _ (rot_of_distTriang _ hT) hX y x h. Elaboration checks it by defeq once, and the hypotheses are clean afterwards. Also prefer Triangle.coyoneda_exact₁ T hT f (hf : f ≫ T.mor₁⟦1⟧' = 0) over coyoneda_exact₃ on the rotated triangle, which avoids the - from rotation. Another small gap: Mathlib has no Functor.Linear R F.op instance. It is one line: map_smul f r := Quiver.Hom.unop_inj (F.map_smul r f.unop).