R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
⊢ Function.Injective Nat.cast
intro a b h
no goals
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Function.Injective ↑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]