tiny simplification of gcd_rec proof

leanprover-community · Jul 1, 2021 · fd1c568 · fd1c568
1 parent 5ef8f93
commit fd1c568
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Mathlib/Data/Nat/Gcd.lean b/Mathlib/Data/Nat/Gcd.lean
@@ -144,8 +144,7 @@ Exists.elim H (λ l H1 => by rw [Nat.mul_assoc] at H1
 theorem gcd_rec (m n : ℕ) : gcd m n = gcd (n % m) m :=
   match m with
   | 0 => by have := (mod_zero n).symm
-            simp
-            exact this
+            rwa [gcd_zero_right]
   | pm + 1 => by simp [gcd_succ]
 
 theorem gcd.induction