case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
⊢ f.domain ≤ g.domain

case right
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
⊢ ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ g.domain }⦄, ↑x = ↑y → ↑f x = ↑g y
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
⊢ f ≤ g
constructor
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ ↑f { val := x, property := hx } = ↑g { val := y, property := hy }
case right
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
⊢ ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ g.domain }⦄, ↑x = ↑y → ↑f x = ↑g y
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ (y, ↑f { val := x, property := hx }) ∈ graph g
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ ↑f { val := x, property := hx } = ↑g { val := y, property := hy }
rw [image_iff]
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ (y, ↑f { val := x, property := hx }) ∈ graph f
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ (y, ↑f { val := x, property := hx }) ∈ graph g
refine' h _
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f { val := x, property := hx }) ∈ graph f
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑{ val := x, property := hx } = ↑{ val := y, property := hy }
⊢ (y, ↑f { val := x, property := hx }) ∈ graph f
simp only [Submodule.coe_mk] at hxy
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f { val := x, property := hx✝ }) ∈ graph f
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f { val := x, property := hx }) ∈ graph f
rw [hxy] at hx
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f { val := x, property := hx✝ } = ↑f { val := y, property := hx }
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f { val := x, property := hx✝ }) ∈ graph f
rw [← image_iff hx]
no goals
case right.mk.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f { val := x, property := hx✝ } = ↑f { val := y, property := hx }
simp [hxy]
case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
⊢ x ∈ g.domain
case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
⊢ f.domain ≤ g.domain
intro x hx
case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : ∃ y, (x, y) ∈ graph f
⊢ ∃ y, (x, y) ∈ graph g
case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : x ∈ f.domain
⊢ x ∈ g.domain
rw [mem_domain_iff] at hx⊢
case left.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
y : F
hx : (x, y) ∈ graph f
⊢ ∃ y, (x, y) ∈ graph g
case left
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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
hx : ∃ y, (x, y) ∈ graph f
⊢ ∃ y, (x, y) ∈ graph g
cases' hx with y hx
case left.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
y : F
hx : (x, y) ∈ graph f
⊢ (x, y) ∈ graph g
case left.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
y : F
hx : (x, y) ∈ graph f
⊢ ∃ y, (x, y) ∈ graph g
use y
no goals
case left.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.595684
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.596200
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : graph f ≤ graph g
x : E
y : F
hx : (x, y) ∈ graph f
⊢ (x, y) ∈ graph g
exact h hx