by_cases hab : a ≤ b
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
case pos
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

case neg
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)