Theorem: segment_reProdIm_segment_eq_convexHull (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
simp_rw [← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm, reProdIm]
State after:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ (convexHull ℝ) (re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ (convexHull ℝ) (re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
exact congrArg _ <| Set.ext <| by simpa [Complex.ext_iff] using by tauto
State after:
no goals

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ ∀ (x : ℂ), x ∈ re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im} ↔ x ∈ {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
Tactic:
simpa [Complex.ext_iff] using by tauto
State after:
no goals

State before:
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ ∀ (x : ℂ),
    (x.re = z.re ∨ x.re = w.re) ∧ (x.im = z.im ∨ x.im = w.im) ↔
      x.re = z.re ∧ x.im = z.im ∨ x.re = z.re ∧ x.im = w.im ∨ x.re = w.re ∧ x.im = z.im ∨ x.re = w.re ∧ x.im = w.im
Tactic:
tauto
State after:
no goals