no goals
p : ℕ
R : Type u_2
S : Type u_1
T : Type ?u.80564
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.80579
β : Type ?u.80582
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x + y) = mapFun (↑f) x + mapFun (↑f) y
map_fun_tac