R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
this : (↑f x, ↑x) ∈ graph (inverse hf)
⊢ ↑(inverse hf) y = ↑x
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
⊢ ↑(inverse hf) y = ↑x
have := mem_inverse_graph hf x
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
this : ∃ x_1, ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑x
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
this : (↑f x, ↑x) ∈ graph (inverse hf)
⊢ ↑(inverse hf) y = ↑x
simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left] at this
case intro
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑x
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
this : ∃ x_1, ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑x
rcases this with ⟨hx, h⟩
case intro
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) }
case intro
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑x
rw [← h]
case intro.e_a
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ y = { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) }
case intro
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ ↑(inverse hf) y = ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) }
congr
no goals
case intro.e_a
R : Type u_2
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_1
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.728555
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
y : { x // x ∈ (inverse hf).domain }
x : { x // x ∈ f.domain }
hxy : ↑f x = ↑y
hx : ↑f x ∈ (inverse hf).domain
h : ↑(inverse hf) { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) } = ↑x
⊢ y = { val := ↑f x, property := (_ : ↑f x ∈ (inverse hf).domain) }
simp only [hxy, Subtype.coe_eta]