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