exact mul_ne_zero h0 <| add_ne_add_left 1 |>.mpr h1 |>.trans_eq (add_left_neg 1)
case hx.intro
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
x : ℂ
hx : x ∈ {0, -1}ᶜ
h0 : ¬x = 0
h1 : x ∉ {-1}
⊢ x * (x + 1) ≠ 0
no goals