Theorem: DirectSum.support_subset (DividedPowers/ForMathlib/GradedAlgebra.lean)

State before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
⊢ (Function.support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)
Tactic:
intro m
State after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)

State before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ Function.support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)
Tactic:
rw [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not]
State after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0

State before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ x m = 0 → ↑(x m) = 0
Tactic:
intro hm'
State after:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0

State before:
ι : Type v
inst✝² : DecidableEq ι
M : Type w
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Tactic:
rw [hm', AddSubmonoid.coe_zero]
State after:
no goals