case h
p : ℕ
R : Type ?u.19259
S : Type ?u.19262
T : Type ?u.19265
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ coeff (mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n))) n = coeff x n
p : ℕ
R : Type ?u.19259
S : Type ?u.19262
T : Type ?u.19265
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n)) = x
ext n
no goals
case h
p : ℕ
R : Type ?u.19259
S : Type ?u.19262
T : Type ?u.19265
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ coeff (mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n))) n = coeff x n
simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]