[GOAL]
R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ ↑(Subsemiring.subtype S) ↑x = 0
[PROOFSTEP]
rw [map_natCast, h]
[GOAL]
R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ ↑(Subsemiring.subtype S) ↑x = 0
[PROOFSTEP]
rw [h, RingHom.map_zero]
[GOAL]
R : Type u
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
S : Subring R
x : ℕ
h : ↑x = 0
⊢ ↑(Subring.subtype S) ↑x = 0
[PROOFSTEP]
rw [map_natCast, h]
[GOAL]
R : Type u
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
S : Subring R
x : ℕ
h : ↑x = 0
⊢ ↑(Subring.subtype S) ↑x = 0
[PROOFSTEP]
rw [h, RingHom.map_zero]
