Theorem: Aux.inv_sub_antitoneOn_Icc (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedField R
a b c : R
ha : c < a
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
Tactic:
by_cases hab : a ≤ b
State after:
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)

State before:
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)
Tactic:
exact inv_sub_antitoneOn_gt c |>.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
State after:
no goals

State before:
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)
Tactic:
simp [hab, Set.Subsingleton.antitoneOn]
State after:
no goals