-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph_snd_inj (f : E →ₗ.[R] F) {x y : E} {x' y' : F} (hx : (x, x') ∈ f.graph)
    (hy : (y, y') ∈ f.graph) (hxy : x = y) : x' = y'

Proof state:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
x'' : ↥f.domain
hx1 : ↑x'' = x
hx2 : ↑f x'' = x'
y'' : ↥f.domain
hxy : x'' = y''
hy1 : ↑y'' = y
hy2 : ↑f y'' = y'
⊢ x' = y'

Tactic:
rw [← hx2, ← hy2, hxy]

Result:
no goals

Proof state:
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hx : ∃ y, ↑y = (x, x').1 ∧ ↑f y = (x, x').2
hy : ∃ y_1, ↑y_1 = (y, y').1 ∧ ↑f y_1 = (y, y').2
hxy : x = y
⊢ x' = y'

Tactic:
rcases hx with ⟨x'', hx1, hx2⟩

Result:
case intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hy : ∃ y_1, ↑y_1 = (y, y').1 ∧ ↑f y_1 = (y, y').2
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = (x, x').1
hx2 : ↑f x'' = (x, x').2
⊢ x' = y'

Proof state:
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hx : (x, x') ∈ f.graph
hy : (y, y') ∈ f.graph
hxy : x = y
⊢ x' = y'

Tactic:
rw [mem_graph_iff] at hx hy

Result:
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hx : ∃ y, ↑y = (x, x').1 ∧ ↑f y = (x, x').2
hy : ∃ y_1, ↑y_1 = (y, y').1 ∧ ↑f y_1 = (y, y').2
hxy : x = y
⊢ x' = y'

Proof state:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = (x, x').1
hx2 : ↑f x'' = (x, x').2
y'' : ↥f.domain
hy1 : ↑y'' = (y, y').1
hy2 : ↑f y'' = (y, y').2
⊢ x' = y'

Tactic:
simp only at hx1 hx2 hy1 hy2

Result:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = x
hx2 : ↑f x'' = x'
y'' : ↥f.domain
hy1 : ↑y'' = y
hy2 : ↑f y'' = y'
⊢ x' = y'

Proof state:
case intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hy : ∃ y_1, ↑y_1 = (y, y').1 ∧ ↑f y_1 = (y, y').2
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = (x, x').1
hx2 : ↑f x'' = (x, x').2
⊢ x' = y'

Tactic:
rcases hy with ⟨y'', hy1, hy2⟩

Result:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = (x, x').1
hx2 : ↑f x'' = (x, x').2
y'' : ↥f.domain
hy1 : ↑y'' = (y, y').1
hy2 : ↑f y'' = (y, y').2
⊢ x' = y'

Proof state:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
hxy : x = y
x'' : ↥f.domain
hx1 : ↑x'' = x
hx2 : ↑f x'' = x'
y'' : ↥f.domain
hy1 : ↑y'' = y
hy2 : ↑f y'' = y'
⊢ x' = y'

Tactic:
rw [← hx1, ← hy1, SetLike.coe_eq_coe] at hxy

Result:
case intro.intro.intro.intro
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
f : E →ₗ.[R] F
x y : E
x' y' : F
x'' : ↥f.domain
hx1 : ↑x'' = x
hx2 : ↑f x'' = x'
y'' : ↥f.domain
hxy : x'' = y''
hy1 : ↑y'' = y
hy2 : ↑f y'' = y'
⊢ x' = y'