case a
σ : Type ?u.4371968
R : Type u_1
inst✝ : CommSemiring R
φ ψ x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ coeff x n✝ = coeff y n✝
σ : Type ?u.4371968
R : Type u_1
inst✝ : CommSemiring R
φ ψ x y : R[X]
h : Coe.coe x = Coe.coe y
⊢ x = y
ext
case a
σ : Type ?u.4371968
R : Type u_1
inst✝ : CommSemiring R
φ ψ x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑x = ↑(PowerSeries.coeff R n✝) ↑y
case a
σ : Type ?u.4371968
R : Type u_1
inst✝ : CommSemiring R
φ ψ x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ coeff x n✝ = coeff y n✝
simp_rw [← coeff_coe]
no goals
case a
σ : Type ?u.4371968
R : Type u_1
inst✝ : CommSemiring R
φ ψ x y : R[X]
h : Coe.coe x = Coe.coe y
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) ↑x = ↑(PowerSeries.coeff R n✝) ↑y
congr