Theorem: Submodule.mem_sup_iff_exists_add (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ m ∈ M₁ ⊔ M₂ ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m
Tactic:
rw [← Submodule.mem_toAddSubmonoid (M₁ ⊔ M₂),
  Submodule.sup_toAddSubmonoid, AddSubmonoid.mem_sup]
State after:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ (∃ y ∈ M₁.toAddSubmonoid, ∃ z ∈ M₂.toAddSubmonoid, y + z = m) ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m

State before:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ (∃ y ∈ M₁.toAddSubmonoid, ∃ z ∈ M₂.toAddSubmonoid, y + z = m) ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m
Tactic:
simp only [Submodule.mem_toAddSubmonoid]
State after:
no goals