awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : 0 ≤ a
⊢ b₁ < b₂

Tactic:
PosSMulReflectLT.lt_of_smul_lt_smul_left ha h

Premises used: PosSMulReflectLT.lt_of_smul_lt_smul_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : 0 < a
⊢ b₁ ≤ b₂

Tactic:
PosSMulReflectLE.le_of_smul_le_smul_left ha h

Premises used: PosSMulReflectLE.le_of_smul_le_smul_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
⊢ a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂

Tactic:
⟨fun h ↦ le_of_smul_le_smul_left h ha, fun h ↦ smul_le_smul_of_nonneg_left h ha.le⟩

Premises used: le_of_smul_le_smul_left, LT.lt.le, Iff.intro, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
⊢ a • b₁ < a • b₂ ↔ b₁ < b₂

Tactic:
⟨fun h ↦ lt_of_smul_lt_smul_left h ha.le, fun hb ↦ smul_lt_smul_of_pos_left hb ha⟩

Premises used: LT.lt.le, Iff.intro, lt_of_smul_lt_smul_left, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosMono α β
hb : 0 ≤ b
⊢ Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ x • b

Tactic:
SMulPosMono.smul_le_smul_of_nonneg_right hb

Premises used: Monotone, SMulPosMono.smul_le_smul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosStrictMono α β
hb : 0 < b
⊢ StrictMono.{u_1, u_2} (β := β) fun (x : α) ↦ x • b

Tactic:
SMulPosStrictMono.smul_lt_smul_of_pos_right hb

Premises used: StrictMono, SMulPosStrictMono.smul_lt_smul_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosMono α β
ha : a₁ ≤ a₂
hb : 0 ≤ b
⊢ a₁ • b ≤ a₂ • b

Tactic:
monotone_smul_right_of_nonneg hb ha

Premises used: monotone_smul_right_of_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : One β
inst_5 : ZeroLEOneClass β
inst_6 : SMulPosMono α β
⊢ Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1

Tactic:
fun _ _ ha ↦ smul_le_smul_of_nonneg_right ha zero_le_one

Premises used: smul_le_smul_of_nonneg_right, Monotone, zero_le_one
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosStrictMono α β
ha : a₁ < a₂
hb : 0 < b
⊢ a₁ • b < a₂ • b

Tactic:
strictMono_smul_right_of_pos hb ha

Premises used: strictMono_smul_right_of_pos
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosReflectLT α β
h : a₁ • b < a₂ • b
hb : 0 ≤ b
⊢ a₁ < a₂

Tactic:
SMulPosReflectLT.lt_of_smul_lt_smul_right hb h

Premises used: SMulPosReflectLT.lt_of_smul_lt_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosReflectLE α β
h : a₁ • b ≤ a₂ • b
hb : 0 < b
⊢ a₁ ≤ a₂

Tactic:
SMulPosReflectLE.le_of_smul_le_smul_right hb h

Premises used: SMulPosReflectLE.le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosMono α β
inst_5 : SMulPosReflectLE α β
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b ↔ a₁ ≤ a₂

Tactic:
⟨fun h ↦ le_of_smul_le_smul_right h hb, fun ha ↦ smul_le_smul_of_nonneg_right ha hb.le⟩

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, le_of_smul_le_smul_right, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero β
inst_4 : SMulPosStrictMono α β
inst_5 : SMulPosReflectLT α β
hb : 0 < b
⊢ a₁ • b < a₂ • b ↔ a₁ < a₂

Tactic:
⟨fun h ↦ lt_of_smul_lt_smul_right h hb.le, fun ha ↦ smul_lt_smul_of_pos_right ha hb⟩

Premises used: lt_of_smul_lt_smul_right, LT.lt.le, smul_lt_smul_of_pos_right, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosMono α β
ha : a₁ ≤ a₂
hb : b₁ < b₂
h₁ : 0 < a₁
h₂ : 0 ≤ b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_lt_smul_of_pos_left hb h₁).trans_le (smul_le_smul_of_nonneg_right ha h₂)

Premises used: smul_le_smul_of_nonneg_right, LT.lt.trans_le, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosMono α β
ha : a₁ ≤ a₂
hb : b₁ < b₂
h₂ : 0 < a₂
h₁ : 0 ≤ b₁
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_le_smul_of_nonneg_right ha h₁).trans_lt (smul_lt_smul_of_pos_left hb h₂)

Premises used: smul_le_smul_of_nonneg_right, smul_lt_smul_of_pos_left, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ < a₂
hb : b₁ ≤ b₂
h₁ : 0 ≤ a₁
h₂ : 0 < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_le_smul_of_nonneg_left hb h₁).trans_lt (smul_lt_smul_of_pos_right ha h₂)

Premises used: smul_lt_smul_of_pos_right, LE.le.trans_lt, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ < a₂
hb : b₁ ≤ b₂
h₂ : 0 ≤ a₂
h₁ : 0 < b₁
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_lt_smul_of_pos_right ha h₁).trans_le (smul_le_smul_of_nonneg_left hb h₂)

Premises used: smul_lt_smul_of_pos_right, LT.lt.trans_le, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ < a₂
hb : b₁ < b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_lt_smul_of_pos_left hb h₁).trans (smul_lt_smul_of_pos_right ha h₂)

Premises used: smul_lt_smul_of_pos_right, LT.lt.trans, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ < a₂
hb : b₁ < b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
(smul_lt_smul_of_pos_right ha h₁).trans (smul_lt_smul_of_pos_left hb h₂)

Premises used: smul_lt_smul_of_pos_right, LT.lt.trans, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 ≤ a₁
h₂ : 0 ≤ b₂
⊢ a₁ • b₁ ≤ a₂ • b₂

Tactic:
(smul_le_smul_of_nonneg_left hb h₁).trans (smul_le_smul_of_nonneg_right ha h₂)

Premises used: smul_le_smul_of_nonneg_right, LE.le.trans, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : SMul α β
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Zero α
inst_4 : Zero β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 ≤ a₂
h₁ : 0 ≤ b₁
⊢ a₁ • b₁ ≤ a₂ • b₂

Tactic:
(smul_le_smul_of_nonneg_right ha h₁).trans (smul_le_smul_of_nonneg_left hb h₂)

Premises used: smul_le_smul_of_nonneg_right, LE.le.trans, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : PartialOrder β
inst_3 : Zero β
inst_4 : One β
inst_5 : ZeroLEOneClass β
inst_6 : NeZero.{u_2} (R := β) 1
inst_7 : SMulPosStrictMono α β
⊢ StrictMono.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1

Tactic:
fun _ _ ha ↦ smul_lt_smul_of_pos_right ha (zero_lt_one (α := β))

Premises used: StrictMono, smul_lt_smul_of_pos_right, zero_lt_one
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : LinearOrder β
inst_3 : Zero α
⊢ PosSMulStrictMono α β ↔ PosSMulReflectLE α β

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ PosSMulReflectLE.toPosSMulStrictMono⟩

Premises used: inferInstance, Iff.intro, PosSMulReflectLE.toPosSMulStrictMono
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : Preorder α
inst_2 : LinearOrder β
inst_3 : Zero α
⊢ PosSMulMono α β ↔ PosSMulReflectLT α β

Tactic:
⟨fun _ ↦ PosSMulMono.toPosSMulReflectLT, fun _ ↦ PosSMulReflectLT.toPosSMulMono⟩

Premises used: PosSMulReflectLT.toPosSMulMono, Iff.intro, PosSMulMono.toPosSMulReflectLT
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
inst : SMul α β
inst_1 : Preorder α
inst_2 : LinearOrder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
ha : 0 ≤ a
b₁ b₂ : β
⊢ a • max b₁ b₂ = max (a • b₁) (a • b₂)

Tactic:
(monotone_smul_left_of_nonneg ha).map_max

Premises used: monotone_smul_left_of_nonneg, Monotone.map_max
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
inst : SMul α β
inst_1 : Preorder α
inst_2 : LinearOrder β
inst_3 : Zero α
inst_4 : PosSMulMono α β
ha : 0 ≤ a
b₁ b₂ : β
⊢ a • min b₁ b₂ = min (a • b₁) (a • b₂)

Tactic:
(monotone_smul_left_of_nonneg ha).map_min

Premises used: monotone_smul_left_of_nonneg, Monotone.map_min
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : LinearOrder α
inst_2 : LinearOrder β
inst_3 : Zero β
⊢ SMulPosStrictMono α β ↔ SMulPosReflectLE α β

Tactic:
⟨fun _ ↦ SMulPosStrictMono.toSMulPosReflectLE, fun _ ↦ SMulPosReflectLE.toSMulPosStrictMono⟩

Premises used: Iff.intro, SMulPosStrictMono.toSMulPosReflectLE, SMulPosReflectLE.toSMulPosStrictMono
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
inst_1 : LinearOrder α
inst_2 : LinearOrder β
inst_3 : Zero β
⊢ SMulPosMono α β ↔ SMulPosReflectLT α β

Tactic:
⟨fun _ ↦ SMulPosMono.toSMulPosReflectLT, fun _ ↦ SMulPosReflectLT.toSMulPosMono⟩

Premises used: SMulPosMono.toSMulPosReflectLT, SMulPosReflectLT.toSMulPosMono, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

Premises used: smul_zero, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulStrictMono α β
ha : 0 < a
hb : b < 0
⊢ a • b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

Premises used: smul_zero, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulStrictMono α β
inst_6 : PosSMulReflectLT α β
ha : 0 < a
⊢ 0 < a • b ↔ 0 < b

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)

Premises used: smul_zero, smul_lt_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulStrictMono α β
inst_6 : PosSMulReflectLT α β
ha : 0 < a
⊢ a • b < 0 ↔ b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β))

Premises used: smul_zero, smul_lt_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Premises used: smul_zero, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
ha : 0 ≤ a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Premises used: smul_zero, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
rwa rwa₁ rwa₂ rwa₃ : 0 < a • b
⊢ HSMul.hSMul (β := β) a 0 < a • b

Tactic:
rwa [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
rwa rwa₁ rwa₂ rwa₃ : a • b < 0
⊢ a • b < HSMul.hSMul (β := β) a 0

Tactic:
rwa [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulReflectLE α β
h : 0 ≤ a • b
ha : 0 < a
⊢ HSMul.hSMul (β := β) a 0 ≤ a • b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulReflectLE α β
h : a • b ≤ 0
ha : 0 < a
⊢ a • b ≤ HSMul.hSMul (β := β) a 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
ha : 0 < a
⊢ 0 ≤ a • b ↔ 0 ≤ b

Tactic:
⟨(nonneg_of_smul_nonneg_of_pos_left · ha), smul_nonneg ha.le⟩

Premises used: smul_nonneg, nonneg_of_smul_nonneg_of_pos_left, LT.lt.le, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
inst_6 : PosSMulReflectLE α β
ha : 0 < a
⊢ a • b ≤ 0 ↔ b ≤ 0

Tactic:
⟨(nonpos_of_smul_nonpos_of_pos_left · ha), smul_nonpos_of_nonneg_of_nonpos ha.le⟩

Premises used: nonpos_of_smul_nonpos_of_pos_left, LT.lt.le, Iff.intro, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb

Premises used: smul_lt_smul_of_pos_right, zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
ha : a < 0
hb : 0 < b
⊢ a • b < 0

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb

Premises used: smul_lt_smul_of_pos_right, zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
inst_6 : SMulPosReflectLT α β
hb : 0 < b
⊢ 0 < a • b ↔ 0 < a

Tactic:
simpa only [zero_smul] using smul_lt_smul_iff_of_pos_right hb (a₁ := 0) (a₂ := a)

Premises used: smul_lt_smul_iff_of_pos_right, zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

Premises used: smul_le_smul_of_nonneg_right, zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
ha : a ≤ 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

Premises used: smul_le_smul_of_nonneg_right, zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
rwa rwa₁ rwa₂ rwa₃ : 0 < a • b
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b < a • b

Tactic:
rwa [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
rwa rwa₁ rwa₂ rwa₃ : a • b < 0
⊢ a • b < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b

Tactic:
rwa [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulReflectLT α β
inst_6 : SMulPosReflectLT α β
hab : 0 < a • b
⊢ 0 < a ↔ 0 < b

Tactic:
⟨pos_of_smul_pos_left hab ∘ le_of_lt, pos_of_smul_pos_right hab ∘ le_of_lt⟩

Premises used: le_of_lt, Function.comp, pos_of_smul_pos_left, Iff.intro, pos_of_smul_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosReflectLE α β
h : 0 ≤ a • b
hb : 0 < b
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b ≤ a • b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosReflectLE α β
h : a • b ≤ 0
hb : 0 < b
⊢ a • b ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
inst_6 : SMulPosReflectLE α β
hb : 0 < b
⊢ 0 ≤ a • b ↔ 0 ≤ a

Tactic:
⟨(nonneg_of_smul_nonneg_of_pos_right · hb), (smul_nonneg' · hb.le)⟩

Premises used: smul_nonneg', LT.lt.le, Iff.intro, nonneg_of_smul_nonneg_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
inst_6 : SMulPosReflectLE α β
hb : 0 < b
⊢ a • b ≤ 0 ↔ a ≤ 0

Tactic:
⟨(nonpos_of_smul_nonpos_of_pos_right · hb), (smul_nonpos_of_nonpos_of_nonneg · hb.le)⟩

Premises used: smul_nonpos_of_nonpos_of_nonneg, nonpos_of_smul_nonpos_of_pos_right, LT.lt.le, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : MulOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
inst_8 : IsScalarTower α β β
h : Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1
x : α
ha : 0 ≤ x
x_1 x_2 : β
hb : x_1 ≤ x_2
⊢ 0 ≤ HSMul.hSMul (β := β) x 1

Tactic:
simpa using h ha
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : MulOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
inst_8 : IsScalarTower α β β
h : Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1
x : α
ha : 0 ≤ x
x_1 x_2 : β
hb : x_1 ≤ x_2
⊢ HSMul.hSMul (β := β) x 1 * x_1 ≤ HSMul.hSMul (β := β) x 1 * x_2

Tactic:
have := mul_le_mul_of_nonneg_left hb (by simpa using h ha)
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : MulOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
inst_8 : IsScalarTower α β β
h : Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1
x : α
ha : 0 ≤ x
x_1 x_2 : β
hb : x_1 ≤ x_2
this : HSMul.hSMul (β := β) x 1 * x_1 ≤ HSMul.hSMul (β := β) x 1 * x_2
⊢ x • x_1 ≤ x • x_2

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : MulOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
inst_8 : IsScalarTower α β β
h : Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1
x : β
ha : 0 ≤ x
x_1 x_2 : α
hb : x_1 ≤ x_2
⊢ x_1 • x ≤ x_2 • x

Tactic:
simpa using mul_le_mul_of_nonneg_right (h hb) ha

Premises used: mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
inl : ∀ (ha : 0 = a), a • b₁ ≤ a • b₂
inr : ∀ (ha : 0 < a), a • b₁ ≤ a • b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
obtain ha | ha := ha.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 = a
⊢ a • b₁ ≤ a • b₂

Tactic:
simp [← ha]
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Tactic:
h₀ _ ha _ _ h
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Tactic:
exact h₀ _ ha _ _ h