case a.mk
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : ↑f sqrtd = ↑g sqrtd
x_re x_im : ℤ
⊢ ↑f { re := x_re, im := x_im } = ↑g { re := x_re, im := x_im }
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : ↑f sqrtd = ↑g sqrtd
⊢ f = g
ext ⟨x_re, x_im⟩
no goals
case a.mk
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : ↑f sqrtd = ↑g sqrtd
x_re x_im : ℤ
⊢ ↑f { re := x_re, im := x_im } = ↑g { re := x_re, im := x_im }
simp [decompose, h]