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 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c
have obtain : ∀ (d : R) (hcd : 0 = c + d), a * c ≤ b * c
Tactic: obtain ⟨d, hcd⟩ := exists_add_of_le hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c ≤ b * c
have refine : a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
Tactic: refine le_of_add_le_add_right (a := b * d + a * d) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d
have rw : b * d + (a * c + a * d) = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₁ : b * d + a * (c + d) = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₂ : b * d + a * 0 = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
rw₂ : b * d + a * 0 = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₃ : b * d + 0 = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
rw₂ : b * d + a * 0 = b * d
rw₃ : b * d + 0 = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₄ : b * d = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ b * d ≤ a * d
have ha : 0 ≤ d
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)
have rw : a * d = b * c + b * d + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₁ : a * d = b * (c + d) + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₂ : a * d = b * 0 + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
rw₂ : a * d = b * 0 + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₃ : a * d = 0 + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
rw₂ : a * d = b * 0 + a * d
rw₃ : a * d = 0 + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₄ : a * d = a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
have _ : a * c + (b * d + a * d) = b * d
Tactic: calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
_ : a * c + (b * d + a * d) = b * d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
have _₁ : b * d ≤ a * d
Tactic: calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
_ : a * c + (b * d + a * d) = b * d
_₁ : b * d ≤ a * d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
have _₂ : a * d = b * c + (b * d + a * d)
Tactic: calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
⊢ c * a < c * b
have obtain : ∀ (d : R) (hcd : 0 = c + d), c * a < c * b
Tactic: obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a < c * b
have refine : c * a + (d * b + d * a) < c * b + (d * b + d * a)
Tactic: refine (add_lt_add_iff_right (d * b + d * a)).1 ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) = d * b
have rw : d * b + (c * a + d * a) = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * b + (c * a + d * a) = d * b
⊢ c * a + (d * b + d * a) = d * b
have rw₁ : d * b + (c + d) * a = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * b + (c * a + d * a) = d * b
rw₁ : d * b + (c + d) * a = d * b
⊢ c * a + (d * b + d * a) = d * b
have rw₂ : d * b + 0 * a = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * b + (c * a + d * a) = d * b
rw₁ : d * b + (c + d) * a = d * b
rw₂ : d * b + 0 * a = d * b
⊢ c * a + (d * b + d * a) = d * b
have rw₃ : d * b + 0 = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * b + (c * a + d * a) = d * b
rw₁ : d * b + (c + d) * a = d * b
rw₂ : d * b + 0 * a = d * b
rw₃ : d * b + 0 = d * b
⊢ c * a + (d * b + d * a) = d * b
have rw₄ : d * b = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)
have rw : d * a = c * b + d * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * a = c * b + d * b + d * a
⊢ d * a = c * b + (d * b + d * a)
have rw₁ : d * a = (c + d) * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * a = c * b + d * b + d * a
rw₁ : d * a = (c + d) * b + d * a
⊢ d * a = c * b + (d * b + d * a)
have rw₂ : d * a = 0 * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * a = c * b + d * b + d * a
rw₁ : d * a = (c + d) * b + d * a
rw₂ : d * a = 0 * b + d * a
⊢ d * a = c * b + (d * b + d * a)
have rw₃ : d * a = 0 + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : d * a = c * b + d * b + d * a
rw₁ : d * a = (c + d) * b + d * a
rw₂ : d * a = 0 * b + d * a
rw₃ : d * a = 0 + d * a
⊢ d * a = c * b + (d * b + d * a)
have rw₄ : d * a = d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) < c * b + (d * b + d * a)
have _ : c * a + (d * b + d * a) = d * b
Tactic: calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
_ : c * a + (d * b + d * a) = d * b
⊢ c * a + (d * b + d * a) < c * b + (d * b + d * a)
have _₁ : d * a = c * b + (d * b + d * a)
Tactic: calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
⊢ a * c < b * c
have obtain : ∀ (d : R) (hcd : 0 = c + d), a * c < b * c
Tactic: obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * c < b * c
have refine : a * c + (b * d + a * d) < b * c + (b * d + a * d)
Tactic: refine (add_lt_add_iff_right (b * d + a * d)).1 ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) = b * d
have rw : b * d + (a * c + a * d) = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₁ : b * d + a * (c + d) = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₂ : b * d + a * 0 = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
rw₂ : b * d + a * 0 = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₃ : b * d + 0 = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
rw₂ : b * d + a * 0 = b * d
rw₃ : b * d + 0 = b * d
⊢ a * c + (b * d + a * d) = b * d
have rw₄ : b * d = b * d
Tactic: rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * d = b * c + (b * d + a * d)
have rw : a * d = b * c + b * d + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₁ : a * d = b * (c + d) + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₂ : a * d = b * 0 + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
rw₂ : a * d = b * 0 + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₃ : a * d = 0 + a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
rw : a * d = b * c + b * d + a * d
rw₁ : a * d = b * (c + d) + a * d
rw₂ : a * d = b * 0 + a * d
rw₃ : a * d = 0 + a * d
⊢ a * d = b * c + (b * d + a * d)
have rw₄ : a * d = a * d
Tactic: rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) < b * c + (b * d + a * d)
have _ : a * c + (b * d + a * d) = b * d
Tactic: calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
h : b < a
hc : c < 0
d : R
hcd : 0 = c + d
_ : a * c + (b * d + a * d) = b * d
⊢ a * c + (b * d + a * d) < b * c + (b * d + a * d)
have _₁ : a * d = b * c + (b * d + a * d)
Tactic: calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
hab : a ≤ b
hcd : c ≤ d
⊢ a * d + b * c ≤ a * c + b * d
have obtain : ∀ (d : R) (hd : 0 ≤ d) (hcd : c ≤ c + d), a * (c + d) + b * c ≤ a * c + b * (c + d)
Tactic: obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd
Cleared hypotheses: d, hcd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * (c + d) + b * c ≤ a * c + b * (c + d)
have rw : a * c + b * c + a * d ≤ a * c + b * c + b * d
Tactic: rw [mul_add, add_right_comm, mul_add, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
inst_5 : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ a * d + b * c ≤ a * c + b * d
have rw : b * c + a * d ≤ b * d + a * c
Tactic: rw [add_comm (a * d), add_comm (a * c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c d : R
inst_2 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
hab : a < b
hcd : c < d
⊢ a * d + b * c < a * c + b * d
have obtain : ∀ (d : R) (hd : 0 < d) (hcd : c < c + d), a * (c + d) + b * c < a * c + b * (c + d)
Tactic: obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd
Cleared hypotheses: d, hcd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b c : R
inst_2 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ a * (c + d) + b * c < a * c + b * (c + d)
have rw : a * c + b * c + a * d < a * c + b * c + b * d
Tactic: rw [mul_add, add_right_comm, mul_add, ← add_assoc]