case inl
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

case inr.inl
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

case inr.inr
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
rcases lt_trichotomy b 0 with (hb | rfl | hb)
no goals
case inl
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
simp [hb, hb.not_lt, one_lt_div_of_neg]
no goals
case inr.inl
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a c d : α
n : ℤ
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0
simp [lt_irrefl, zero_le_one]
no goals
case inr.inr
ι : Type ?u.160788
α : Type u_1
β : Type ?u.160794
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
simp [hb, hb.not_lt, one_lt_div]