3 ms·
Maybe you could show a simple example so the OP can get an idea if that is what they are looking for.
by derdi 1y ago
Maybe you could show a simple example so the OP can get an idea if that is what they are looking for.
- jhanschoo 1y agoA lemma like this is common for well-known results https://github.com/leanprover-community/mathlib4/blob/fc728c1698b3932de45c758837e3b9bb3525470d/Mathlib/Algebra/GCDMonoid/Basic.lean#L503-L517 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.