case h
R : Type u_2
R₂ : Type ?u.103212
K : Type ?u.103215
M : Type u_1
M₂ : Type ?u.103221
V : Type ?u.103224
S : Type ?u.103227
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') ↔ x✝ ∈ ↑p + ↑p'
R : Type u_2
R₂ : Type ?u.103212
K : Type ?u.103215
M : Type u_1
M₂ : Type ?u.103221
V : Type ?u.103224
S : Type ?u.103227
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') = ↑p + ↑p'
ext
case h
R : Type u_2
R₂ : Type ?u.103212
K : Type ?u.103215
M : Type u_1
M₂ : Type ?u.103221
V : Type ?u.103224
S : Type ?u.103227
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✝) ↔ ∃ x y, x ∈ ↑p ∧ y ∈ ↑p' ∧ x + y = x✝
case h
R : Type u_2
R₂ : Type ?u.103212
K : Type ?u.103215
M : Type u_1
M₂ : Type ?u.103221
V : Type ?u.103224
S : Type ?u.103227
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') ↔ x✝ ∈ ↑p + ↑p'
rw [SetLike.mem_coe, mem_sup, Set.mem_add]
no goals
case h
R : Type u_2
R₂ : Type ?u.103212
K : Type ?u.103215
M : Type u_1
M₂ : Type ?u.103221
V : Type ?u.103224
S : Type ?u.103227
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✝) ↔ ∃ x y, x ∈ ↑p ∧ y ∈ ↑p' ∧ x + y = x✝
simp