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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : y ∈ range ↑f
⊢ ∃ x, (x, y) ∈ graph f

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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : ∃ x, (x, y) ∈ graph f
⊢ y ∈ range ↑f
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
⊢ y ∈ range ↑f ↔ ∃ x, (x, y) ∈ graph f
constructor <;> intro h
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
h : (x, y) ∈ graph f
⊢ y ∈ range ↑f
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : ∃ x, (x, y) ∈ graph f
⊢ y ∈ range ↑f
cases' h with x h
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
h : ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
⊢ y ∈ range ↑f
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
h : (x, y) ∈ graph f
⊢ y ∈ range ↑f
rw [mem_graph_iff] at h
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ y ∈ range ↑f
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
h : ∃ y_1, ↑y_1 = (x, y).fst ∧ ↑f y_1 = (x, y).snd
⊢ y ∈ range ↑f
cases' h with x h
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ ∃ y_1, ↑f y_1 = y
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ y ∈ range ↑f
rw [Set.mem_range]
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ ↑f x = y
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ ∃ y_1, ↑f y_1 = y
use x
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = x✝ ∧ ↑f x = y
⊢ ↑f x = y
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = (x✝, y).fst ∧ ↑f x = (x✝, y).snd
⊢ ↑f x = y
simp only at h
no goals
case mpr.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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x✝ : E
x : { x // x ∈ f.domain }
h : ↑x = x✝ ∧ ↑f x = y
⊢ ↑f x = y
rw [h.2]
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : ∃ y_1, ↑f y_1 = y
⊢ ∃ x, (x, y) ∈ graph f
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : y ∈ range ↑f
⊢ ∃ x, (x, y) ∈ graph f
rw [Set.mem_range] at h
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ ∃ x, (x, y) ∈ graph f
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
h : ∃ y_1, ↑f y_1 = y
⊢ ∃ x, (x, y) ∈ graph f
rcases h with ⟨⟨x, hx⟩, h⟩
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ (x, y) ∈ graph f
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ ∃ x, (x, y) ∈ graph f
use x
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ (x, ↑f { val := x, property := hx }) ∈ graph f
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ (x, y) ∈ graph f
rw [← h]
no goals
case mp.intro.mk
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.585339
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.585855
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f : E →ₗ.[R] F
y : F
x : E
hx : x ∈ f.domain
h : ↑f { val := x, property := hx } = y
⊢ (x, ↑f { val := x, property := hx }) ∈ graph f
exact f.mem_graph ⟨x, hx⟩