case h
R : Type u_3
R₂ : Type ?u.249983
K : Type ?u.249986
M : Type u_1
M₂ : Type ?u.249992
V : Type ?u.249995
S : Type ?u.249998
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
M' : Type u_2
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
x✝ : M × M'
⊢ x✝ ∈ prod ⊤ ⊤ ↔ x✝ ∈ ⊤
R : Type u_3
R₂ : Type ?u.249983
K : Type ?u.249986
M : Type u_1
M₂ : Type ?u.249992
V : Type ?u.249995
S : Type ?u.249998
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
M' : Type u_2
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
⊢ prod ⊤ ⊤ = ⊤
ext
no goals
case h
R : Type u_3
R₂ : Type ?u.249983
K : Type ?u.249986
M : Type u_1
M₂ : Type ?u.249992
V : Type ?u.249995
S : Type ?u.249998
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
M' : Type u_2
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
q₁ q₁' : Submodule R M'
x✝ : M × M'
⊢ x✝ ∈ prod ⊤ ⊤ ↔ x✝ ∈ ⊤
simp