case refine_1
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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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
⊢ x ∈ f.domain ↔ x ∈ g.domain

case refine_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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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 }
h' : ↑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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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
refine ext (Submodule.ext fun x => ?_) (fun x y h' => ?_)
case refine_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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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 }
h' : ↑x = ↑y
⊢ ↑f x = ↑g y
case refine_1
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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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
⊢ x ∈ f.domain ↔ x ∈ g.domain

case refine_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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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 }
h' : ↑x = ↑y
⊢ ↑f x = ↑g y
exact mem_domain_iff_of_eq_graph h
no goals
case refine_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.613202
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
M : Type ?u.613718
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 }
h' : ↑x = ↑y
⊢ ↑f x = ↑g y
exact (le_of_le_graph h.le).2 h'