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

State before:
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
Tactic:
convert inv_sub_antitoneOn_Icc a b 0 ha
State after:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
x✝ : R
⊢ x✝ = x✝ - 0

State before:
case h.e'_5.h.h.e'_3
R : Type u_1
inst✝ : LinearOrderedField R
a b : R
ha : 0 < a
x✝ : R
⊢ x✝ = x✝ - 0
Tactic:
ring
State after:
no goals