-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
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 ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have 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 ℂ)
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]