-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_inverse_graph_snd_eq_zero (x : F × E)
    (hv : x ∈ (graph f).map (LinearEquiv.prodComm R E F))
    (hv' : x.fst = 0) : x.snd = 0

Proof state:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = b
hv' : b = 0
⊢ a = 0

Tactic:
rw [hv'] at h1

Result:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
⊢ a = 0

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
hf : LinearMap.ker f.toFun = ⊥
x : F × E
hv : x ∈ Submodule.map (LinearEquiv.prodComm R E F) f.graph
hv' : x.1 = 0
⊢ x.2 = 0

Tactic:
simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
  LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk] at hv

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
hf : LinearMap.ker f.toFun = ⊥
x : F × E
hv' : x.1 = 0
hv : ∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ (b, a) = x
⊢ x.2 = 0

Proof state:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
⊢ a = 0

Tactic:
rw [LinearMap.ker_eq_bot'] at hf

Result:
case intro.intro.intro.intro.refl
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
hf : ∀ (m : ↥f.domain), f.toFun m = 0 → m = 0
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
⊢ a = 0

Proof state:
case intro.intro.intro.intro.refl
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
hf : ∀ (m : ↥f.domain), f.toFun m = 0 → m = 0
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
⊢ a = 0

Tactic:
specialize hf ⟨a, ha⟩ h1

Result:
case intro.intro.intro.intro.refl
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
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
hf : ⟨a, ha⟩ = 0
⊢ a = 0

Proof state:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = b
hv' : (b, a).1 = 0
⊢ (b, a).2 = 0

Tactic:
simp only at hv' ⊢

Result:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = b
hv' : b = 0
⊢ a = 0

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
hf : LinearMap.ker f.toFun = ⊥
x : F × E
hv' : x.1 = 0
hv : ∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ (b, a) = x
⊢ x.2 = 0

Tactic:
rcases hv with ⟨a, b, ⟨ha, h1⟩, ⟨h2, h3⟩⟩

Result:
case intro.intro.intro.intro.refl
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
hf : LinearMap.ker f.toFun = ⊥
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = b
hv' : (b, a).1 = 0
⊢ (b, a).2 = 0

Proof state:
case intro.intro.intro.intro.refl
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
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
hf : a = 0
⊢ a = 0

Tactic:
exact hf

Result:
no goals

Proof state:
case intro.intro.intro.intro.refl
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
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
hf : ⟨a, ha⟩ = 0
⊢ a = 0

Tactic:
simp only [Submodule.mk_eq_zero] at hf

Result:
case intro.intro.intro.intro.refl
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
a : E
b : F
ha : a ∈ f.domain
h1 : ↑f ⟨a, ⋯⟩ = 0
hv' : b = 0
hf : a = 0
⊢ a = 0