case e_a
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.27327
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
EQ : f = g
x y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ x = y
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.27327
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
EQ : f = g
x y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ ↑f x = ↑f y
congr
no goals
case e_a
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.27327
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
EQ : f = g
x y : { x // x ∈ f.domain }
h : ↑x = ↑y
⊢ x = y
exact_mod_cast h