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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
⊢ x ∈ Submodule.map (LinearMap.fst R E F) (graph f) ↔ x ∈ f.domain
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.fst R E F) (graph f) = f.domain
ext x
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
⊢ (∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = x_1) ↔ x ∈ f.domain
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
⊢ x ∈ Submodule.map (LinearMap.fst R E F) (graph f) ↔ x ∈ f.domain
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]
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : ∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = 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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = x_1
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
⊢ (∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = x_1) ↔ x ∈ f.domain
constructor <;> intro h
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x✝ : E
x : F
hx : x✝ ∈ f.domain
h✝ : ↑f { val := x✝, property := (_ : (x✝, x).fst ∈ f.domain) } = x
⊢ x✝ ∈ f.domain
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : ∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = x_1
⊢ x ∈ f.domain
rcases h with ⟨x, hx, _⟩
no goals
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x✝ : E
x : F
hx : x✝ ∈ f.domain
h✝ : ↑f { val := x✝, property := (_ : (x✝, x).fst ∈ f.domain) } = x
⊢ x✝ ∈ f.domain
exact hx
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ h_1,
    ↑f { val := x, property := (_ : (x, ↑f { val := x, property := h }).fst ∈ f.domain) } =
      ↑f { val := x, property := h }
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1 h, ↑f { val := x, property := (_ : (x, x_1).fst ∈ f.domain) } = x_1
use f ⟨x, h⟩
no goals
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
G : Type ?u.484814
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ h_1,
    ↑f { val := x, property := (_ : (x, ↑f { val := x, property := h }).fst ∈ f.domain) } =
      ↑f { val := x, property := h }
simp only [h, exists_prop]