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