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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : Disjoint f.domain g.domain
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y
rw [disjoint_def] at h
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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
hy : y = 0
⊢ ↑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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
⊢ ↑f x = ↑g y
have hy : y = 0 := Subtype.eq (h y (hxy ▸ x.2) y.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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
hy : y = 0
hx : x = 0
⊢ ↑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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
hy : y = 0
⊢ ↑f x = ↑g y
have hx : x = 0 := Subtype.eq (hxy.trans <| congr_arg _ hy)
no goals
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.210345
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : E), x ∈ f.domain → x ∈ g.domain → x = 0
x : { x // x ∈ f.domain }
y : { x // x ∈ g.domain }
hxy : ↑x = ↑y
hy : y = 0
hx : x = 0
⊢ ↑f x = ↑g y
simp [*]