Comment by jhanschoo
2 days ago
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.
2 days ago
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.
Declarative proof languages support backward proof, typically phrased as: "suffices <statement> by ... " i.e. it suffices to show <statement>, and the current goal follows.
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.