no goals
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.590759
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.591275
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f = graph g
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain
simp_rw [mem_domain_iff, h]