-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem graph_map_fst_eq_domain (f : E →ₗ.[R] F) :
    f.graph.map (LinearMap.fst R E F) = f.domain

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
h : x ∈ f.domain
⊢ ∃ (h_1 : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = ↑f ⟨x, h⟩

Tactic:
simp only [h, exists_const]

Result:
no goals

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
⊢ x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain

Tactic:
simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
  LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]

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
⊢ (∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1) ↔ x ∈ f.domain

Proof state:
case h.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
h : ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
⊢ x ∈ f.domain

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

Result:
case h.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✝ : E
x : F
hx : x✝ ∈ f.domain
h✝ : ↑f ⟨x✝, ⋯⟩ = x
⊢ x✝ ∈ f.domain

Proof state:
case h.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✝ : E
x : F
hx : x✝ ∈ f.domain
h✝ : ↑f ⟨x✝, ⋯⟩ = x
⊢ x✝ ∈ f.domain

Tactic:
exact hx

Result:
no goals

Proof state:
case h.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
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1

Tactic:
use f ⟨x, 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
x : E
h : x ∈ f.domain
⊢ ∃ (h_1 : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = ↑f ⟨x, h⟩

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
⊢ (∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1) ↔ x ∈ f.domain

Tactic:
constructor <;> intro h

Result:
case h.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
h : ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
⊢ x ∈ f.domain

case h.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
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1

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
⊢ Submodule.map (LinearMap.fst R E F) f.graph = f.domain

Tactic:
ext 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
x : E
⊢ x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain