Maybe you could show a simple example so the OP can get an idea if that is what they are looking for.

A lemma like this is common for well-known results https://github.com/leanprover-community/mathlib4/blob/fc728c...

The one immediately before (`gcd_mul_dvd_mul_gcd`) is also well-known but uses a style closer to forward proof.

The very well-known ones `gcd_assoc` at the start oof this file are even more extreme and directly supply the proof term without tactics.