R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (fun b =>
        if a0 : a = 0 then b
        else
          let_fun x := (_ : EuclideanDomain.r (b % a) a);
          gcd (b % a) a)
      b =
    gcd (b % a) a
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a
rw [gcd]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (fun b =>
        if a0 : a = 0 then b
        else
          let_fun x := (_ : EuclideanDomain.r (b % a) a);
          gcd (b % a) a)
      b =
    gcd (b % a) a
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]