-- Module: Mathlib.Analysis.Complex.Convex
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₄ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₅ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹'
          (Prod.mk z.re '' {z.im, w.im} ∪ SProd.sprod (α := Set ℝ) (β := Set ℝ) {w.re} {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₆ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          (Prod.mk z.re '' {z.im, w.im} ∪ Prod.mk w.re '' {z.im, w.im})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₇ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          ({(z.re, z.im), (z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)})) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₈ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          (insert (z.re, z.im) ({(z.re, w.im)} ∪ {(w.re, z.im), (w.re, w.im)}))) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₉ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (preimage (β := ℝ × ℝ) (⇑equivRealProd : (a : ℂ) → ℝ × ℝ)
          {(z.re, z.im), (z.re, w.im), (w.re, z.im), (w.re, w.im)}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₁₀ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (image (α := ℝ × ℝ) (⇑equivRealProd.symm : (a : ℝ × ℝ) → ℂ)
          {(z.re, z.im), (z.re, w.im), (w.re, z.im), (w.re, w.im)}) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₁₁ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (z.re, z.im) : ℂ)
          (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (z.re, w.im) : ℂ)
            (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (w.re, z.im) : ℂ)
              (image (α := ℝ × ℝ) (⇑equivRealProd.symm : (a : ℝ × ℝ) → ℂ) {(w.re, w.im)})))) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₁₂ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (z.re, z.im) : ℂ)
          (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (z.re, w.im) : ℂ)
            (insert (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (w.re, z.im) : ℂ)
              (singleton (α := ℂ) ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) (w.re, w.im) : ℂ))))) :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
simp_rw₁₃ :
  Eq (α := Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
        {(↑z.re : ℂ) + (↑z.im : ℂ) * I, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I,
          (↑w.re : ℂ) + (↑w.im : ℂ) * I} :
      Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}

Tactic:
simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]

Premises used: Set.image_pair, Complex.convexHull_reProdIm, Set.insert_eq, Set.image_singleton, segment_eq_uIcc, Complex.equivRealProd_symm_apply, Complex.Rectangle, Complex.preimage_equivRealProd_prod, Set.singleton_prod, convexHull_pair, Set.insert_prod, Set.insert_union, Set.image_insert_eq, Complex.re_add_im, Equiv.image_symm_eq_preimage