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

case inr
ι : Type ?u.58702
α : Type u_1
β : Type ?u.58708
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : ¬a = 1
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
ι : Type ?u.58702
α : Type u_1
β : Type ?u.58708
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
rcases em (a = 1) with (rfl | ha)
no goals
case inl
ι : Type ?u.58702
α : Type u_1
β : Type ?u.58708
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
⊢ 1⁻¹ ≤ 1 ↔ 1 ≤ 0 ∨ 1 ≤ 1
simp [le_rfl]
no goals
case inr
ι : Type ?u.58702
α : Type u_1
β : Type ?u.58708
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : ¬a = 1
⊢ a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
simp only [Ne.le_iff_lt (Ne.symm ha), Ne.le_iff_lt (mt inv_eq_one.1 ha), inv_lt_one_iff]