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 α
a b c d e : α
inst_3 : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ 0 ≤ 1 / e

Tactic:
one_div_nonneg.2 he

Premises used: Iff.mpr, one_div_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
inst_3 : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ 0 ≤ 1 / e

Tactic:
exact one_div_nonneg.2 he

Premises used: Iff.mpr, one_div_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ a * b / c ≤ d

Tactic:
rw [← mul_div_assoc] at h

Premises used: mul_div_assoc
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
h₁ : a * b / c ≤ d
⊢ 0 < c

Tactic:
rw [← mul_div_assoc] at h

Premises used: mul_div_assoc
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
rwa : a * b ≤ d * c
rwa₁ rwa₂ rwa₃ rwa₄ : a * b / c ≤ d
⊢ b * a ≤ d * c

Tactic:
rwa [mul_comm b, ← div_le_iff₀ hc]

Premises used: div_le_iff₀, mul_comm
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
ha : 0 ≤ a
⊢ Monotone (β := α) fun (x : α) ↦ x / a

Tactic:
fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha

Premises used: div_le_div_of_nonneg_right, Monotone
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
ha : 0 < a
⊢ StrictMono (β := α) fun (x : α) ↦ x / a

Tactic:
fun _b _c hbc ↦ div_lt_div_of_pos_right hbc ha

Premises used: StrictMono, div_lt_div_of_pos_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
β : Type u_4
inst_3 : Preorder β
f : β → α
hf : Monotone f
c : α
hc : 0 ≤ c
⊢ Monotone.{u_4, u_2} (β := α) fun (x : β) ↦ f x / c

Tactic:
(monotone_div_right_of_nonneg hc).comp hf

Premises used: Monotone.comp, monotone_div_right_of_nonneg
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
β : Type u_4
inst_4 : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono.{u_4, u_2} (β := α) fun (x : β) ↦ f x / c

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)

Premises used: Iff.mpr, inv_pos, div_eq_mul_inv, StrictMono.mul_const
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst_3 : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
hc : LT.lt.{u_2} (α := α) 0 2
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst_3 : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ LT.lt.{u_2} (α := α) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst_3 : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ LT.lt.{u_2} (α := α) 0 2

Tactic:
exact zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst_3 : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
hc : LT.lt.{u_2} (α := α) 0 2
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ StrictAntiOn (β := α) (fun (x : α) ↦ 1 / x) (Set.Ioi 0)

Tactic:
fun _ x1 _ y1 xy => (one_div_lt_one_div (Set.mem_Ioi.mp y1) (Set.mem_Ioi.mp x1)).mpr xy

Premises used: Iff.mpr, StrictAntiOn, Set.mem_Ioi, one_div_lt_one_div, Iff.mp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
(one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn)

Premises used: Iff.mpr, one_div_le_one_div, pow_right_mono₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
refine_1 : 0 < a ^ n
refine_2 : 0 < a ^ m
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn)

Premises used: Iff.mpr, one_div_le_one_div, pow_right_mono₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

Tactic:
pow_pos (zero_lt_one.trans_le a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

Tactic:
exact pow_pos (zero_lt_one.trans_le a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m

Tactic:
pow_pos (zero_lt_one.trans_le a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m

Tactic:
exact pow_pos (zero_lt_one.trans_le a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
(one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn)

Premises used: Iff.mpr, pow_lt_pow_right₀, one_div_lt_one_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
refine_1 : 0 < a ^ n
refine_2 : 0 < a ^ m
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn)

Premises used: Iff.mpr, pow_lt_pow_right₀, one_div_lt_one_div
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ n

Tactic:
pow_pos (zero_lt_one.trans a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ n

Tactic:
exact pow_pos (zero_lt_one.trans a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ m

Tactic:
pow_pos (zero_lt_one.trans a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ m

Tactic:
exact pow_pos (zero_lt_one.trans a1) _

Premises used: pow_pos, zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
⊢ Antitone.{0, u_2} (β := α) fun (n : ℕ) ↦ 1 / a ^ n

Tactic:
fun _ _ =>
  one_div_pow_le_one_div_pow_of_le a1

Premises used: Antitone, one_div_pow_le_one_div_pow_of_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
⊢ StrictAnti.{0, u_2} (β := α) fun (n : ℕ) ↦ 1 / a ^ n

Tactic:
fun _ _ =>
  one_div_pow_lt_one_div_pow_of_lt a1

Premises used: one_div_pow_lt_one_div_pow_of_lt, StrictAnti
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
⊢ StrictAntiOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Ioi 0)

Tactic:
fun _ hx _ hy xy =>
  (inv_lt_inv₀ hy hx).2 xy

Premises used: Iff.mpr, StrictAntiOn, inv_lt_inv₀
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
one_div_pow_le_one_div_pow_of_le a1 mn

Premises used: one_div_pow_le_one_div_pow_of_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
h : (a ^ n)⁻¹ = 1 / a ^ n
h₁ : (a ^ m)⁻¹ = 1 / a ^ m
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Tactic:
convert! one_div_pow_le_one_div_pow_of_le a1 mn using 1

Premises used: one_div_pow_le_one_div_pow_of_le
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
one_div_pow_lt_one_div_pow_of_lt a1 mn

Premises used: one_div_pow_lt_one_div_pow_of_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
h : (a ^ n)⁻¹ = 1 / a ^ n
h₁ : (a ^ m)⁻¹ = 1 / a ^ m
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹

Tactic:
convert! one_div_pow_lt_one_div_pow_of_lt a1 mn using 1

Premises used: one_div_pow_lt_one_div_pow_of_lt
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 ≤ a
⊢ Antitone.{0, u_2} (β := α) fun (n : ℕ) ↦ (a ^ n)⁻¹

Tactic:
fun _ _ =>
  inv_pow_le_inv_pow_of_le a1

Premises used: inv_pow_le_inv_pow_of_le, Antitone
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
a1 : 1 < a
⊢ StrictAnti.{0, u_2} (β := α) fun (n : ℕ) ↦ (a ^ n)⁻¹

Tactic:
fun _ _ =>
  inv_pow_lt_inv_pow_of_lt a1

Premises used: inv_pow_lt_inv_pow_of_lt, StrictAnti
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩

Premises used: LT.lt.le, le_mul_of_one_le_right, Iff.intro, LE.le.trans
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
refine : ∀ (h : ∀ (ε : α), 1 < ε → a ≤ b * ε), a ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

Tactic:
refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
inl : ∀ (hb : LE.le.{u_4} (α := α) 0 0) (h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε), a ≤ 0
inr : ∀ (hb : 0 < b), a ≤ b
⊢ a ≤ b

Tactic:
obtain rfl | hb := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : LE.le.{u_4} (α := α) 0 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ ∀ (ε : α), 1 < ε → a ≤ 0

Tactic:
simp_rw [zero_mul] at h

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : LE.le.{u_4} (α := α) 0 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0

Tactic:
h 2 one_lt_two

Premises used: one_lt_two, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : LE.le.{u_4} (α := α) 0 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0

Tactic:
exact h 2 one_lt_two

Premises used: one_lt_two, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb_1 : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b

Tactic:
le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb_1 : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
inr : ∀ (x : α) (hbx : b < x), a ≤ x
⊢ a ≤ b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb_1 : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ a ≤ b * (x / b)

Tactic:
h (x / b) ((one_lt_div hb).mpr hbx)

Premises used: Iff.mpr, one_lt_div, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb_1 : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
h₁ : x = b * (x / b)
⊢ a ≤ x

Tactic:
convert! h (x / b) ((one_lt_div hb).mpr hbx)

Premises used: Iff.mpr, one_lt_div, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb_1 : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
h₁ h₂ : x = x
⊢ x = b * (x / b)

Tactic:
rw [mul_div_cancel₀ _ hb.ne']

Premises used: mul_div_cancel₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
ha : 0 ≤ a
n : ℕ
h : n = 0
⊢ a / (↑n : α) ≤ a

Tactic:
simpa [h] using ha
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
ha : 0 < a
n : ℕ
hn : 2 ≤ n
⊢ a / (↑n : α) < a

Tactic:
div_lt_self ha (n.one_lt_cast.mpr hn)

Premises used: Iff.mpr, div_lt_self, Nat.one_lt_cast
-- 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 : IsGLB s b
inl : ∀ (ha : 0 < a), IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)
inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0), IsGLB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
⊢ IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)

Premises used: lt_or_eq_of_le, rfl
-- 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_1 : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
(OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs

Premises used: Iff.mpr, OrderIso.isGLB_image', OrderIso.mulLeft₀
-- 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_1 : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs

Premises used: Iff.mpr, OrderIso.isGLB_image', OrderIso.mulLeft₀
-- 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 : IsGLB s b
ha : LE.le.{u_2} (α := α) 0 0
inr : IsGLB (α := α) ((fun (a : α) ↦ 0) '' s) 0
⊢ IsGLB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)

Tactic:
simp_rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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 : IsGLB s b
ha : LE.le.{u_2} (α := α) 0 0
inr : IsGLB (α := α) {0} 0
⊢ IsGLB (α := α) ((fun (a : α) ↦ 0) '' s) 0

Tactic:
rw [hs.nonempty.image_const]

Premises used: Set.Nonempty.image_const, IsGLB.nonempty
-- 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 : IsGLB s b
ha : LE.le.{u_2} (α := α) 0 0
⊢ IsGLB (α := α) {0} 0

Tactic:
isGLB_singleton

Premises used: isGLB_singleton
-- 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 : IsGLB s b
ha : LE.le.{u_2} (α := α) 0 0
⊢ IsGLB (α := α) {0} 0

Tactic:
exact isGLB_singleton

Premises used: isGLB_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 : IsGLB s b
⊢ IsGLB ((fun (b : α) ↦ b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

Premises used: IsGLB.mul_left, mul_comm
-- 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
inl : ∀ (ha : 0 < a), IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)
inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0), IsLUB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
⊢ IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
obtain ha | rfl := ha.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- 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_1 : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
(OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs

Premises used: Iff.mpr, OrderIso.isLUB_image', OrderIso.mulLeft₀
-- 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_1 : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)

Tactic:
exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs

Premises used: Iff.mpr, OrderIso.isLUB_image', OrderIso.mulLeft₀
-- 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
inr : IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
⊢ IsLUB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)

Tactic:
simp_rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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
inr : ∀ (hs : IsLUB ∅ b), IsLUB.{u_2} (α := α) ((fun (a : α) ↦ 0) '' ∅) 0
inr₁ : ∀ (ne : s.Nonempty), IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
⊢ IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0

Tactic:
obtain rfl | ne := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
ha : LE.le.{u_2} (α := α) 0 0
hs : IsLUB ∅ b
inr : ∀ (hs : IsBot b), IsBot.{u_2} (α := α) 0
⊢ IsLUB.{u_2} (α := α) ((fun (a : α) ↦ 0) '' ∅) 0

Tactic:
simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢

Premises used: isLUB_empty_iff, Set.image_empty
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
ha : LE.le.{u_2} (α := α) 0 0
hs : IsBot b
⊢ b ≤ b + b

Tactic:
have hb := hs (b + b)
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
ha : LE.le.{u_2} (α := α) 0 0
hs : IsBot b
hb : b ≤ b + b
⊢ 0 ≤ b

Tactic:
rw [le_add_iff_nonneg_right] at hb

Premises used: le_add_iff_nonneg_right
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
ha : LE.le.{u_2} (α := α) 0 0
hs : IsBot b
hb : 0 ≤ b
⊢ IsBot.{u_2} (α := α) 0

Tactic:
hs.mono hb

Premises used: IsBot.mono
-- Module: Mathlib.Algebra.Order.Field.Basic
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
b : α
inst_3 : IsStrictOrderedRing α
ha : LE.le.{u_2} (α := α) 0 0
hs : IsBot b
hb : 0 ≤ b
⊢ IsBot.{u_2} (α := α) 0

Tactic:
exact hs.mono hb

Premises used: IsBot.mono
-- 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
inr : IsLUB (α := α) {0} 0
⊢ IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0

Tactic:
rw [ne.image_const]

Premises used: Set.Nonempty.image_const
-- 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:
isLUB_singleton

Premises used: isLUB_singleton