case h
R✝ : Type ?u.111042
R₂ : Type ?u.111045
K : Type ?u.111048
M✝ : Type ?u.111051
M₂ : Type ?u.111054
V : Type ?u.111057
S : Type ?u.111060
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✝
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ toAddSubgroup (p ⊔ p') ↔ x ∈ toAddSubgroup p ⊔ toAddSubgroup p'
R✝ : Type ?u.111042
R₂ : Type ?u.111045
K : Type ?u.111048
M✝ : Type ?u.111051
M₂ : Type ?u.111054
V : Type ?u.111057
S : Type ?u.111060
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✝
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ toAddSubgroup (p ⊔ p') = toAddSubgroup p ⊔ toAddSubgroup p'
ext x
case h
R✝ : Type ?u.111042
R₂ : Type ?u.111045
K : Type ?u.111048
M✝ : Type ?u.111051
M₂ : Type ?u.111054
V : Type ?u.111057
S : Type ?u.111060
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✝
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x) ↔ ∃ y, y ∈ toAddSubgroup p ∧ ∃ z, z ∈ toAddSubgroup p' ∧ y + z = x
case h
R✝ : Type ?u.111042
R₂ : Type ?u.111045
K : Type ?u.111048
M✝ : Type ?u.111051
M₂ : Type ?u.111054
V : Type ?u.111057
S : Type ?u.111060
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✝
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ toAddSubgroup (p ⊔ p') ↔ x ∈ toAddSubgroup p ⊔ toAddSubgroup p'
rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]
no goals
case h
R✝ : Type ?u.111042
R₂ : Type ?u.111045
K : Type ?u.111048
M✝ : Type ?u.111051
M₂ : Type ?u.111054
V : Type ?u.111057
S : Type ?u.111060
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✝
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y, y ∈ p ∧ ∃ z, z ∈ p' ∧ y + z = x) ↔ ∃ y, y ∈ toAddSubgroup p ∧ ∃ z, z ∈ toAddSubgroup p' ∧ y + z = x
rfl