∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x y : E × F},
  x ∈ f.graph → y ∈ f.graph → x.1 = y.1 → x.2 = y.2