case inl
ι : Type ?u.55403
α : Type u_1
β : Type ?u.55409
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : a ≤ 0
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

case inr
ι : Type ?u.55403
α : Type u_1
β : Type ?u.55409
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
ι : Type ?u.55403
α : Type u_1
β : Type ?u.55409
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
cases' le_or_lt a 0 with ha ha
no goals
case inl
ι : Type ?u.55403
α : Type u_1
β : Type ?u.55409
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : a ≤ 0
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
simp [ha, (inv_nonpos.2 ha).trans_lt zero_lt_one]
no goals
case inr
ι : Type ?u.55403
α : Type u_1
β : Type ?u.55409
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a
simp only [ha.not_le, false_or_iff, inv_lt_one_iff_of_pos ha]