simpa [← hx, reProdIm]
z w : ℂ
c a b₁ b₂ : ℝ
x✝² : ℂ
hx✝ : x✝² ∈ (fun y => ↑a + ↑y * I) '' [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]] ∧ (fun y => ↑a + ↑y * I) x✝¹ = x✝²
left✝ : x✝¹ ∈ [[b₁, b₂]]
hx : (fun y => ↑a + ↑y * I) x✝¹ = x✝²
⊢ x✝² ∈ {a} ×ℂ [[b₁, b₂]]
no goals