Theorem: SkewPolynomial.eta (SkewPolynomials.lean)

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

State before:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
Tactic:
rfl
State after:
no goals