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

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

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