awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
⊢ 0 < a
have pos : ∀ (ha : 0 < a), 0 < a
Tactic: by_cases! ha : 0 < a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddRightReflectLE R
h : b * a < c * a
hbc : b ≤ c
pos : ∀ (ha : 0 < a), 0 < a
⊢ 0 < a
have neg : ∀ (ha : a ≤ 0), 0 < a
Tactic: by_cases! ha : 0 < a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
c0 : 0 ≤ a
⊢ b * a ≤ max d b * max c a
have b0 : 0 ≤ max d b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
c0 : 0 ≤ a
b0 : 0 ≤ max d b
⊢ b * a ≤ max d b * max c a
have h₁ : b ≤ max d b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
a d : R
inst_2 : PosMulMono R
inst_3 : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
c0 : 0 ≤ a
b0 : 0 ≤ max d b
h₁ : b ≤ max d b
⊢ b * a ≤ max d b * max c a
have h₂ : a ≤ max c a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
⊢ 4 * a * b = 2 * a * b + 2 * a * b
have rw : 4 * (a * b) = 2 * a * b + 2 * a * b
Tactic: rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
rw : 4 * (a * b) = 2 * a * b + 2 * a * b
⊢ 4 * a * b = 2 * a * b + 2 * a * b
have rw₁ : HAdd.hAdd (α := R) 2 2 * (a * b) = 2 * a * b + 2 * a * b
Tactic: rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
rw : 4 * (a * b) = 2 * a * b + 2 * a * b
rw₁ : HAdd.hAdd (α := R) 2 2 * (a * b) = 2 * a * b + 2 * a * b
⊢ 4 * a * b = 2 * a * b + 2 * a * b
have rw₂ : 2 * (a * b) + 2 * (a * b) = 2 * a * b + 2 * a * b
Tactic: rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
rw : 4 * (a * b) = 2 * a * b + 2 * a * b
rw₁ : HAdd.hAdd (α := R) 2 2 * (a * b) = 2 * a * b + 2 * a * b
rw₂ : 2 * (a * b) + 2 * (a * b) = 2 * a * b + 2 * a * b
⊢ 4 * a * b = 2 * a * b + 2 * a * b
have rw₃ : 2 * (a * b) + 2 * (a * b) = 2 * (a * b) + 2 * (a * b)
Tactic: rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
⊢ 2 * a * b + 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
have bc : 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b =
    HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw : HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [add_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
⊢ 4 * a * b ≤ HPow.hPow (β := ℕ) (a + b) 2
have calc : 4 * a * b = 2 * a * b + 2 * a * b
Tactic: calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
calc : 4 * a * b = 2 * a * b + 2 * a * b
⊢ 4 * a * b ≤ HPow.hPow (β := ℕ) (a + b) 2
have calc₁ : 2 * a * b + 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
Tactic: calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
a b : R
calc : 4 * a * b = 2 * a * b + 2 * a * b
calc₁ : 2 * a * b + 2 * a * b ≤ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
⊢ 4 * a * b ≤ HPow.hPow (β := ℕ) (a + b) 2
have calc₂ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b =
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
⊢ 2 * r ≤ a + b
have apply : 2 * r * (2 * r) ≤ (a + b) * (a + b)
Tactic: apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
⊢ 2 * r * (2 * r) ≤ (a + b) * (a + b)
have rw : 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
Tactic: rw [mul_mul_mul_comm, ← pow_two r, two_mul, two_add_two_eq_four]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
⊢ 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
have grw : 4 * (a * b) ≤ (a + b) * (a + b)
Tactic: grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
grw : 4 * (a * b) ≤ (a + b) * (a + b)
⊢ 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
have grw₁ : 4 * a * b ≤ (a + b) * (a + b)
Tactic: grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
grw : 4 * (a * b) ≤ (a + b) * (a + b)
grw₁ : 4 * a * b ≤ (a + b) * (a + b)
⊢ 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
have grw₂ : HPow.hPow (β := ℕ) (a + b) 2 ≤ (a + b) * (a + b)
Tactic: grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : HPow.hPow (β := ℕ) r 2 ≤ a * b
grw : 4 * (a * b) ≤ (a + b) * (a + b)
grw₁ : 4 * a * b ≤ (a + b) * (a + b)
grw₂ : HPow.hPow (β := ℕ) (a + b) 2 ≤ (a + b) * (a + b)
⊢ 4 * HPow.hPow (β := ℕ) r 2 ≤ (a + b) * (a + b)
have grw₃ : (a + b) * (a + b) ≤ (a + b) * (a + b)
Tactic: grw [mul_le_mul_of_nonneg_left ht zero_le_four, ← mul_assoc, four_mul_le_sq_add a b, sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₃ : 0 < a ∧ b < 0 ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftReflectLT R
inst_5 : AddLeftStrictMono R
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₃ : 0 < a ∧ b < 0 ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₄ : 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftReflectLE R
inst_5 : AddLeftMono R
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₄ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
have rw : (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Tactic: rw [← neg_mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
have rw : (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Tactic: rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
⊢ a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
have rw : (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Tactic: rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₄ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₄ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₅ : b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₄ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
rw₅ : b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₆ : b ≤ x ∨ x ≤ a ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 ≤ x - a ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₁ : a ≤ x ∧ 0 ≤ x - b ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₂ : a ≤ x ∧ b ≤ x ∨ x - a ≤ 0 ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₃ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x - b ≤ 0 ↔ x ≤ a ∨ b ≤ x
rw₄ : a ≤ x ∧ b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
rw₅ : b ≤ x ∨ x ≤ a ∧ x ≤ b ↔ x ≤ a ∨ b ≤ x
rw₆ : b ≤ x ∨ x ≤ a ↔ x ≤ a ∨ b ≤ x
⊢ 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x
have rw₇ : x ≤ a ∨ b ≤ x ↔ x ≤ a ∨ b ≤ x
Tactic: rw [mul_nonneg_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos,
    and_iff_right_of_imp h.trans, and_iff_left_of_imp h.trans', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b
have rw : b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b
Tactic: rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]