-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_range_iff {f : E →ₗ.[R] F} {y : F} : y ∈ Set.range f ↔ ∃ x : E, (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
y : F
x : E
hx : x ∈ f.domain
h : ↑f ⟨x, hx⟩ = y
⊢ (x, y) ∈ f.graph

Tactic:
rw [← h]

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

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
y : F
h : ∃ x, (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

Tactic:
obtain ⟨x, h⟩ := h

Result:
case mpr.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
y : F
x : E
h : (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

Proof state:
case mpr.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
y : F
x : E
h : (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

Tactic:
rw [mem_graph_iff] at h

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

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

Tactic:
simp only at h

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
y : F
x✝ : E
x : ↥f.domain
h : ↑x = x✝ ∧ ↑f x = y
⊢ ↑f x = y

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
y : F
x✝ : E
x : ↥f.domain
h : ↑x = x✝ ∧ ↑f x = y
⊢ ↑f x = y

Tactic:
rw [h.2]

Result:
no goals

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

Tactic:
use x

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

Proof state:
case 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
y : F
x✝ : E
x : ↥f.domain
h : ↑x = (x✝, y).1 ∧ ↑f x = (x✝, y).2
⊢ y ∈ Set.range ↑f

Tactic:
rw [Set.mem_range]

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

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

Tactic:
use x

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

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
y : F
h : y ∈ Set.range ↑f
⊢ ∃ x, (x, y) ∈ f.graph

Tactic:
rw [Set.mem_range] at 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
y : F
h : ∃ y_1, ↑f y_1 = y
⊢ ∃ x, (x, y) ∈ f.graph

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

Tactic:
obtain ⟨x, h⟩ := h

Result:
case 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
y : F
x✝ : E
x : ↥f.domain
h : ↑x = (x✝, y).1 ∧ ↑f x = (x✝, y).2
⊢ y ∈ Set.range ↑f

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
y : F
⊢ y ∈ Set.range ↑f ↔ ∃ x, (x, y) ∈ f.graph

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
y : F
h : y ∈ Set.range ↑f
⊢ ∃ x, (x, y) ∈ f.graph

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
y : F
h : ∃ x, (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

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
y : F
h : ∃ y_1, ↑f y_1 = y
⊢ ∃ x, (x, y) ∈ f.graph

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

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

Tactic:
exact f.mem_graph ⟨x, hx⟩

Result:
no goals