Theorem: SkewPolynomial.toFinsupp_pow (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a : R[X;φ]
n : ℕ
⊢ (a ^ n).toFinsupp = SkewPolynomial.AddMonoidAlgebra.pow' φ n a.toFinsupp
Tactic:
cases a
State after:
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp =
    SkewPolynomial.AddMonoidAlgebra.pow' φ n { toFinsupp := toFinsupp✝ }.toFinsupp

State before:
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp =
    SkewPolynomial.AddMonoidAlgebra.pow' φ n { toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_pow]
State after:
no goals