awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_lt_of_neg ha hb

Premises used: inv_lt_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 ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
simpa using le_inv_of_neg ha hb

Premises used: le_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 < 1 / b ↔ b < 1 / a

Tactic:
simpa using lt_inv_of_neg ha hb

Premises used: 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 : α
hb : b < 0
h : a ≤ b
rwa : b * (1 / a) ≤ 1
rwa₁ : b / a ≤ 1
rwa₂ rwa₃ rwa₄ rwa₅ : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]

Premises used: div_le_one_of_neg, div_le_iff_of_neg', div_eq_mul_one_div, LE.le.trans_lt
-- 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 : a < b
rwa : b * (1 / a) < 1
rwa₁ : b / a < 1
rwa₂ rwa₃ rwa₄ rwa₅ : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]

Premises used: div_lt_one_of_neg, div_lt_iff_of_neg', div_eq_mul_one_div, LT.lt.trans
-- 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 : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
simpa using one_div_le_one_div_of_neg_of_le (one_div b ▸ inv_lt_zero'.2 hb) h

Premises used: one_div_le_one_div_of_neg_of_le
-- 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 : 1 / a < 1 / b
⊢ b < a

Tactic:
simpa using one_div_lt_one_div_of_neg_of_lt (one_div b ▸ inv_lt_zero'.2 hb) h

Premises used: one_div_lt_one_div_of_neg_of_lt
-- 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 ≤ 1 / b ↔ b ≤ a

Tactic:
simpa [one_div] using inv_le_inv_of_neg ha hb

Premises used: inv_le_inv_of_neg, one_div
-- 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 < 1 / b ↔ b < a

Tactic:
simpa [one_div] using inv_lt_inv_of_neg ha hb

Premises used: inv_lt_inv_of_neg, one_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < HDiv.hDiv (α := α) 1 (-1)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : 1 / a < -1), 1 / a < -1
⊢ 1 / a < -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

Premises used: one_div_neg_one_eq_neg_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ HDiv.hDiv (α := α) 1 (-1)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : 1 / a ≤ -1), 1 / a ≤ -1
⊢ 1 / a ≤ -1

Tactic:
rwa [one_div_neg_one_eq_neg_one] at this

Premises used: one_div_neg_one_eq_neg_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ a - a / 2 = a / 2

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ a / 2 - a = -(a / 2)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
rwa₃ : a + -(a / 2) + b / 2 < b
rwa₄ : a - a / 2 + b / 2 < b
rwa₅ : a - a / 2 < b - b / 2
rwa₆ : a / 2 < b - b / 2
rwa₇ : a / 2 < b / 2
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : a < b
⊢ a + (b - a) / 2 < b

Tactic:
rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]

Premises used: add_assoc, div_lt_div_iff_of_pos_right, sub_eq_add_neg, HDiv.hDiv, add_comm, zero_lt_two', div_sub_div_same, lt_sub_iff_add_lt, OfNat.ofNat, sub_self_div_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
(inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))

Premises used: Iff.mpr, LE.le.trans_eq, inv_pos, inv_inv, zero_lt_two', OfNat.ofNat, inv_anti₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
refine : 2⁻¹ ≤ 1 - 1 / a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))

Premises used: Iff.mpr, LE.le.trans_eq, inv_pos, inv_inv, zero_lt_two', OfNat.ofNat, inv_anti₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
rw : 1 / a ≤ HSub.hSub (α := α) 1 2⁻¹
⊢ 2⁻¹ ≤ 1 - 1 / a

Tactic:
rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]

Premises used: add_comm, le_sub_iff_add_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 2⁻¹

Tactic:
(one_div a).le.trans (inv_anti₀ zero_lt_two a2)

Premises used: Eq.le, one_div, LE.le.trans, zero_lt_two, inv_anti₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
h : HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹
⊢ 1 / a ≤ HSub.hSub (α := α) 1 2⁻¹

Tactic:
convert! (one_div a).le.trans (inv_anti₀ zero_lt_two a2) using 1

Premises used: Eq.le, one_div, LE.le.trans, zero_lt_two, inv_anti₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
h : 1 = HAdd.hAdd (α := α) 2⁻¹ 2⁻¹
h₁ : 1 = HMul.hMul (α := α) 2 2⁻¹
h₂ h₃ : Eq.{u_2 + 1} (α := α) 1 1
⊢ HSub.hSub (α := α) 1 2⁻¹ = 2⁻¹

Tactic:
rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]

Premises used: mul_inv_cancel₀, two_mul, two_ne_zero, sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) < 0 ↔ a / c < b / d
rw₁ : a / c - b / d < 0 ↔ a / c < b / d
rw₂ rw₃ : a / c < b / d ↔ a / c < b / d
⊢ (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d

Tactic:
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]

Premises used: sub_lt_zero, mul_comm, div_sub_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
rw : (a * d - c * b) / (c * d) ≤ 0 ↔ a / c ≤ b / d
rw₁ : a / c - b / d ≤ 0 ↔ a / c ≤ b / d
rw₂ rw₃ : a / c ≤ b / d ↔ a / c ≤ b / d
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Tactic:
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]

Premises used: mul_comm, sub_nonpos, div_sub_div
-- 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
⊢ ∃ (c : α), b + c < a ∧ 0 < c

Tactic:
⟨(a - b) / 2, add_sub_div_two_lt h, div_pos (sub_pos_of_lt h) zero_lt_two⟩

Premises used: HSub.hSub, HDiv.hDiv, add_sub_div_two_lt, And.intro, Exists.intro, div_pos, zero_lt_two, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]

Premises used: inv_pos, mul_pos_iff, division_def, inv_lt_zero
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
simp [division_def, mul_neg_iff]

Premises used: division_def, mul_neg_iff
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp [division_def, mul_nonneg_iff]

Premises used: mul_nonneg_iff, division_def
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
⊢ a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
simp [division_def, mul_nonpos_iff]

Premises used: division_def, mul_nonpos_iff
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
inr : 1 < a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0
inr₁ : ∀ (hb : 0 < b), 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
simp [hb, hb.not_gt, one_lt_div_of_neg]

Premises used: one_lt_div_of_neg, LT.lt.not_gt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 1 < a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
simp [hb, hb.not_gt, one_lt_div]

Premises used: one_lt_div, LT.lt.not_gt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
inr : 1 ≤ a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0
inr₁ : ∀ (hb : 0 < b), 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
simp [hb, hb.not_gt, one_le_div_of_neg]

Premises used: LT.lt.not_gt, one_le_div_of_neg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a / 0 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a ∨ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0

Tactic:
simp [zero_lt_one.not_ge]

Premises used: zero_lt_one, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
simp [hb, hb.not_gt, one_le_div]

Premises used: LT.lt.not_gt, one_le_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
inr : a / 0 < 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a
inr₁ : ∀ (hb : 0 < b), a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
simp [hb, hb.not_gt, hb.ne, div_lt_one_of_neg]

Premises used: div_lt_one_of_neg, LT.lt.not_gt, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ a / 0 < 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a < 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 < a

Tactic:
simp [zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
simp [hb, hb.not_gt, div_lt_one, hb.ne.symm]

Premises used: Ne.symm, div_lt_one, LT.lt.not_gt, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
inl : ∀ (hb : b < 0), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
inr : a / 0 ≤ 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a
inr₁ : ∀ (hb : 0 < b), a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_gt, hb.ne, div_le_one_of_neg]

Premises used: div_le_one_of_neg, LT.lt.not_gt, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ a / 0 ≤ 1 ↔ LT.lt.{u_2} (α := α) 0 0 ∧ a ≤ 0 ∨ Eq.{u_2 + 1} (α := α) 0 0 ∨ LT.lt.{u_2} (α := α) 0 0 ∧ 0 ≤ a

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

Premises used: Ne.symm, div_le_one, LT.lt.not_gt, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : ∀ ε > 0, b - ε ≤ a
contrapose! : ∀ (h : a < b), ∃ ε > 0, a < b - ε
⊢ b ≤ a

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : a < b
⊢ ∃ ε > 0, a < b - ε

Tactic:
simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
    exists_add_lt_and_pos_of_lt h

Premises used: and_comm, gt_iff_lt, exists_add_lt_and_pos_of_lt, lt_sub_iff_add_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ 0 < b

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
obtain : ∀ (a' : α) (ha' : c / b < a') (a_a' : a' < a), ∃ a' ∈ Set.Ico 0 a, c < a' * b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)

Premises used: Iff.mpr, exists_between, div_lt_iff₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
a' : α
ha' : c / b < a'
a_a' : a' < a
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩

Premises used: LT.lt.le, div_lt_iff₀, And.intro, Exists.intro, Iff.mp, div_nonneg, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
a' : α
ha' : c / b < a'
a_a' : a' < a
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
simp_rw : ∀ (h : c < b * a), ∃ b' ∈ Set.Ico 0 b, c < b' * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
simp_rw [mul_comm a] at h ⊢

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a

Tactic:
exists_lt_mul_left_of_nonneg hb.le hc h

Premises used: _private.0.exists_lt_mul_left_of_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

Premises used: _private.0.exists_lt_mul_left_of_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
inl : ∀ (hb : b ≤ 0), ∃ a' > a, a' * b < c
inr : ∀ (hb : 0 < b), ∃ a' > a, a' * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
rcases le_or_gt b 0 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
inl : ∀ (a' : α) (ha' : a < a'), ∃ a' > a, a' * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
a' : α
ha' : a < a'
⊢ ∃ a' > a, a' * b < c

Tactic:
⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩

Premises used: LT.lt.le, LT.lt.trans_le', antitone_mul_right, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
a' : α
ha' : a < a'
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
inr : ∀ (a' : α) (ha' : a < a') (hc' : a' < c / b), ∃ a' > a, a' * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)

Premises used: Iff.mpr, lt_div_iff₀, exists_between
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a' > a, a' * b < c

Tactic:
⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

Premises used: lt_div_iff₀, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : a * b < c
simp_rw : ∀ (hc : b * a < c), ∃ b' > b, b' * a < c
⊢ ∃ b' > b, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Tactic:
exists_mul_left_lt₀ hc

Premises used: _private.0.exists_mul_left_lt₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Tactic:
exact exists_mul_left_lt₀ hc

Premises used: _private.0.exists_mul_left_lt₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
refine : ∀ (d : α) (hd : a * b < d), c ≤ d
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd : a * b < d
obtain : ∀ (a' : α) (ha' : a' > a) (hd : a' * b < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd

Premises used: _private.0.exists_mul_left_lt₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
obtain : ∀ (b' : α) (hb' : b' > b) (hd : a' * b' < d), c ≤ d
⊢ c ≤ d

Tactic:
obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd

Premises used: _private.0.exists_mul_right_lt₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd_2 : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
(h a' ha' b' hb').trans hd.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd_2 : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' ha' b' hb').trans hd.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense