case inl
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hn : x < 0
⊢ Infinite x

case inr
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hp : x > 0
⊢ Infinite x
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
⊢ Infinite x
cases' lt_or_gt_of_ne h0 with hn hp
no goals
case inl
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hn : x < 0
⊢ Infinite x
exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)
no goals
case inr
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hp : x > 0
⊢ Infinite x
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)