-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem image_iff {f : E →ₗ.[R] F} {x : E} {y : F} (hx : x ∈ f.domain) :
    y = f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph

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 : E
y : F
hx : x ∈ f.domain
h : y = ↑f ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (x, y).1 ∧ ↑f ⟨x, hx⟩ = (x, y).2

Tactic:
simp [h]

Result:
no goals

Proof state:
case 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 : E
y : F
hx : x ∈ f.domain
h : ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2
⊢ y = ↑f ⟨x, hx⟩

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

Result:
case mpr.intro.mk.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 : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : ↑⟨x', hx'⟩ = (x, y).1
h2 : ↑f ⟨x', hx'⟩ = (x, y).2
⊢ y = ↑f ⟨x, hx⟩

Proof state:
case mpr.intro.mk.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 : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : ↑⟨x', hx'⟩ = (x, y).1
h2 : ↑f ⟨x', hx'⟩ = (x, y).2
⊢ y = ↑f ⟨x, hx⟩

Tactic:
simp only [Submodule.coe_mk] at h1 h2

Result:
case mpr.intro.mk.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 : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : x' = x
h2 : ↑f ⟨x', hx'⟩ = y
⊢ y = ↑f ⟨x, hx⟩

Proof state:
case mpr.intro.mk.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 : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : x' = x
h2 : ↑f ⟨x', hx'⟩ = y
⊢ y = ↑f ⟨x, hx⟩

Tactic:
simp only [← h2, h1]

Result:
no goals

Proof state:
case 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 : E
y : F
hx : x ∈ f.domain
h : y = ↑f ⟨x, hx⟩
⊢ ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2

Tactic:
use ⟨x, hx⟩

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 : E
y : F
hx : x ∈ f.domain
h : y = ↑f ⟨x, hx⟩
⊢ ↑⟨x, hx⟩ = (x, y).1 ∧ ↑f ⟨x, hx⟩ = (x, y).2

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 : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph

Tactic:
rw [mem_graph_iff]

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 : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f ⟨x, hx⟩ ↔ ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2

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 : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f ⟨x, hx⟩ ↔ ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2

Tactic:
constructor <;> intro h

Result:
case 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 : E
y : F
hx : x ∈ f.domain
h : y = ↑f ⟨x, hx⟩
⊢ ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2

case 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 : E
y : F
hx : x ∈ f.domain
h : ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2
⊢ y = ↑f ⟨x, hx⟩