case h
R : Type u_2
R₂ : Type ?u.109627
K : Type ?u.109630
M : Type u_1
M₂ : Type ?u.109636
V : Type ?u.109639
S : Type ?u.109642
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
R : Type u_2
R₂ : Type ?u.109627
K : Type ?u.109630
M : Type u_1
M₂ : Type ?u.109636
V : Type ?u.109639
S : Type ?u.109642
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
⊢ (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid
ext x
case h
R : Type u_2
R₂ : Type ?u.109627
K : Type ?u.109630
M : Type u_1
M₂ : Type ?u.109636
V : Type ?u.109639
S : Type ?u.109642
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
⊢ (∃ y, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x) ↔ ∃ y, y ∈ p.toAddSubmonoid ∧ ∃ z, z ∈ p'.toAddSubmonoid ∧ y + z = x
case h
R : Type u_2
R₂ : Type ?u.109627
K : Type ?u.109630
M : Type u_1
M₂ : Type ?u.109636
V : Type ?u.109639
S : Type ?u.109642
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
rw [mem_toAddSubmonoid, mem_sup, AddSubmonoid.mem_sup]
no goals
case h
R : Type u_2
R₂ : Type ?u.109627
K : Type ?u.109630
M : Type u_1
M₂ : Type ?u.109636
V : Type ?u.109639
S : Type ?u.109642
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
⊢ (∃ y, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x) ↔ ∃ y, y ∈ p.toAddSubmonoid ∧ ∃ z, z ∈ p'.toAddSubmonoid ∧ y + z = x
rfl