case h.mk
R : Type u_3
R₂ : Type ?u.251481
K : Type ?u.251484
M : Type u_1
M₂ : Type ?u.251490
V : Type ?u.251493
S : Type ?u.251496
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
y : M'
⊢ (x, y) ∈ prod ⊥ ⊥ ↔ (x, y) ∈ ⊥
R : Type u_3
R₂ : Type ?u.251481
K : Type ?u.251484
M : Type u_1
M₂ : Type ?u.251490
V : Type ?u.251493
S : Type ?u.251496
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 ⟨x, y⟩
no goals
case h.mk
R : Type u_3
R₂ : Type ?u.251481
K : Type ?u.251484
M : Type u_1
M₂ : Type ?u.251490
V : Type ?u.251493
S : Type ?u.251496
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
y : M'
⊢ (x, y) ∈ prod ⊥ ⊥ ↔ (x, y) ∈ ⊥
simp [Prod.zero_eq_mk]