-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem neg_graph (f : E →ₗ.[R] F) :
    (-f).graph =
    f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (-(LinearMap.id : F →ₗ[R] F)))

Proof state:
case h.mk.mp
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_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rcases h with ⟨y, hy, h⟩

Result:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Proof state:
case h.mk.mpr
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_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
rw [Submodule.mem_map] at h

Result:
case h.mk.mpr
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_fst : E
x_snd : F
h : ∃ y ∈ f.graph, (LinearMap.id.prodMap (-LinearMap.id)) y = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph

Proof state:
case h.mk.mpr.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_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h : (LinearMap.id.prodMap (-LinearMap.id)) x' = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
cases x'

Result:
case h.mk.mpr.intro.intro.mk
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_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : (fst✝, snd✝) ∈ f.graph
h : (LinearMap.id.prodMap (-LinearMap.id)) (fst✝, snd✝) = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph

Proof state:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rw [Submodule.mem_map]

Result:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ ∃ y ∈ f.graph, (LinearMap.id.prodMap (-LinearMap.id)) y = (x_fst, x_snd)

Proof state:
case h
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_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2

Tactic:
rw [← h.1, ← h.2]

Result:
case h
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_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ↑y = (fst✝, -snd✝).1 ∧ ↑(-f) y = (fst✝, -snd✝).2

Proof state:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ ∃ y ∈ f.graph, (LinearMap.id.prodMap (-LinearMap.id)) y = (x_fst, x_snd)

Tactic:
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
  LinearMap.neg_apply, Prod.mk.inj_iff, Prod.exists, exists_exists_and_eq_and]

Result:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ ∃ a a_1, ↑a_1 = a ∧ a = x_fst ∧ -↑f a_1 = x_snd

Proof state:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ ∃ a a_1, ↑a_1 = a ∧ a = x_fst ∧ -↑f a_1 = x_snd

Tactic:
use x_fst, y, hy

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
⊢ (-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
ext ⟨x_fst, x_snd⟩

Result:
case h.mk
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_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ (-f).graph ↔ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Proof state:
case h.mk.mp
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_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rw [mem_graph_iff] at h

Result:
case h.mk.mp
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_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Proof state:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rw [LinearPMap.neg_apply] at h

Result:
case h.mk.mp.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_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : -↑f y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Proof state:
case h.mk.mpr
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_fst : E
x_snd : F
h : ∃ y ∈ f.graph, (LinearMap.id.prodMap (-LinearMap.id)) y = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
rcases h with ⟨x', hx', h⟩

Result:
case h.mk.mpr.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_fst : E
x_snd : F
x' : E × F
hx' : x' ∈ f.graph
h : (LinearMap.id.prodMap (-LinearMap.id)) x' = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (-f).graph