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