case H.mk
R : Type ?u.82639
S : Type ?u.82642
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
x y : ℝ
⊢ ↑f { re := x, im := y } = ↑g { re := x, im := y }
R : Type ?u.82639
S : Type ?u.82642
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
⊢ f = g
ext ⟨x, y⟩
no goals
case H.mk
R : Type ?u.82639
S : Type ?u.82642
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : ↑f I = ↑g I
x y : ℝ
⊢ ↑f { re := x, im := y } = ↑g { re := x, im := y }
simp only [mk_eq_add_mul_I, AlgHom.map_add, AlgHom.map_coe_real_complex, AlgHom.map_mul, h]