awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a ≤ a * 2 ↔ 0 ≤ a
⊢ a / 2 ≤ a ↔ 0 ≤ a
have rw₁ : a ≤ a + a ↔ 0 ≤ a
Tactic: rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a ≤ a * 2 ↔ 0 ≤ a
rw₁ : a ≤ a + a ↔ 0 ≤ a
⊢ a / 2 ≤ a ↔ 0 ≤ a
have rw₂ : 0 ≤ a ↔ 0 ≤ a
Tactic: rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
⊢ a / 2 < a ↔ 0 < a
have rw : a < a * 2 ↔ 0 < a
Tactic: rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a < a * 2 ↔ 0 < a
⊢ a / 2 < a ↔ 0 < a
have rw₁ : a < a + a ↔ 0 < a
Tactic: rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a : α
inst_3 : IsStrictOrderedRing α
rw : a < a * 2 ↔ 0 < a
rw₁ : a < a + a ↔ 0 < a
⊢ a / 2 < a ↔ 0 < a
have rw₂ : 0 < a ↔ 0 < a
Tactic: rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
⊢ a / 3 + a / 3 + a / 3 = a
have rw : (a + a) / 3 + a / 3 = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₁ : (a + a + a) / 3 = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
rw₁ : (a + a + a) / 3 = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₂ : (2 * a + a) / 3 = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
rw₁ : (a + a + a) / 3 = a
rw₂ : (2 * a + a) / 3 = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₃ : HAdd.hAdd (α := α) 2 1 * a / 3 = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
rw₁ : (a + a + a) / 3 = a
rw₂ : (2 * a + a) / 3 = a
rw₃ : HAdd.hAdd (α := α) 2 1 * a / 3 = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₄ : 3 * a / 3 = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a : α
rw : (a + a) / 3 + a / 3 = a
rw₁ : (a + a + a) / 3 = a
rw₂ : (2 * a + a) / 3 = a
rw₃ : HAdd.hAdd (α := α) 2 1 * a / 3 = a
rw₄ : 3 * a / 3 = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₅ : a = a
Tactic: rw [← add_div, ← add_div, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
    mul_div_cancel_left₀ a three_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a / (b * e) ≤ c / (d * e)
have rw : a / b * (1 / e) ≤ c / d * (1 / e)
Tactic: rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a / b * (1 / e) ≤ c / d * (1 / e)
have ha : 0 ≤ 1 / e
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
have h₁ : a * b / c ≤ d
Tactic: rw [← mul_div_assoc] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Semifield α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c
have rwa : a * b ≤ d * c
Tactic: rwa [mul_comm b, ← div_le_iff₀ hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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₂
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2
have hc : LT.lt.{u_2} (α := α) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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₂
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2
have hc : LT.lt.{u_2} (α := α) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
have refine_1 : 0 < a ^ n
Tactic: refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ 1 / a ^ n ≤ 1 / a ^ m
have refine_2 : 0 < a ^ m
Tactic: refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
have refine_1 : 0 < a ^ n
Tactic: refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ 1 / a ^ n < 1 / a ^ m
have refine_2 : 0 < a ^ m
Tactic: refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)⁻¹ ≤ (a ^ m)⁻¹
have h : (a ^ n)⁻¹ = 1 / a ^ n
Tactic: convert! one_div_pow_le_one_div_pow_of_le a1 mn using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹
have h₁ : (a ^ m)⁻¹ = 1 / a ^ m
Tactic: convert! one_div_pow_le_one_div_pow_of_le a1 mn using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)⁻¹ < (a ^ m)⁻¹
have h : (a ^ n)⁻¹ = 1 / a ^ n
Tactic: convert! one_div_pow_lt_one_div_pow_of_lt a1 mn using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹
have h₁ : (a ^ m)⁻¹ = 1 / a ^ m
Tactic: convert! one_div_pow_lt_one_div_pow_of_lt a1 mn using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε
have refine : ∀ (h : ∀ (ε : α), 1 < ε → a ≤ b * ε), a ≤ b
Tactic: refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b : α
hb : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
⊢ a ≤ b
have inl : ∀ (hb : LE.le.{u_4} (α := α) 0 0) (h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε), a ≤ 0
Tactic: obtain rfl | hb := hb.eq_or_lt
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a ≤ b
have inr : ∀ (hb : 0 < b), a ≤ b
Tactic: obtain rfl | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
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
have h₁ : ∀ (ε : α), 1 < ε → a ≤ 0
Tactic: simp_rw [zero_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
have inr : ∀ (x : α) (hbx : b < x), a ≤ x
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 ≤ x
have h₁ : x = b * (x / b)
Tactic: convert! h (x / b) ((one_lt_div hb).mpr hbx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ x = b * (x / b)
have h₁ : x = x
Tactic: rw [mul_div_cancel₀ _ hb.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 : α) ↦ a * b) '' s) (a * b)
have inl : ∀ (ha : 0 < a), IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)
Tactic: rcases lt_or_eq_of_le ha with (ha | rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ IsGLB ((fun (b : α) ↦ a * b) '' s) (a * b)
have inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0), IsGLB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
Tactic: rcases lt_or_eq_of_le ha with (ha | rfl)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
have inr : IsGLB (α := α) ((fun (a : α) ↦ 0) '' s) 0
Tactic: simp_rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 (α := α) ((fun (a : α) ↦ 0) '' s) 0
have inr : IsGLB (α := α) {0} 0
Tactic: rw [hs.nonempty.image_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 : α) ↦ a * b) '' s) (a * b)
have inl : ∀ (ha : 0 < a), IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)
Tactic: obtain ha | rfl := ha.lt_or_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ IsLUB ((fun (b : α) ↦ a * b) '' s) (a * b)
have inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0), IsLUB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
Tactic: obtain ha | rfl := ha.lt_or_eq
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ IsLUB ((fun (b : α) ↦ 0 * b) '' s) (0 * b)
have inr : IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
Tactic: simp_rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
have inr : ∀ (hs : IsLUB ∅ b), IsLUB.{u_2} (α := α) ((fun (a : α) ↦ 0) '' ∅) 0
Tactic: obtain rfl | ne := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
have inr₁ : ∀ (ne : s.Nonempty), IsLUB (α := α) ((fun (a : α) ↦ 0) '' s) 0
Tactic: obtain rfl | ne := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ IsLUB.{u_2} (α := α) ((fun (a : α) ↦ 0) '' ∅) 0
have inr : ∀ (hs : IsBot b), IsBot.{u_2} (α := α) 0
Tactic: simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
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
⊢ IsBot.{u_2} (α := α) 0
have hb : b ≤ b + b
Tactic: have hb := hs (b + b)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
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
⊢ IsBot.{u_2} (α := α) 0
have hb₁ : 0 ≤ b
Tactic: rw [le_add_iff_nonneg_right] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 (α := α) ((fun (a : α) ↦ 0) '' s) 0
have inr : IsLUB (α := α) {0} 0
Tactic: rw [ne.image_const]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
⊢ ∃ (c : α), 0 < c ∧ b * c < a
have this : 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))
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
have refine : b * (a / max (b + 1) 1) < a
Tactic: refine ⟨a / max (b + 1) 1, this, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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 * (a / max (b + 1) 1) < a
have rw : b < max (b + 1) 1
Tactic: rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ b < c⁻¹ * a
have rwa : b < a / c
Tactic: rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
⊢ a⁻¹ < 0 ↔ a < 0
have rw : 0 < -a⁻¹ ↔ a < 0
Tactic: rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
rw : 0 < -a⁻¹ ↔ a < 0
⊢ a⁻¹ < 0 ↔ a < 0
have rw₁ : 0 < (-a)⁻¹ ↔ a < 0
Tactic: rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a⁻¹ < 0 ↔ a < 0
have rw₂ : 0 < -a ↔ a < 0
Tactic: rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a⁻¹ < 0 ↔ a < 0
have rw₃ : a < 0 ↔ a < 0
Tactic: rw [← neg_pos, ← inv_neg, inv_pos, neg_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c ≤ a ↔ c * a ≤ b
have rw : b / c ≤ a ↔ a * c ≤ b
Tactic: rw [mul_comm, div_le_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ b / c ≤ a ↔ c * a ≤ b
have rw₁ : a * c ≤ b ↔ a * c ≤ b
Tactic: rw [mul_comm, div_le_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c
have rw : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a ≤ b / c ↔ b ≤ a * c
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ a ≤ b / c ↔ b ≤ a * c
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ a ≤ b / c ↔ b ≤ a * c
have rw₃ : b / -c ≤ -a ↔ b ≤ -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ a ≤ b / c ↔ b ≤ a * c
have rw₄ : b ≤ -a * -c ↔ b ≤ -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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)
⊢ a ≤ b / c ↔ b ≤ a * c
have rw₅ : b ≤ -(a * -c) ↔ b ≤ -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ c * a
have rw : a ≤ b / c ↔ b ≤ a * c
Tactic: rw [mul_comm, le_div_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ a ≤ b / c ↔ b ≤ c * a
have rw₁ : b ≤ a * c ↔ b ≤ a * c
Tactic: rw [mul_comm, le_div_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c < a ↔ c * a < b
have rw : b / c < a ↔ a * c < b
Tactic: rw [mul_comm, div_lt_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
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
⊢ b / c < a ↔ c * a < b
have rw₁ : a * c < b ↔ a * c < b
Tactic: rw [mul_comm, div_lt_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / c ↔ b < a * c
have rw : 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]