case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝ } + q) ⊆ support { toFinsupp := toFinsupp✝ } ∪ support q
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ support (p + q) ⊆ support p ∪ support q
rcases p with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) ⊆
    support { toFinsupp := toFinsupp✝¹ } ∪ support { toFinsupp := toFinsupp✝ }
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝ } + q) ⊆ support { toFinsupp := toFinsupp✝ } ∪ support q
rcases q with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (toFinsupp✝¹ + toFinsupp✝).support ⊆ toFinsupp✝¹.support ∪ toFinsupp✝.support
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) ⊆
    support { toFinsupp := toFinsupp✝¹ } ∪ support { toFinsupp := toFinsupp✝ }
simp only [← ofFinsupp_add, support]
no goals
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (toFinsupp✝¹ + toFinsupp✝).support ⊆ toFinsupp✝¹.support ∪ toFinsupp✝.support
exact support_add