Theorem: reProdIm_subset_iff (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Tactic:
simp_rw [← preimage_equivRealProd_prod, equivRealProd.preimage_subset]
State after:
no goals