Theorem: RectSubRect' (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
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₃
Tactic:
rw [← re_add_im z₀, ← re_add_im z₁, ← re_add_im z₂, ← re_add_im z₃]
State after:
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)

State before:
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)
Tactic:
exact RectSubRect x₀_le_x₁ x₁_le_x₂ x₂_le_x₃ y₀_le_y₁ y₁_le_y₂ y₂_le_y₃
State after:
no goals