case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ coeff (reflect N { toFinsupp := f }) i = coeff { toFinsupp := f } (↑(revAt N) i)
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N : ℕ
f : R[X]
i : ℕ
⊢ coeff (reflect N f) i = coeff f (↑(revAt N) i)
rcases f with ⟨f⟩
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ ↑(embDomain (revAt N) f) i = ↑f (↑(revAt N) i)
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ coeff (reflect N { toFinsupp := f }) i = coeff { toFinsupp := f } (↑(revAt N) i)
simp only [reflect, coeff]
no goals
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ ↑(embDomain (revAt N) f) i = ↑f (↑(revAt N) i)
calc
  Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by
    rw [revAt_invol]
  _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _
no goals
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ ↑(embDomain (revAt N) f) i = ↑(embDomain (revAt N) f) (↑(revAt N) (↑(revAt N) i))
rw [revAt_invol]