Theorem: horizontalSegment_eq (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
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}
Tactic:
simpa [← hx, reProdIm]
State after:
no goals

State before:
z w : ℂ
c a₁ a₂ b : ℝ
x✝ : ℂ
hx : x✝ ∈ [[a₁, a₂]] ×ℂ {b}
⊢ x✝ ∈ re ⁻¹' [[a₁, a₂]] → x✝ ∈ im ⁻¹' {b} → x✝ ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]
Tactic:
simp_all [Complex.ext_iff]
State after:
no goals