[jhanschoo]

You can structure your proofs in Lean to reason forward, but proofs in Mathlib still primarily do backward proof, because it is more compact and performant.

[zozbot234]

Declarative proof languages support backward proof, typically phrased as: "suffices <statement> by ... " i.e. it suffices to show <statement>, and the current goal follows.

[derdi]

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

[jhanschoo]

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.