α : Type ?u.1488
β : Type ?u.1491
M✝ : Type ?u.1494
N : Type ?u.1497
P : Type ?u.1500
G : Type ?u.1503
H : Type ?u.1506
F : Type u_3
R : Type u_1
M : Type u_2
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ ↑f 0
α : Type ?u.1488
β : Type ?u.1491
M✝ : Type ?u.1494
N : Type ?u.1497
P : Type ?u.1500
G : Type ?u.1503
H : Type ?u.1506
F : Type u_3
R : Type u_1
M : Type u_2
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ 0
rw [← ZeroHomClass.map_zero f]
no goals
α : Type ?u.1488
β : Type ?u.1491
M✝ : Type ?u.1494
N : Type ?u.1497
P : Type ?u.1500
G : Type ?u.1503
H : Type ?u.1506
F : Type u_3
R : Type u_1
M : Type u_2
inst✝³ : Zero R
r : R
inst✝² : NeZero r
inst✝¹ : Zero M
inst✝ : ZeroHomClass F R M
f : F
hf : Function.Injective ↑f
⊢ ↑f r ≠ ↑f 0
exact hf.ne NeZero.out