R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.720040
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : { x // x ∈ f.domain }
⊢ ∃ a b, (∃ h, ↑f { val := a, property := (_ : (a, b).fst ∈ f.domain) } = b) ∧ b = ↑f x ∧ a = ↑x
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.720040
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : { x // x ∈ f.domain }
⊢ (↑f x, ↑x) ∈ graph (inverse hf)
simp only [inverse_graph, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left,
  exists_eq_left, LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
no goals
R : Type u_2
inst✝⁶ : Ring R
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.720040
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : { x // x ∈ f.domain }
⊢ ∃ a b, (∃ h, ↑f { val := a, property := (_ : (a, b).fst ∈ f.domain) } = b) ∧ b = ↑f x ∧ a = ↑x
exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩