Theorem: SkewPolynomial.toFinsupp_add (SkewPolynomials.lean)

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

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

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