Commit 2022-08-11 16:02 c5ef8bc0
View on Github →add [elabAsElim] attribute to Nat.gcd.induction (#364)
Adds [elabAsElim] to Nat.gcd.induction, to bring it in line with mathlib3's version: https://github.com/leanprover-community/lean/blob/22b09be35ef66aece11e6e8f5d114f42b064259b/library/init/data/nat/gcd.lean#L42-L43
This is possible now that https://github.com/leanprover/lean4/commit/012cb13f51604cbb3bad96c8234f30acb746065c has landed.
This allows us to simplify some proofs.