Theorem: RectSubRect
Proof state before:
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
Tactic:
refine ⟨⟨?_, ?_, ?_, ?_⟩, ?_, ?_, ?_, ?_⟩
Proof state after:
case refine_1
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 refine_2
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 refine_3
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 refine_4
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 refine_5
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 refine_6
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 refine_7
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 refine_8
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

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