no goals
α : Type u_1
M : Type u_2
N : Type ?u.113774
P : Type ?u.113777
R : Type u_3
S : Type ?u.113783
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
s t : Set α
h : Disjoint s t
⊢ supported M R s ⊓ supported M R t = ⊥
rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]