case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (invUnitsSub u)) = ↑(coeff S n✝) (invUnitsSub (↑(Units.map ↑f) u))
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ ↑(map f) (invUnitsSub u) = invUnitsSub (↑(Units.map ↑f) u)
ext
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑f ↑(u ^ (n✝ + 1))⁻¹ = ↑(↑(Units.map ↑f) (u ^ (n✝ + 1)))⁻¹
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (invUnitsSub u)) = ↑(coeff S n✝) (invUnitsSub (↑(Units.map ↑f) u))
simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
no goals
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑f ↑(u ^ (n✝ + 1))⁻¹ = ↑(↑(Units.map ↑f) (u ^ (n✝ + 1)))⁻¹
rfl