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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ graph f
⊢ x ∈ graph g
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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : f ≤ g
⊢ graph f ≤ graph g
intro x 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : ∃ y, ↑y = x.fst ∧ ↑f y = x.snd
⊢ ∃ y, ↑y = x.fst ∧ ↑g y = x.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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ graph f
⊢ x ∈ graph g
rw [mem_graph_iff] at hx⊢
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ∃ y, ↑y = x.fst ∧ ↑g y = x.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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : ∃ y, ↑y = x.fst ∧ ↑f y = x.snd
⊢ ∃ y, ↑y = x.fst ∧ ↑g y = x.snd
cases' hx with y hx
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑{ val := ↑y, property := (_ : ↑y ∈ g.domain) } = x.fst ∧ ↑g { val := ↑y, property := (_ : ↑y ∈ g.domain) } = x.snd
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ∃ y, ↑y = x.fst ∧ ↑g y = x.snd
use ⟨y, h.1 y.2⟩
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑g { val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) } = x.snd
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑{ val := ↑y, property := (_ : ↑y ∈ g.domain) } = x.fst ∧ ↑g { val := ↑y, property := (_ : ↑y ∈ g.domain) } = x.snd
simp only [hx, Submodule.coe_mk, eq_self_iff_true, true_and_iff]
case h.e'_2
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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑g { val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) } = ↑f y
case 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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑g { val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) } = x.snd
convert hx.2 using 1
case h.e'_2
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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑y = ↑{ val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) }
case h.e'_2
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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑g { val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) } = ↑f y
refine' (h.2 _).symm
no goals
case h.e'_2
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.601958
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.602474
inst✝² : Monoid M
inst✝¹ : DistribMulAction M F
inst✝ : SMulCommClass R M F
y✝ : M
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : { x // x ∈ f.domain }
hx : ↑y = x.fst ∧ ↑f y = x.snd
⊢ ↑y = ↑{ val := x.fst, property := (_ : (fun x => x ∈ g.domain) x.fst) }
simp only [hx.1, Submodule.coe_mk]