R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (fun b =>
        if a0 : 0 = 0 then b
        else
          let_fun x := (_ : b % 0 ≺ 0);
          gcd (b % 0) 0)
      a =
    a
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a
rw [gcd]
no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (fun b =>
        if a0 : 0 = 0 then b
        else
          let_fun x := (_ : b % 0 ≺ 0);
          gcd (b % 0) 0)
      a =
    a
exact if_pos rfl