Theorem: rect_subset_iff (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ Rectangle z' w' ⊆ Rectangle z w ↔ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w
Tactic:
use fun h ↦ ⟨h (left_mem_rect z' w'), h (right_mem_rect z' w')⟩
State after:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w → Rectangle z' w' ⊆ Rectangle z w

State before:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
⊢ z' ∈ Rectangle z w ∧ w' ∈ Rectangle z w → Rectangle z' w' ⊆ Rectangle z w
Tactic:
intro ⟨⟨⟨hz're_ge, hz're_le⟩, ⟨hz'im_ge, hz'im_le⟩⟩,
  ⟨⟨hw're_ge, hw're_le⟩, ⟨hw'im_ge, hw'im_le⟩⟩⟩ x ⟨⟨hxre_ge, hxre_le⟩, ⟨hxim_ge, hxim_le⟩⟩
State after:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x ∈ Rectangle z w

State before:
case mpr
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x ∈ Rectangle z w
Tactic:
refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩
State after:
case mpr.refine_1
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.re ⊓ w.re ≤ x.re

case mpr.refine_2
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.re ≤ z.re ⊔ w.re

case mpr.refine_3
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.im ⊓ w.im ≤ x.im

case mpr.refine_4
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.im ≤ z.im ⊔ w.im

State before:
case mpr.refine_1
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.re ⊓ w.re ≤ x.re
Tactic:
exact (le_inf hz're_ge hw're_ge).trans hxre_ge
State after:
no goals

State before:
case mpr.refine_2
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.re ≤ z.re ⊔ w.re
Tactic:
exact (le_sup_iff.mp hxre_le).casesOn (fun h ↦ h.trans hz're_le) (fun h ↦ h.trans hw're_le)
State after:
no goals

State before:
case mpr.refine_3
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ z.im ⊓ w.im ≤ x.im
Tactic:
exact (le_inf hz'im_ge hw'im_ge).trans hxim_ge
State after:
no goals

State before:
case mpr.refine_4
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.im ≤ z.im ⊔ w.im
Tactic:
exact (le_sup_iff.mp hxim_le).casesOn (fun h ↦ h.trans hz'im_le) (fun h ↦ h.trans hw'im_le)
State after:
no goals