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

State before:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type w
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R 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
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R M
A : ι → Submodule R M
x : ⨁ (i : ι), ↥(A i)
m : ι
hm' : x m = 0
⊢ ↑(x m) = 0
Tactic:
simp only [hm', Submodule.coe_zero]
State after:
no goals