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

State before:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Ioi c)
Tactic:
refine antitoneOn_iff_forall_lt.mpr ?_
State after:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ ∀ ⦃a : R⦄, a ∈ Set.Ioi c → ∀ ⦃b : R⦄, b ∈ Set.Ioi c → a < b → (b - c)⁻¹ ≤ (a - c)⁻¹

State before:
R : Type u_1
inst✝ : LinearOrderedField R
c : R
⊢ ∀ ⦃a : R⦄, a ∈ Set.Ioi c → ∀ ⦃b : R⦄, b ∈ Set.Ioi c → a < b → (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
intro a ha b hb hab
State after:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : a ∈ Set.Ioi c
b : R
hb : b ∈ Set.Ioi c
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹

State before:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : a ∈ Set.Ioi c
b : R
hb : b ∈ Set.Ioi c
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
rw [Set.mem_Ioi] at ha hb
State after:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹

State before:
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ (b - c)⁻¹ ≤ (a - c)⁻¹
Tactic:
gcongr
State after:
case ha
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ 0 < a - c

State before:
case ha
R : Type u_1
inst✝ : LinearOrderedField R
c a : R
ha : c < a
b : R
hb : c < b
hab : a < b
⊢ 0 < a - c
Tactic:
linarith
State after:
no goals