Theorem: RectSubRect (PrimeNumberTheoremAnd/Rectangle.lean)

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₃
⊢ Rectangle (↑x₁ + ↑y₁ * I) (↑x₂ + ↑y₂ * I) ⊆ Rectangle (↑x₀ + ↑y₀ * I) (↑x₃ + ↑y₃ * I)
Tactic:
rw [rect_subset_iff, mem_Rect, mem_Rect]
State after:
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

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 ⟨⟨?_, ?_, ?_, ?_⟩, ?_, ?_, ?_, ?_⟩
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

State before:
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
Tactic:
all_goals simpa using by linarith
State after:
no goals

State before:
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:
simpa using by linarith
State after:
no goals

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₃
⊢ y₀ ≤ y₃
Tactic:
linarith
State after:
no goals