rw [and_assoc, and_comm]
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ x ∈ s ∧ p x ↔ (x ∈ t ∧ p x) ∧ x ∈ s
case h
𝕜 : Type ?u.10873
E : Type ?u.10876
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type ?u.10889
inst✝ : Preorder β
s✝ : Set E
f : E → β
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
x : α
⊢ p x ∧ x ∈ s ↔ x ∈ t ∧ p x ∧ x ∈ s