awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : PosSMulStrictMono α β
inst_9 : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
.inr ⟨smul_le_smul_of_nonneg_left h₁ ha.le, smul_lt_smul_of_pos_left h₂ ha⟩

Premises used: LT.lt.le, And.intro, smul_lt_smul_of_pos_left, Or.inr, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : PosSMulStrictMono α β
inst_9 : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
exact .inr ⟨smul_le_smul_of_nonneg_left h₁ ha.le, smul_lt_smul_of_pos_left h₂ ha⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
simp_rw :
  ∀ ⦃b : β × γ⦄ (hb : 0.1 < b.1 ∧ 0.2 ≤ b.2 ∨ 0.1 ≤ b.1 ∧ 0.2 < b.2) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂),
    (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2
⊢ ∀ ⦃b : β × γ⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂), a₁ • b < a₂ • b

Tactic:
simp_rw [lt_iff]

Premises used: Prod.lt_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 < a.1
h₂ : 0.2 ≤ a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

Tactic:
.inl ⟨smul_lt_smul_of_pos_right hb h₁, smul_le_smul_of_nonneg_right hb.le h₂⟩

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, smul_lt_smul_of_pos_right, And.intro, Or.inl
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 < a.1
h₂ : 0.2 ≤ a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

Tactic:
exact .inl ⟨smul_lt_smul_of_pos_right hb h₁, smul_le_smul_of_nonneg_right hb.le h₂⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 ≤ a.1
h₂ : 0.2 < a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

Tactic:
.inr ⟨smul_le_smul_of_nonneg_right hb.le h₁, smul_lt_smul_of_pos_right hb h₂⟩

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, smul_lt_smul_of_pos_right, And.intro, Or.inr
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 ≤ a.1
h₂ : 0.2 < a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

Tactic:
exact .inr ⟨smul_le_smul_of_nonneg_right hb.le h₁, smul_lt_smul_of_pos_right hb h₂⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
simp_rw :
  ∀ ⦃b : β × γ⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄
    (hb : (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2),
    a₁ < a₂
⊢ ∀ ⦃b : β × γ⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b < a₂ • b), a₁ < a₂

Tactic:
simp_rw [lt_iff]

Premises used: Prod.lt_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 < (_a₂ • b).1
h₂ : (_a₁ • b).2 ≤ (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
lt_of_smul_lt_smul_right h₁ hb.1

Premises used: lt_of_smul_lt_smul_right, And.left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 < (_a₂ • b).1
h₂ : (_a₁ • b).2 ≤ (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
exact lt_of_smul_lt_smul_right h₁ hb.1

Premises used: lt_of_smul_lt_smul_right, And.left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
lt_of_smul_lt_smul_right h₂ hb.2

Premises used: lt_of_smul_lt_smul_right, And.right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
exact lt_of_smul_lt_smul_right h₂ hb.2

Premises used: lt_of_smul_lt_smul_right, And.right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : (i : ι) → Preorder (β i)
inst_3 : (i : ι) → SMul.{u_1, u_4} α (β i)
inst_4 : (i : ι) → Zero (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLE.{u_1, u_4} α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
obtain : ∀ (i : ι) (hi : 0 i < _b i), _a₁ ≤ _a₂
⊢ _a₁ ≤ _a₂

Tactic:
obtain ⟨-, i, hi⟩ := lt_def.1 hb

Premises used: Pi.lt_def, Iff.mp
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : (i : ι) → Preorder (β i)
inst_3 : (i : ι) → SMul.{u_1, u_4} α (β i)
inst_4 : (i : ι) → Zero (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLE.{u_1, u_4} α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
i : ι
hi : 0 i < _b i
⊢ _a₁ ≤ _a₂

Tactic:
le_of_smul_le_smul_right (h _) hi

Premises used: le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : (i : ι) → Preorder (β i)
inst_3 : (i : ι) → SMul.{u_1, u_4} α (β i)
inst_4 : (i : ι) → Zero (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLE.{u_1, u_4} α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
i : ι
hi : 0 i < _b i
⊢ _a₁ ≤ _a₂

Tactic:
exact le_of_smul_le_smul_right (h _) hi

Premises used: le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), PosSMulStrictMono.{u_1, u_4} α (β i)
simp_rw :
  ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : (i : ι) → β i⦄ (hb : b₁ ≤ b₂ ∧ ∃ (i : ι), b₁ i < b₂ i),
    a • b₁ ≤ a • b₂ ∧ ∃ (i : ι), (a • b₁) i < (a • b₂) i
⊢ ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : (i : ι) → β i⦄ (hb : b₁ < b₂), a • b₁ < a • b₂

Tactic:
simp_rw [lt_def]

Premises used: Pi.lt_def
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), PosSMulStrictMono.{u_1, u_4} α (β i)
_a : α
ha : 0 < _a
_b₁ _b₂ : (i : ι) → β i
hb : _b₁ ≤ _b₂
i : ι
hi : _b₁ i < _b₂ i
⊢ _a • _b₁ ≤ _a • _b₂ ∧ ∃ (i : ι), (_a • _b₁) i < (_a • _b₂) i

Tactic:
⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩

Premises used: LT.lt.le, And.intro, Exists.intro, smul_lt_smul_of_pos_left, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), PosSMulStrictMono.{u_1, u_4} α (β i)
_a : α
ha : 0 < _a
_b₁ _b₂ : (i : ι) → β i
hb : _b₁ ≤ _b₂
i : ι
hi : _b₁ i < _b₂ i
⊢ _a • _b₁ ≤ _a • _b₂ ∧ ∃ (i : ι), (_a • _b₁) i < (_a • _b₂) i

Tactic:
exact ⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosStrictMono.{u_1, u_4} α (β i)
simp_rw :
  ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b ∧ ∃ (i : ι), 0 i < b i) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂),
    a₁ • b ≤ a₂ • b ∧ ∃ (i : ι), (a₁ • b) i < (a₂ • b) i
⊢ ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂), a₁ • b < a₂ • b

Tactic:
simp_rw [lt_def]

Premises used: Pi.lt_def
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosStrictMono.{u_1, u_4} α (β i)
a : (i : ι) → β i
ha : 0 ≤ a
i : ι
hi : 0 i < a i
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ _b₁ • a ≤ _b₂ • a ∧ ∃ (i : ι), (_b₁ • a) i < (_b₂ • a) i

Tactic:
⟨smul_le_smul_of_nonneg_right hb.le ha, i, smul_lt_smul_of_pos_right hb hi⟩

Premises used: smul_le_smul_of_nonneg_right, LT.lt.le, smul_lt_smul_of_pos_right, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a_1 a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosStrictMono.{u_1, u_4} α (β i)
a : (i : ι) → β i
ha : 0 ≤ a
i : ι
hi : 0 i < a i
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ _b₁ • a ≤ _b₂ • a ∧ ∃ (i : ι), (_b₁ • a) i < (_b₂ • a) i

Tactic:
exact ⟨smul_le_smul_of_nonneg_right hb.le ha, i, smul_lt_smul_of_pos_right hb hi⟩
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLT.{u_1, u_4} α (β i)
simp_rw :
  ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b ≤ a₂ • b ∧ ∃ (i : ι), (a₁ • b) i < (a₂ • b) i), a₁ < a₂
⊢ ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b < a₂ • b), a₁ < a₂

Tactic:
simp_rw [lt_def]

Premises used: Pi.lt_def
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLT.{u_1, u_4} α (β i)
b : (i : ι) → β i
hb : 0 ≤ b
_a₁ _a₂ : α
i : ι
hi : (_a₁ • b) i < (_a₂ • b) i
⊢ _a₁ < _a₂

Tactic:
lt_of_smul_lt_smul_right hi <| hb _

Premises used: lt_of_smul_lt_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b_1 b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLT.{u_1, u_4} α (β i)
b : (i : ι) → β i
hb : 0 ≤ b
_a₁ _a₂ : α
i : ι
hi : (_a₁ • b) i < (_a₂ • b) i
⊢ _a₁ < _a₂

Tactic:
exact lt_of_smul_lt_smul_right hi <| hb _

Premises used: lt_of_smul_lt_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
hb : b₁ ≤ b₂
simp : ∀ (hf : ∀ {b₁ b₂ : β}, True) (smul : ∀ (a : α) (b : β), True) (hb : f b₁ ≤ f b₂), a • f b₁ ≤ a • f b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
simp only [← hf, smul] at *
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
smul_le_smul_of_nonneg_left hb ha

Premises used: smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
exact smul_le_smul_of_nonneg_left hb ha

Premises used: smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
hb : b₁ < b₂
simp : ∀ (smul : ∀ (a : α) (b : β), True) (hb : f b₁ < f b₂), a • f b₁ < a • f b₂
⊢ a • b₁ < a • b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Tactic:
smul_lt_smul_of_pos_left hb ha

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Tactic:
exact smul_lt_smul_of_pos_left hb ha

Premises used: smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
simpa only [smul] using hf.2 h

Premises used: Iff.mpr
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
simp : ∀ (smul : ∀ (a : α) (b : β), True) (h : a • f b₁ < a • f b₂), f b₁ < f b₂
⊢ b₁ < b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂

Tactic:
lt_of_smul_lt_smul_left h ha

Premises used: lt_of_smul_lt_smul_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero α
inst_6 : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂

Tactic:
exact lt_of_smul_lt_smul_left h ha

Premises used: lt_of_smul_lt_smul_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
ha : a₁ ≤ a₂
simp : ∀ (hf : ∀ {b₁ b₂ : β}, True) (smul : ∀ (a : α) (b : β), True) (zero : True) (hb : 0 ≤ f b), a₁ • f b ≤ a₂ • f b
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp only [← hf, zero, smul] at *
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
smul_le_smul_of_nonneg_right ha hb

Premises used: smul_le_smul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
exact smul_le_smul_of_nonneg_right ha hb

Premises used: smul_le_smul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
ha : a₁ < a₂
simp : ∀ (smul : ∀ (a : α) (b : β), True) (zero : True) (hb : 0 < f b), a₁ • f b < a₂ • f b
⊢ a₁ • b < a₂ • b

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b

Tactic:
smul_lt_smul_of_pos_right ha hb

Premises used: smul_lt_smul_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b

Tactic:
exact smul_lt_smul_of_pos_right ha hb

Premises used: smul_lt_smul_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ ∀ {b₁ b₂ : β}, True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
⊢ ∀ (a : α) (b : β), True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
⊢ True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'