awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : LE.le.{u_2} (α := α) 0 0
ne : s.Nonempty
⊢ IsLUB (α := α) {0} 0

Tactic:
exact isLUB_singleton

Premises used: isLUB_singleton
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b : α
inst_3 : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun (b : α) ↦ b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

Premises used: IsLUB.mul_left, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
⊢ 0 < a / max (b + 1) 1

Tactic:
have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ ∃ (c : α), 0 < c ∧ b * c < a

Tactic:
⟨a / max (b + 1) 1, this, ?_⟩

Premises used: HDiv.hDiv, HAdd.hAdd, Max.max, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
refine : b * (a / max (b + 1) 1) < a
⊢ ∃ (c : α), 0 < c ∧ b * c < a

Tactic:
refine ⟨a / max (b + 1) 1, this, ?_⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
rw : b < max (b + 1) 1
⊢ b * (a / max (b + 1) 1) < a

Tactic:
rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']

Premises used: lt_div_iff₀, LT.lt.ne', div_div_cancel₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < max (b + 1) 1

Tactic:
lt_max_iff.2 (Or.inl <| lt_add_one _)

Premises used: Iff.mpr, lt_add_one, Or.inl, lt_max_iff
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < max (b + 1) 1

Tactic:
exact lt_max_iff.2 (Or.inl <| lt_add_one _)

Premises used: Iff.mpr, lt_add_one, Or.inl, lt_max_iff
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
rwa : b < a / c
rwa₁ rwa₂ rwa₃ rwa₄ : b * c < a
⊢ b < c⁻¹ * a

Tactic:
rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]

Premises used: lt_div_iff₀, div_eq_inv_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
hc : 0 ≤ c
a b : α
⊢ min (a / c) (b / c) = min a b / c

Tactic:
(monotone_div_right_of_nonneg hc).map_min.symm

Premises used: Monotone.map_min, monotone_div_right_of_nonneg, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
hc : 0 ≤ c
a b : α
⊢ max (a / c) (b / c) = max a b / c

Tactic:
(monotone_div_right_of_nonneg hc).map_max.symm

Premises used: Monotone.map_max, monotone_div_right_of_nonneg, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
rw : 0 < -a⁻¹ ↔ a < 0
rw₁ : 0 < (-a)⁻¹ ↔ a < 0
rw₂ : 0 < -a ↔ a < 0
rw₃ rw₄ : a < 0 ↔ a < 0
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]

Premises used: neg_pos, inv_neg, inv_pos
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
grind [inv_lt_zero', le_iff_eq_or_lt]

Premises used: le_iff_eq_or_lt, inv_lt_zero'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a / b

Tactic:
div_eq_mul_inv a b ▸ mul_nonneg_of_nonpos_of_nonpos ha (inv_nonpos'.2 hb)

Premises used: Iff.mpr, Eq.rec, div_eq_mul_inv, mul_nonneg_of_nonpos_of_nonpos, Eq.symm, inv_nonpos'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ 0 < a / b

Tactic:
div_eq_mul_inv a b ▸ mul_pos_of_neg_of_neg ha (inv_lt_zero'.2 hb)

Premises used: Iff.mpr, inv_lt_zero', Eq.rec, div_eq_mul_inv, Eq.symm, mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
⊢ a / b < 0

Tactic:
div_eq_mul_inv a b ▸ mul_neg_of_neg_of_pos ha (inv_pos.2 hb)

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, Eq.rec, inv_pos, div_eq_mul_inv, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
hb : b < 0
⊢ a / b < 0

Tactic:
div_eq_mul_inv a b ▸ mul_neg_of_pos_of_neg ha (inv_lt_zero'.2 hb)

Premises used: Iff.mpr, inv_lt_zero', Eq.rec, div_eq_mul_inv, Eq.symm, mul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c ≤ a ↔ a * c ≤ b
rw₁ rw₂ : a * c ≤ b ↔ a * c ≤ b
⊢ b / c ≤ a ↔ c * a ≤ b

Tactic:
rw [mul_comm, div_le_iff_of_neg hc]

Premises used: div_le_iff_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a ≤ b / - -c ↔ b ≤ a * - -c
rw₁ : a ≤ b / - -c ↔ b ≤ -(a * -c)
rw₂ : a ≤ -(b / -c) ↔ b ≤ -(a * -c)
rw₃ : b / -c ≤ -a ↔ b ≤ -(a * -c)
rw₄ : b ≤ -a * -c ↔ b ≤ -(a * -c)
rw₅ rw₆ : b ≤ -(a * -c) ↔ b ≤ -(a * -c)
⊢ a ≤ b / c ↔ b ≤ a * c

Tactic:
rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]

Premises used: Iff.mpr, div_le_iff₀, neg_pos, le_neg, neg_neg, div_neg, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a ≤ b / c ↔ b ≤ a * c
rw₁ rw₂ : b ≤ a * c ↔ b ≤ a * c
⊢ a ≤ b / c ↔ b ≤ c * a

Tactic:
rw [mul_comm, le_div_iff_of_neg hc]

Premises used: le_div_iff_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c < a ↔ a * c < b
rw₁ rw₂ : a * c < b ↔ a * c < b
⊢ b / c < a ↔ c * a < b

Tactic:
rw [mul_comm, div_lt_iff_of_neg hc]

Premises used: div_lt_iff_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
rw₁ : a < b / - -c ↔ b < -(a * -c)
rw₂ : a < -(b / -c) ↔ b < -(a * -c)
rw₃ : b / -c < -a ↔ b < -(a * -c)
rw₄ : b < -a * -c ↔ b < -(a * -c)
rw₅ rw₆ : b < -(a * -c) ↔ b < -(a * -c)
⊢ a < b / c ↔ b < a * c

Tactic:
rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]

Premises used: Iff.mpr, lt_neg, neg_pos, neg_neg, div_lt_iff₀, div_neg, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / c ↔ b < a * c
rw₁ rw₂ : b < a * c ↔ b < a * c
⊢ a < b / c ↔ b < c * a

Tactic:
rw [mul_comm, lt_div_iff_of_neg hc]

Premises used: lt_div_iff_of_neg, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : b ≤ a
hb : b ≤ 0
⊢ a / b ≤ 1

Tactic:
simpa only [neg_div_neg_eq] using div_le_one_of_le₀ (neg_le_neg h) (neg_nonneg_of_nonpos hb)

Premises used: div_le_one_of_le₀, neg_div_neg_eq, neg_nonneg_of_nonpos, neg_le_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
rw₁ : b⁻¹ * a ≤ 1 ↔ b ≤ a
rw₂ : a / b ≤ 1 ↔ b ≤ a
rw₃ : 1 * b ≤ a ↔ b ≤ a
rw₄ rw₅ : b ≤ a ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]

Premises used: div_le_iff_of_neg, one_div, div_eq_inv_mul, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
rw₁ rw₂ : b⁻¹ ≤ a ↔ b⁻¹ ≤ a
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
rw [← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha), inv_inv]

Premises used: Iff.mpr, inv_le_inv_of_neg, inv_lt_zero', inv_inv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
rw₁ rw₂ : b ≤ a⁻¹ ↔ b ≤ a⁻¹
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
rw [← inv_le_inv_of_neg (inv_lt_zero'.2 hb) ha, inv_inv]

Premises used: Iff.mpr, inv_le_inv_of_neg, inv_lt_zero', inv_inv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a < b⁻¹ ↔ b⁻¹ * a < 1

Tactic:
have := div_lt_iff_of_neg ha (b := 1) (a := b⁻¹)
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₁ : ∀ (this : a⁻¹ < b⁻¹ ↔ a * b⁻¹ < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₂ : ∀ (this : a⁻¹ < b⁻¹ ↔ a / b < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₃ : ∀ (this : a⁻¹ < b⁻¹ ↔ 1 * b < a), a⁻¹ < b⁻¹ ↔ b < a
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : a⁻¹ < b⁻¹ ↔ b < a), a⁻¹ < b⁻¹ ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this

Premises used: div_lt_iff_of_neg, division_def, Inv.inv, one_div, mul_comm, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
simpa using inv_lt_inv_of_neg ha (inv_lt_zero'.2 hb)

Premises used: Iff.mpr, inv_lt_zero', inv_lt_inv_of_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
simpa using inv_lt_inv_of_neg (inv_lt_zero'.2 ha) hb

Premises used: Iff.mpr, inv_lt_zero', inv_lt_inv_of_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
c : α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Ioi c)

Tactic:
antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv₀ (sub_pos.mpr hb) (sub_pos.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl

Premises used: Iff.mpr, sub_pos, le_rfl, le_of_lt, sub_le_sub, antitoneOn_iff_forall_lt, inv_le_inv₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
c : α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Iio c)

Tactic:
antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
    inv_le_inv_of_neg (sub_neg.mpr hb) (sub_neg.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl

Premises used: sub_neg, Iff.mpr, le_rfl, inv_le_inv_of_neg, le_of_lt, sub_le_sub, antitoneOn_iff_forall_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
neg : ∀ (hab : ¬a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha

Premises used: Iff.mpr, sub_inv_antitoneOn_Ioi, Set.Icc_subset_Ioi_iff, AntitoneOn.mono
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha

Premises used: Iff.mpr, sub_inv_antitoneOn_Ioi, Set.Icc_subset_Ioi_iff, AntitoneOn.mono
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
hab : ¬a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

Premises used: Set.Subsingleton.antitoneOn
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
neg : ∀ (hab : ¬a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha

Premises used: Iff.mpr, AntitoneOn.mono, Set.Icc_subset_Iio_iff, sub_inv_antitoneOn_Iio
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha

Premises used: Iff.mpr, AntitoneOn.mono, Set.Icc_subset_Iio_iff, sub_inv_antitoneOn_Iio
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

Premises used: Set.Subsingleton.antitoneOn
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - 0)⁻¹) (Set.Ioi 0)

Tactic:
sub_inv_antitoneOn_Ioi (α := α)

Premises used: sub_inv_antitoneOn_Ioi
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
h : ∀ (x : α), x = x - 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Ioi 0)

Tactic:
convert! sub_inv_antitoneOn_Ioi (α := α)

Premises used: sub_inv_antitoneOn_Ioi
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
x : α
⊢ x = x - 0

Tactic:
(sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
x : α
⊢ x = x - 0

Tactic:
exact (sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - 0)⁻¹) (Set.Iio 0)

Tactic:
sub_inv_antitoneOn_Iio (α := α)

Premises used: sub_inv_antitoneOn_Iio
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
h : ∀ (x : α), x = x - 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Iio 0)

Tactic:
convert! sub_inv_antitoneOn_Iio (α := α)

Premises used: sub_inv_antitoneOn_Iio
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - 0)⁻¹) (Set.Icc a b)

Tactic:
sub_inv_antitoneOn_Icc_right ha

Premises used: sub_inv_antitoneOn_Icc_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
h : ∀ (x : α), x = x - 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Icc a b)

Tactic:
convert! sub_inv_antitoneOn_Icc_right ha

Premises used: sub_inv_antitoneOn_Icc_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
x : α
⊢ x = x - 0

Tactic:
(sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
x : α
⊢ x = x - 0

Tactic:
exact (sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - 0)⁻¹) (Set.Icc a b)

Tactic:
sub_inv_antitoneOn_Icc_left hb

Premises used: sub_inv_antitoneOn_Icc_left
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
h : ∀ (x : α), x = x - 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Icc a b)

Tactic:
convert! sub_inv_antitoneOn_Icc_left hb

Premises used: sub_inv_antitoneOn_Icc_left
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
x : α
⊢ x = x - 0

Tactic:
(sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
x : α
⊢ x = x - 0

Tactic:
exact (sub_zero _).symm

Premises used: sub_zero, Eq.symm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
rw : a * c⁻¹ ≤ b * c⁻¹
⊢ a / c ≤ b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a * c⁻¹ ≤ b * c⁻¹

Tactic:
mul_le_mul_of_nonpos_right h (inv_nonpos'.2 hc)

Premises used: Iff.mpr, mul_le_mul_of_nonpos_right, inv_nonpos'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a * c⁻¹ ≤ b * c⁻¹

Tactic:
exact mul_le_mul_of_nonpos_right h (inv_nonpos'.2 hc)

Premises used: Iff.mpr, mul_le_mul_of_nonpos_right, inv_nonpos'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
h : b < a
rw : a * c⁻¹ < b * c⁻¹
⊢ a / c < b / c

Tactic:
rw [div_eq_mul_inv a c, div_eq_mul_inv b c]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
h : b < a
⊢ a * c⁻¹ < b * c⁻¹

Tactic:
mul_lt_mul_of_neg_right h (inv_lt_zero'.2 hc)

Premises used: Iff.mpr, inv_lt_zero', mul_lt_mul_of_neg_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
h : b < a
⊢ a * c⁻¹ < b * c⁻¹

Tactic:
exact mul_lt_mul_of_neg_right h (inv_lt_zero'.2 hc)

Premises used: Iff.mpr, inv_lt_zero', mul_lt_mul_of_neg_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c * c ≤ a ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ a / c ≤ b / c ↔ b ≤ a

Tactic:
rw [div_le_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

Premises used: div_mul_cancel₀, div_le_iff_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c * c < a ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ a / c < b / c ↔ b < a

Tactic:
rw [div_lt_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]

Premises used: div_mul_cancel₀, div_lt_iff_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : a ≤ 1 * b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ 1 ≤ a / b ↔ a ≤ b

Tactic:
rw [le_div_iff_of_neg hb, one_mul]

Premises used: le_div_iff_of_neg, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : 1 * b ≤ a ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ a / b ≤ 1 ↔ b ≤ a

Tactic:
rw [div_le_iff_of_neg hb, one_mul]

Premises used: div_le_iff_of_neg, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : a < 1 * b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ 1 < a / b ↔ a < b

Tactic:
rw [lt_div_iff_of_neg hb, one_mul]

Premises used: lt_div_iff_of_neg, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : 1 * b < a ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ a / b < 1 ↔ b < a

Tactic:
rw [div_lt_iff_of_neg hb, one_mul]

Premises used: div_lt_iff_of_neg, one_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
simpa using inv_le_of_neg ha hb

Premises used: inv_le_of_neg