awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact mul_add_mul_le_mul_add_mul hba hdc

Premises used: mul_add_mul_le_mul_add_mul
-- 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 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono 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_pos_add_of_lt' hcd

Premises used: exists_pos_add_of_lt', 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 : 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
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 : 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
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 : 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
⊢ 0 < d

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

Tactic:
exact hd
-- 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 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono 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 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c

Tactic:
mul_add_mul_lt_mul_add_mul hba hdc

Premises used: mul_add_mul_lt_mul_add_mul
-- 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 : AddLeftReflectLT R
inst_3 : ExistsAddOfLE R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c

Tactic:
exact mul_add_mul_lt_mul_add_mul hba hdc

Premises used: mul_add_mul_lt_mul_add_mul
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
Decidable.or_iff_not_not_and_not.2 ?_

Premises used: Iff.mpr, Decidable.or_iff_not_not_and_not
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
refine : ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
refine Decidable.or_iff_not_not_and_not.2 ?_

Premises used: Iff.mpr, Decidable.or_iff_not_not_and_not
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
simp : (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))

Tactic:
simp only [not_and, not_le]

Premises used: not_le, not_and
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
apply : a * b < 0
⊢ False

Tactic:
apply not_lt_of_ge hab _

Premises used: not_lt_of_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a * b < 0
inr : ∀ (hab : 0 ≤ 0 * b) (ab : LE.le.{u} (α := R) 0 0 → b < 0) (nab : LE.le.{u} (α := R) 0 0 → 0 < b), 0 * b < 0
inr₁ : ∀ (ha : a < 0), a * b < 0
⊢ a * b < 0

Tactic:
rcases lt_trichotomy 0 a with (ha | rfl | ha)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

Tactic:
mul_neg_of_pos_of_neg ha (ab ha.le)

Premises used: LT.lt.le, mul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0

Tactic:
exact mul_neg_of_pos_of_neg ha (ab ha.le)

Premises used: LT.lt.le, mul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : LE.le.{u} (α := R) 0 0 → b < 0
nab : LE.le.{u} (α := R) 0 0 → 0 < b
⊢ 0 * b < 0

Tactic:
((ab le_rfl).asymm (nab le_rfl)).elim

Premises used: le_rfl, False.elim, LT.lt.asymm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ 0 * b
ab : LE.le.{u} (α := R) 0 0 → b < 0
nab : LE.le.{u} (α := R) 0 0 → 0 < b
⊢ 0 * b < 0

Tactic:
exact ((ab le_rfl).asymm (nab le_rfl)).elim

Premises used: le_rfl, False.elim, LT.lt.asymm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
mul_neg_of_neg_of_pos ha (nab ha.le)

Premises used: mul_neg_of_neg_of_pos, LT.lt.le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0

Tactic:
exact mul_neg_of_neg_of_pos ha (nab ha.le)

Premises used: mul_neg_of_neg_of_pos, LT.lt.le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
h : 0 ≤ a * b
hb : 0 < b
⊢ 0 ≤ a

Tactic:
le_of_not_gt fun ha => (mul_neg_of_neg_of_pos ha hb).not_ge h

Premises used: mul_neg_of_neg_of_pos, le_of_not_gt, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : 0 ≤ a * b
ha : 0 < a
⊢ 0 ≤ b

Tactic:
le_of_not_gt fun hb => (mul_neg_of_pos_of_neg ha hb).not_ge h

Premises used: le_of_not_gt, LT.lt.not_ge, mul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : a * b ≤ 0
hb : 0 < b
⊢ a ≤ 0

Tactic:
le_of_not_gt fun ha : a > 0 => (mul_pos ha hb).not_ge h

Premises used: le_of_not_gt, mul_pos, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : a * b ≤ 0
ha : 0 < a
⊢ b ≤ 0

Tactic:
le_of_not_gt fun hb : b > 0 => (mul_pos ha hb).not_ge h

Premises used: le_of_not_gt, mul_pos, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b c : R
inst_2 : PosMulStrictMono R
h : 0 < c
⊢ c * 0 ≤ c * b ↔ 0 ≤ b

Tactic:
mul_le_mul_iff_right₀ h

Premises used: mul_le_mul_iff_right₀
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b c : R
inst_2 : PosMulStrictMono R
h : 0 < c
h₁ : 0 = c * 0
⊢ 0 ≤ c * b ↔ 0 ≤ b

Tactic:
convert! mul_le_mul_iff_right₀ h

Premises used: mul_le_mul_iff_right₀
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b c : R
inst_2 : PosMulStrictMono R
h : 0 < c
⊢ 0 = c * 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
b c : R
inst_2 : MulPosStrictMono R
h : 0 < c
⊢ 0 ≤ b * c ↔ 0 ≤ b

Tactic:
simpa using (mul_le_mul_iff_left₀ h : 0 * c ≤ b * c ↔ 0 ≤ b)

Premises used: mul_le_mul_iff_left₀
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
a2 : 2 ≤ a
ab : a ≤ b
this : 0 < b
⊢ a + b ≤ b + b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : AddLeftMono R
inst_5 : PosMulStrictMono R
b2 : 2 ≤ b
ba : b ≤ a
this : 0 < a
⊢ a + b ≤ a + a

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : MulPosStrictMono R
inst_5 : PosMulStrictMono R
inst_6 : AddLeftMono R
a2 : 2 ≤ a
b2 : 2 ≤ b
⊢ a + b ≤ a * b

Tactic:
if hab : a ≤ b then add_le_mul_of_left_le_right a2 hab
  else add_le_mul_of_right_le_left b2 (le_of_not_ge hab)

Premises used: le_of_not_ge, dite, add_le_mul_of_right_le_left, add_le_mul_of_left_le_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : MulPosStrictMono R
inst_5 : PosMulStrictMono R
inst_6 : AddLeftMono R
a2 : 2 ≤ a
b2 : 2 ≤ b
⊢ a + b ≤ b * a

Tactic:
(le_of_eq (add_comm _ _)).trans (add_le_mul b2 a2)

Premises used: add_comm, add_le_mul, LE.le.trans, le_of_eq
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
ha : 0 < a
⊢ 0 ≤ a * b ↔ 0 ≤ b

Tactic:
⟨fun h => nonneg_of_mul_nonneg_right h ha, mul_nonneg ha.le⟩

Premises used: mul_nonneg, nonneg_of_mul_nonneg_right, LT.lt.le, Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
inst_3 : MulPosStrictMono R
hb : 0 < b
⊢ 0 ≤ a * b ↔ 0 ≤ a

Tactic:
⟨fun h => nonneg_of_mul_nonneg_left h hb, fun h => mul_nonneg h hb.le⟩

Premises used: mul_nonneg, LT.lt.le, nonneg_of_mul_nonneg_left, Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : 0 ≤ a * b
hb : b < 0
⊢ a ≤ 0

Tactic:
le_of_not_gt fun ha => absurd h (mul_neg_of_pos_of_neg ha hb).not_ge

Premises used: le_of_not_gt, absurd, LT.lt.not_ge, mul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
h : 0 ≤ a * b
ha : a < 0
⊢ b ≤ 0

Tactic:
le_of_not_gt fun hb => absurd h (mul_neg_of_neg_of_pos ha hb).not_ge

Premises used: mul_neg_of_neg_of_pos, le_of_not_gt, absurd, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : PosMulStrictMono R
u : Rˣ
⊢ 0 < (↑u⁻¹ : R) ↔ 0 < (↑u : R)

Tactic:
have : ∀ {u : Rˣ}, (0 : R) < u → (0 : R) < ↑u⁻¹ := @fun u h =>
    (mul_pos_iff_of_pos_left h).mp <| u.mul_inv.symm ▸ zero_lt_one
  ⟨this, this⟩

Premises used: Eq.rec, Units.mul_inv, zero_lt_one, mul_pos_iff_of_pos_left, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : MulPosMono R
inst_5 : PosMulMono R
u : Rˣ
⊢ (↑u⁻¹ : R) < 0 ↔ (↑u : R) < 0

Tactic:
have : ∀ {u : Rˣ}, ↑u < (0 : R) → ↑u⁻¹ < (0 : R) := @fun u h =>
    neg_of_mul_pos_right (u.mul_inv.symm ▸ zero_lt_one) h.le
  ⟨this, this⟩

Premises used: neg_of_mul_pos_right, LT.lt.le, Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a : R
inst_2 : PosMulStrictMono R
ha : 0 < a
b c : R
⊢ cmp (a * b) (a * c) = cmp b c

Tactic:
(strictMono_mul_left_of_pos ha).cmp_map_eq b c

Premises used: strictMono_mul_left_of_pos, StrictMono.cmp_map_eq
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a : R
inst_2 : MulPosStrictMono R
ha : 0 < a
b c : R
⊢ cmp (b * a) (c * a) = cmp b c

Tactic:
(strictMono_mul_right_of_pos ha).cmp_map_eq b c

Premises used: strictMono_mul_right_of_pos, StrictMono.cmp_map_eq
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a : R
inst_2 : PosMulMono R
b c : R
ha : 0 ≤ a
⊢ a * max b c = max (a * b) (a * c)

Tactic:
(monotone_mul_left_of_nonneg ha).map_max

Premises used: Monotone.map_max, monotone_mul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a : R
inst_2 : PosMulMono R
b c : R
ha : 0 ≤ a
⊢ a * min b c = min (a * b) (a * c)

Tactic:
(monotone_mul_left_of_nonneg ha).map_min

Premises used: Monotone.map_min, monotone_mul_left_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
c : R
inst_2 : MulPosMono R
a b : R
hc : 0 ≤ c
⊢ max a b * c = max (a * c) (b * c)

Tactic:
(monotone_mul_right_of_nonneg hc).map_max

Premises used: monotone_mul_right_of_nonneg, Monotone.map_max
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
c : R
inst_2 : MulPosMono R
a b : R
hc : 0 ≤ c
⊢ min a b * c = min (a * c) (b * c)

Tactic:
(monotone_mul_right_of_nonneg hc).map_min

Premises used: monotone_mul_right_of_nonneg, Monotone.map_min
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u} (R := R) 1
inst_4 : MulPosStrictMono R
inst_5 : PosMulMono R
a b c : R
h : a * c ≤ b
hb : 0 ≤ b
hc : 1 ≤ c
⊢ a ≤ b

Tactic:
le_of_mul_le_mul_right (h.trans <| le_mul_of_one_le_right hb hc) <| zero_lt_one.trans_le hc

Premises used: le_of_mul_le_mul_right, zero_lt_one, LT.lt.trans_le, le_mul_of_one_le_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : PosMulStrictMono R
inst_3 : MulPosMono R
a b : R
hb : 0 ≤ b
h : a * a ≤ b * b
⊢ a ≤ b

Tactic:
le_of_not_gt fun hab => (mul_self_lt_mul_self hb hab).not_ge h

Premises used: le_of_not_gt, mul_self_lt_mul_self, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : PosMulStrictMono R
inst_3 : MulPosMono R
a b : R
h1 : 0 ≤ a
h2 : 0 ≤ b
⊢ a ≤ b ↔ a * a ≤ b * b

Tactic:
⟨mul_self_le_mul_self h1, nonneg_le_nonneg_of_sq_le_sq h2⟩

Premises used: mul_self_le_mul_self, nonneg_le_nonneg_of_sq_le_sq, Iff.intro
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : PosMulStrictMono R
inst_3 : MulPosMono R
a b : R
h1 : 0 ≤ a
h2 : 0 ≤ b
⊢ a < b ↔ a * a < b * b

Tactic:
((@strictMonoOn_mul_self R _).lt_iff_lt h1 h2).symm

Premises used: strictMonoOn_mul_self, Iff.symm, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : PosMulStrictMono R
inst_3 : MulPosMono R
a b : R
h1 : 0 ≤ a
h2 : 0 ≤ b
⊢ a * a = b * b ↔ a = b

Tactic:
(@strictMonoOn_mul_self R _).eq_iff_eq h1 h2

Premises used: StrictMonoOn.eq_iff_eq, strictMonoOn_mul_self
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ 0 ≤ a

Tactic:
simpa only [pow_zero, mul_one] using h 0

Premises used: pow_zero, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
⊢ 0 ≤ a

Tactic:
have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩

Premises used: nonneg_of_mul_nonneg_right, And.intro, LE.le.eq_or_lt', Or.imp_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
refine : ∀ (ha : 0 < a), 0 ≤ a * b
⊢ a = 0 ∨ 0 < a ∧ 0 ≤ b

Tactic:
refine this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩

Premises used: LE.le.eq_or_lt', Or.imp_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : PosMulStrictMono R
h : ∀ (n : ℕ), 0 ≤ a * b ^ n
this : 0 ≤ a
ha : 0 < a
⊢ 0 ≤ a * b

Tactic:
simpa only [pow_one] using h 1

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftStrictMono R
inst_6 : AddLeftReflectLT R
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
⟨pos_and_pos_or_neg_and_neg_of_mul_pos, fun h =>
    h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩

Premises used: Iff.mpr, and_imp, pos_and_pos_or_neg_and_neg_of_mul_pos, mul_pos, Iff.intro, Or.elim, mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftReflectLE R
inst_6 : AddLeftMono R
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg, fun h =>
    h.elim (and_imp.2 mul_nonneg) (and_imp.2 mul_nonneg_of_nonpos_of_nonpos)⟩

Premises used: Iff.mpr, mul_nonneg, and_imp, nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg, mul_nonneg_of_nonpos_of_nonpos, Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Premises used: mul_nonneg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Premises used: mul_nonneg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
rw : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Premises used: mul_nonneg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
iterate : (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
iterate 3 rw [mul_nonneg_iff]

Premises used: mul_nonneg_iff
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a ∨ a ≤ 0

Tactic:
have or_a := le_total 0 a
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
⊢ 0 ≤ b ∨ b ≤ 0

Tactic:
have or_b := le_total 0 b
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ 0 ≤ c ∨ c ≤ 0

Tactic:
have or_c := le_total 0 c
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosStrictMono R
inst_4 : PosMulStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
a b c : R
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
⊢ 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
mul_nonneg_iff.trans ?_

Premises used: mul_nonneg_iff, Iff.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
a b : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulStrictMono R
inst_4 : MulPosStrictMono R
inst_5 : AddLeftMono R
inst_6 : AddLeftReflectLE R
refine : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
⊢ 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
refine mul_nonneg_iff.trans ?_

Premises used: mul_nonneg_iff, Iff.trans