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 9 days ago | parent | next [-]

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 9 days ago | parent | prev [-]

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

	▲	jhanschoo 9 days ago \| parent [-]
		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.