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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f { val := x, property := hx } ↔ ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f { val := x, property := hx } ↔ (x, y) ∈ graph f
rw [mem_graph_iff]
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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : y = ↑f { val := x, property := hx }
⊢ ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd

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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
⊢ y = ↑f { val := x, property := hx }
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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
⊢ y = ↑f { val := x, property := hx } ↔ ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
constructor <;> intro h
case mpr.intro.mk.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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : ↑{ val := x', property := hx' } = (x, y).fst
h2 : ↑f { val := x', property := hx' } = (x, y).snd
⊢ y = ↑f { val := x, property := hx }
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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
⊢ y = ↑f { val := x, property := hx }
rcases h with ⟨⟨x', hx'⟩, ⟨h1, h2⟩⟩
case mpr.intro.mk.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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : x' = x
h2 : ↑f { val := x', property := hx' } = y
⊢ y = ↑f { val := x, property := hx }
case mpr.intro.mk.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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : ↑{ val := x', property := hx' } = (x, y).fst
h2 : ↑f { val := x', property := hx' } = (x, y).snd
⊢ y = ↑f { val := x, property := hx }
simp only [Submodule.coe_mk] at h1 h2
no goals
case mpr.intro.mk.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.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
x' : E
hx' : x' ∈ f.domain
h1 : x' = x
h2 : ↑f { val := x', property := hx' } = y
⊢ y = ↑f { val := x, property := hx }
simp only [← h2, h1]
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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : y = ↑f { val := x, property := hx }
⊢ ↑{ val := x, property := hx } = (x, y).fst ∧ ↑f { val := x, property := hx } = (x, y).snd
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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : y = ↑f { val := x, property := hx }
⊢ ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
use ⟨x, hx⟩
no goals
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
G : Type ?u.579950
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.580466
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
x : E
y : F
hx : x ∈ f.domain
h : y = ↑f { val := x, property := hx }
⊢ ↑{ val := x, property := hx } = (x, y).fst ∧ ↑f { val := x, property := hx } = (x, y).snd
simp [h]