rw [rect_subset_iff, mem_Rect, mem_Rect]
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ Rectangle (↑x₁ + ↑y₁ * I) (↑x₂ + ↑y₂ * I) ⊆ Rectangle (↑x₀ + ↑y₀ * I) (↑x₃ + ↑y₃ * I)
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ ((↑x₀ + ↑y₀ * I).re ≤ (↑x₁ + ↑y₁ * I).re ∧
      (↑x₁ + ↑y₁ * I).re ≤ (↑x₃ + ↑y₃ * I).re ∧
        (↑x₀ + ↑y₀ * I).im ≤ (↑x₁ + ↑y₁ * I).im ∧ (↑x₁ + ↑y₁ * I).im ≤ (↑x₃ + ↑y₃ * I).im) ∧
    (↑x₀ + ↑y₀ * I).re ≤ (↑x₂ + ↑y₂ * I).re ∧
      (↑x₂ + ↑y₂ * I).re ≤ (↑x₃ + ↑y₃ * I).re ∧
        (↑x₀ + ↑y₀ * I).im ≤ (↑x₂ + ↑y₂ * I).im ∧ (↑x₂ + ↑y₂ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im

case zRe_lt_wRe
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).re ≤ (↑x₃ + ↑y₃ * I).re

case zIm_lt_wIm
z w : ℂ
c x₀ x₁ x₂ x₃ y₀ y₁ y₂ y₃ : ℝ
x₀_le_x₁ : x₀ ≤ x₁
x₁_le_x₂ : x₁ ≤ x₂
x₂_le_x₃ : x₂ ≤ x₃
y₀_le_y₁ : y₀ ≤ y₁
y₁_le_y₂ : y₁ ≤ y₂
y₂_le_y₃ : y₂ ≤ y₃
⊢ (↑x₀ + ↑y₀ * I).im ≤ (↑x₃ + ↑y₃ * I).im