Theorem: verticalSegment_eq (PrimeNumberTheoremAnd/Rectangle.lean)

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

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