linarith [show s.re = -1 from congrArg _ hc]
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
xpos : 0 < x
s : ℂ
x✝ : s ∈ Icc (-1 / 2) σ ×ℂ univ \ {0}
hc✝ : s ∈ {0, -1}
left✝ : -1 / 2 ≤ s.re
right✝¹ : s.re ≤ σ
right✝ : s ∈ im ⁻¹' univ
hs0 : s ∉ {0}
hc : s ∈ {-1}
⊢ False
no goals