awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
inl : ∀ (ha : 0 = a), b₁ < b₂
inr : ∀ (ha : 0 < a), b₁ < b₂
⊢ b₁ < 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₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

Tactic:
simp [← ha] at 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₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < 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₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha_1 : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂

Tactic:
exact 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 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
inl : ∀ (hb : 0 = b), a₁ • b ≤ a₂ • b
inr : ∀ (hb : 0 < b), a₁ • b ≤ a₂ • b
⊢ a₁ • b ≤ a₂ • b

Tactic:
obtain hb | hb := hb.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 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp [← hb]
-- 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 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Tactic:
h₀ _ hb _ _ h
-- 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 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Tactic:
exact h₀ _ hb _ _ h
-- 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 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
inl : ∀ (hb : 0 = b), a₁ < a₂
inr : ∀ (hb : 0 < b), a₁ < a₂
⊢ a₁ < a₂

Tactic:
obtain hb | hb := hb.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 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 = b
⊢ a₁ < a₂

Tactic:
simp [← hb] at h
-- 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 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂

Tactic:
h₀ _ hb _ _ h
-- 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 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb_1 : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂

Tactic:
exact h₀ _ hb _ _ h
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
⊢ PosSMulMono α β

Tactic:
PosSMulMono.of_pos fun _a ha ↦ (strictMono_smul_left_of_pos ha).monotone

Premises used: StrictMono.monotone, PosSMulMono.of_pos, strictMono_smul_left_of_pos
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : SMulPosStrictMono α β
⊢ SMulPosMono α β

Tactic:
SMulPosMono.of_pos fun _b hb ↦ (strictMono_smul_right_of_pos hb).monotone

Premises used: StrictMono.monotone, SMulPosMono.of_pos, strictMono_smul_right_of_pos
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a_1 a₁ a₂ : α
b b₁_1 b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ : β
h : a • b₁ < a • b₁
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂ : α
b_1 b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ : α
h : a₁ • b < a₁ • b
⊢ False

Tactic:
simp at h
-- 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 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
h₁ : 0 < a₁
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
h₂ : 0 < b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
refine : ∀ (h : a₁ • b₁ = a₂ • b₂), a₁ = a₂ ∧ b₁ = b₂
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [eq_iff_le_not_lt, ha, hb, true_and]

Premises used: eq_iff_le_not_lt, true_and
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩

Premises used: And.intro, Eq.not_lt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
refine_2 : ∀ (hb : b₁ < b₂), a₁ • b₁ < a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb_1 : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb_1 : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, LT.lt.trans_le, 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 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
h₁ : 0 < b₁
ha : a₁ ≤ a₁
h₂ : 0 < a₁
hb : b₁ ≤ b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
refine : ∀ (h : a₁ • b₁ = a₂ • b₂), a₁ = a₂ ∧ b₁ = b₂
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [eq_iff_le_not_lt, ha, hb, true_and]

Premises used: eq_iff_le_not_lt, true_and
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩

Premises used: And.intro, Eq.not_lt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
refine_2 : ∀ (hb : b₁ < b₂), a₁ • b₁ < a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb_1 : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, 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 : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb_1 : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

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

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, smul_lt_smul_of_pos_left, LE.le.trans_lt
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
inr :
  ∀ (hab : 0 < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b),
    LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
inr₁ : ∀ (ha : 0 < a), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
obtain ha | rfl | ha := lt_trichotomy a 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Premises used: And.intro, lt_imp_lt_of_le_imp_le, Or.inr
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
inl : ∀ (hb : 0 ≤ b), a • b ≤ 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Premises used: Or.inr
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
smul_nonpos_of_nonpos_of_nonneg ha.le hb

Premises used: smul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
exact smul_nonpos_of_nonpos_of_nonneg ha.le hb

Premises used: smul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b
⊢ LT.lt.{u_2} (α := β) 0 0

Tactic:
rw [zero_smul] at hab

Premises used: zero_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : LT.lt.{u_2} (α := β) 0 0
⊢ LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0

Tactic:
hab.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : LT.lt.{u_2} (α := β) 0 0
⊢ LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0

Tactic:
exact hab.false.elim

Premises used: False.elim, LT.lt.false
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Premises used: And.intro, Or.inl, lt_imp_lt_of_le_imp_le
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
inr : ∀ (hb : b ≤ 0), a • b ≤ 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Premises used: Or.inl
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
smul_nonpos_of_nonneg_of_nonpos ha.le hb

Premises used: LT.lt.le, 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

Premises used: LT.lt.le, 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
h : 0 < a • b
ha : a ≤ 0
⊢ b < 0

Tactic:
((pos_and_pos_or_neg_and_neg_of_smul_pos h).resolve_left fun h ↦ h.1.not_ge ha).2

Premises used: Or.resolve_left, And.right, And.left, LT.lt.not_ge, pos_and_pos_or_neg_and_neg_of_smul_pos
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
h : 0 < a • b
ha : b ≤ 0
⊢ a < 0

Tactic:
((pos_and_pos_or_neg_and_neg_of_smul_pos h).resolve_left fun h ↦ h.2.not_ge ha).1

Premises used: Or.resolve_left, And.right, And.left, LT.lt.not_ge, pos_and_pos_or_neg_and_neg_of_smul_pos
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
⊢ a < 0 ↔ b < 0

Tactic:
⟨neg_of_smul_pos_right hab ∘ le_of_lt, neg_of_smul_pos_left hab ∘ le_of_lt⟩

Premises used: le_of_lt, Function.comp, Iff.intro, neg_of_smul_pos_left, neg_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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : SMulPosMono α β
h : a • b < 0
ha : 0 ≤ a
⊢ b < 0

Tactic:
lt_of_not_ge fun hb ↦ (smul_nonneg' ha hb).not_gt h

Premises used: lt_of_not_ge, smul_nonneg', LE.le.not_gt
-- 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 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
h : a • b < 0
hb : 0 ≤ b
⊢ a < 0

Tactic:
lt_of_not_ge fun ha ↦ (smul_nonneg ha hb).not_gt h

Premises used: smul_nonneg, lt_of_not_ge, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
inst_6 : SMulPosReflectLE α β
hb : 0 < b
rw rw₁ : b ≤ a • b ↔ b ≤ a • b
⊢ b ≤ a • b ↔ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b ≤ a • b

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
inst_6 : SMulPosReflectLT α β
hb : 0 < b
rw rw₁ : b < a • b ↔ b < a • b
⊢ b < a • b ↔ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b < a • b

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
inst_6 : SMulPosReflectLE α β
hb : 0 < b
rw rw₁ : a • b ≤ b ↔ a • b ≤ b
⊢ a • b ≤ b ↔ a • b ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
inst_6 : SMulPosReflectLT α β
hb : 0 < b
rw rw₁ : a • b < b ↔ a • b < b
⊢ a • b < b ↔ a • b < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
hb : 0 ≤ b
h : a ≤ 1
⊢ a • b ≤ b

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

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

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

Premises used: smul_le_smul_of_nonneg_right, one_smul