awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₄ rw₅ : a * d = a * d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Premises used: add_assoc, zero_add, MulZeroClass.mul_zero, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 * d = b * c + (b * d + a * d)
⊢ a * c + (b * d + 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]
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonpos_right ha hb

Premises used: mul_le_mul_of_nonpos_right, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
ha : 0 ≤ c
⊢ c * b ≤ c * d

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ 0 ≤ c

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
ha : 0 ≤ a
hd : d ≤ 0
⊢ a * b ≤ c * d

Tactic:
(mul_le_mul_of_nonneg_left hbd ha).trans <| mul_le_mul_of_nonpos_right hca hd

Premises used: mul_le_mul_of_nonpos_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hac : a ≤ c
hdb : d ≤ b
hc : c ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ c * d

Tactic:
(mul_le_mul_of_nonneg_right hac hb).trans <| mul_le_mul_of_nonpos_left hdb hc

Premises used: mul_le_mul_of_nonpos_left, mul_le_mul_of_nonneg_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hca : c ≤ a
hdb : d ≤ b
hc : c ≤ 0
hb : b ≤ 0
⊢ a * b ≤ c * d

Tactic:
(mul_le_mul_of_nonpos_right hca hb).trans <| mul_le_mul_of_nonpos_left hdb hc

Premises used: mul_le_mul_of_nonpos_right, mul_le_mul_of_nonpos_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c d : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hca : c ≤ a
hdb : d ≤ b
ha : a ≤ 0
hd : d ≤ 0
⊢ a * b ≤ c * d

Tactic:
(mul_le_mul_of_nonpos_left hdb ha).trans <| mul_le_mul_of_nonpos_right hca hd

Premises used: mul_le_mul_of_nonpos_right, mul_le_mul_of_nonpos_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
hb : b ≤ 0
h : a ≤ 1
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Premises used: mul_le_mul_of_nonpos_right, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
hb : b ≤ 0
h : 1 ≤ a
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Premises used: mul_le_mul_of_nonpos_right, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
ha : a ≤ 0
h : b ≤ 1
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Premises used: mul_le_mul_of_nonpos_left, mul_one
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
ha : a ≤ 0
h : 1 ≤ b
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Premises used: mul_le_mul_of_nonpos_left, mul_one
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a : R
ha : a ≤ 0
⊢ Antitone (β := R) fun (x : R) ↦ a * x

Tactic:
fun _ _ b_le_c =>
  mul_le_mul_of_nonpos_left b_le_c ha

Premises used: mul_le_mul_of_nonpos_left, Antitone
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
a : R
ha : a ≤ 0
⊢ Antitone (β := R) fun (x : R) ↦ x * a

Tactic:
fun _ _ b_le_c =>
  mul_le_mul_of_nonpos_right b_le_c ha

Premises used: mul_le_mul_of_nonpos_right, Antitone
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hf : Monotone f
ha : a ≤ 0
⊢ Antitone.{u_1, u} (β := R) fun (x : α) ↦ a * f x

Tactic:
(antitone_mul_left ha).comp_monotone hf

Premises used: antitone_mul_left, Antitone.comp_monotone
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hf : Monotone f
ha : a ≤ 0
⊢ Antitone.{u_1, u} (β := R) fun (x : α) ↦ f x * a

Tactic:
(antitone_mul_right ha).comp_monotone hf

Premises used: Antitone.comp_monotone, antitone_mul_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hf : Antitone f
ha : a ≤ 0
⊢ Monotone.{u_1, u} (β := R) fun (x : α) ↦ a * f x

Tactic:
(antitone_mul_left ha).comp hf

Premises used: antitone_mul_left, Antitone.comp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosMono R
inst_5 : AddRightMono R
inst_6 : AddRightReflectLE R
hf : Antitone f
ha : a ≤ 0
⊢ Monotone.{u_1, u} (β := R) fun (x : α) ↦ f x * a

Tactic:
(antitone_mul_right ha).comp hf

Premises used: Antitone.comp, antitone_mul_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
inst_2 : Preorder α
f g : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : MulPosMono R
inst_6 : AddRightMono R
inst_7 : AddRightReflectLE R
hf : Antitone f
hg : Monotone g
hf₀ : ∀ (x : α), f x ≤ 0
hg₀ : ∀ (x : α), 0 ≤ g x
⊢ Antitone (f * g)

Tactic:
fun _ _ h =>
  mul_le_mul_of_nonpos_of_nonneg (hf h) (hg h) (hf₀ _) (hg₀ _)

Premises used: mul_le_mul_of_nonpos_of_nonneg, Antitone
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
inst_2 : Preorder α
f g : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : MulPosMono R
inst_6 : AddRightMono R
inst_7 : AddRightReflectLE R
hf : Monotone f
hg : Antitone g
hf₀ : ∀ (x : α), 0 ≤ f x
hg₀ : ∀ (x : α), g x ≤ 0
⊢ Antitone (f * g)

Tactic:
fun _ _ h =>
  mul_le_mul_of_nonneg_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)

Premises used: Antitone, mul_le_mul_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : Preorder R
inst_2 : Preorder α
f g : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulMono R
inst_5 : MulPosMono R
inst_6 : AddRightMono R
inst_7 : AddRightReflectLE R
hf : Antitone f
hg : Antitone g
hf₀ : ∀ (x : α), f x ≤ 0
hg₀ : ∀ (x : α), g x ≤ 0
⊢ Monotone (f * g)

Tactic:
fun _ _ h => mul_le_mul_of_nonpos_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)

Premises used: Monotone, mul_le_mul_of_nonpos_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a : R
inst_2 : ZeroLEOneClass R
inst_3 : MulPosStrictMono R
inst_4 : NeZero.{u} (R := R) 1
inst_5 : AddLeftStrictMono R
ha : 0 < a
⊢ a < 2 * a

Tactic:
lt_mul_of_one_lt_left ha one_lt_two

Premises used: one_lt_two, lt_mul_of_one_lt_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
obtain : ∀ (d : R) (hcd : 0 = c + d), c * a < c * b
⊢ c * a < c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le

Premises used: LT.lt.le, ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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

Tactic:
(add_lt_add_iff_right (d * b + d * a)).1 ?_

Premises used: HMul.hMul, HAdd.hAdd, Iff.mp, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
refine : c * a + (d * b + d * a) < c * b + (d * b + d * a)
⊢ c * a < c * b

Tactic:
refine (add_lt_add_iff_right (d * b + d * a)).1 ?_

Premises used: HMul.hMul, HAdd.hAdd, Iff.mp, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₄ rw₅ : d * b = d * b
⊢ c * a + (d * b + d * a) = d * b

Tactic:
rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

Premises used: add_mul, add_left_comm, MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 * b < d * a

Tactic:
mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc

Premises used: mul_lt_mul_of_pos_left, Eq.trans_lt, add_lt_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₄ rw₅ : d * a = d * a
⊢ d * a = c * b + (d * b + d * a)

Tactic:
rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Premises used: add_mul, add_assoc, MulZeroClass.zero_mul, zero_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
_₁ : d * a = c * b + (d * b + d * a)
⊢ c * a + (d * b + 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]

Premises used: mul_lt_mul_of_pos_left, Eq.trans_lt, add_lt_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
obtain : ∀ (d : R) (hcd : 0 = c + d), a * c < b * c
⊢ a * c < b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le

Premises used: LT.lt.le, ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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

Tactic:
(add_lt_add_iff_right (b * d + a * d)).1 ?_

Premises used: HMul.hMul, HAdd.hAdd, Iff.mp, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
refine : a * c + (b * d + a * d) < b * c + (b * d + a * d)
⊢ a * c < b * c

Tactic:
refine (add_lt_add_iff_right (b * d + a * d)).1 ?_

Premises used: HMul.hMul, HAdd.hAdd, Iff.mp, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₄ rw₅ : b * d = b * d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

Premises used: add_left_comm, MulZeroClass.mul_zero, mul_add, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ b * d < a * d

Tactic:
mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc

Premises used: mul_lt_mul_of_pos_right, Eq.trans_lt, add_lt_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw₄ rw₅ : a * d = a * d
⊢ a * d = b * c + (b * d + a * d)

Tactic:
rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Premises used: add_assoc, zero_add, MulZeroClass.mul_zero, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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 * d = b * c + (b * d + a * d)
⊢ a * c + (b * d + 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]

Premises used: mul_lt_mul_of_pos_right, Eq.trans_lt, add_lt_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
a b : R
ha : a < 0
hb : b < 0
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb

Premises used: MulZeroClass.zero_mul, mul_lt_mul_of_neg_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
hb : b < 0
h : a < 1
⊢ b < a * b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Premises used: mul_lt_mul_of_neg_right, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
hb : b < 0
h : 1 < a
⊢ a * b < b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Premises used: mul_lt_mul_of_neg_right, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
ha : a < 0
h : b < 1
⊢ a < a * b

Tactic:
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Premises used: mul_one, mul_lt_mul_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
ha : a < 0
h : 1 < b
⊢ a * b < a

Tactic:
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Premises used: mul_one, mul_lt_mul_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
a : R
ha : a < 0
⊢ StrictAnti (β := R) fun (x : R) ↦ a * x

Tactic:
fun _ _ b_lt_c =>
  mul_lt_mul_of_neg_left b_lt_c ha

Premises used: StrictAnti, mul_lt_mul_of_neg_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : AddRightStrictMono R
inst_5 : AddRightReflectLT R
a : R
ha : a < 0
⊢ StrictAnti (β := R) fun (x : R) ↦ x * a

Tactic:
fun _ _ b_lt_c =>
  mul_lt_mul_of_neg_right b_lt_c ha

Premises used: StrictAnti, mul_lt_mul_of_neg_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulStrictMono R
inst_5 : AddRightStrictMono R
inst_6 : AddRightReflectLT R
hf : StrictMono f
ha : a < 0
⊢ StrictAnti.{u_1, u} (β := R) fun (x : α) ↦ a * f x

Tactic:
(strictAnti_mul_left ha).comp_strictMono hf

Premises used: StrictAnti.comp_strictMono, strictAnti_mul_left
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddRightStrictMono R
inst_6 : AddRightReflectLT R
hf : StrictMono f
ha : a < 0
⊢ StrictAnti.{u_1, u} (β := R) fun (x : α) ↦ f x * a

Tactic:
(strictAnti_mul_right ha).comp_strictMono hf

Premises used: strictAnti_mul_right, StrictAnti.comp_strictMono
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : PosMulStrictMono R
inst_5 : AddRightStrictMono R
inst_6 : AddRightReflectLT R
hf : StrictAnti f
ha : a < 0
⊢ StrictMono.{u_1, u} (β := R) fun (x : α) ↦ a * f x

Tactic:
(strictAnti_mul_left ha).comp hf

Premises used: strictAnti_mul_left, StrictAnti.comp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
α : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
a : R
inst_2 : Preorder α
f : α → R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddRightStrictMono R
inst_6 : AddRightReflectLT R
hf : StrictAnti f
ha : a < 0
⊢ StrictMono.{u_1, u} (β := R) fun (x : α) ↦ f x * a

Tactic:
(strictAnti_mul_right ha).comp hf

Premises used: strictAnti_mul_right, StrictAnti.comp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
obtain : ∀ (d : R) (hd : 0 ≤ d) (hcd : c ≤ c + d), a * (c + d) + b * c ≤ a * c + b * (c + d)
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd

Premises used: exists_nonneg_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw : a * c + b * c + a * d ≤ a * c + b * c + b * d
⊢ a * (c + d) + b * c ≤ a * c + b * (c + d)

Tactic:
rw [mul_add, add_right_comm, mul_add, ← add_assoc]

Premises used: add_assoc, add_right_comm, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
bc : 0 ≤ d
⊢ a * c + b * c + a * d ≤ a * c + b * c + b * d

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ 0 ≤ d

Tactic:
assumption
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
rw : b * c + a * d ≤ b * d + a * c
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]

Premises used: HMul.hMul, add_comm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
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
⊢ b * c + a * d ≤ b * d + a * c

Tactic:
mul_add_mul_le_mul_add_mul hba hdc

Premises used: mul_add_mul_le_mul_add_mul