awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α β
hb : 0 < b
h : a < 1
⊢ a • b < b

Tactic:
simpa only [one_smul] using smul_lt_smul_of_pos_right h hb

Premises used: smul_lt_smul_of_pos_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 : SMulPosStrictMono α β
hb : 0 < b
h : 1 < a
⊢ b < a • b

Tactic:
simpa only [one_smul] using smul_lt_smul_of_pos_right h hb

Premises used: smul_lt_smul_of_pos_right, one_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_a : α
ha : 0 ≤ _a
b₁ b₂ : β
⊢ ∀ (hb : b₁ ≤ b₂), _a • b₁ ≤ _a • b₂

Tactic:
simpa [sub_nonneg, smul_sub] using h _ ha (b₂ - b₁)

Premises used: HSub.hSub, smul_sub, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
inst_5 : Preorder α
inst_6 : PartialOrder β
inst_7 : PosSMulMono α β
⊢ PosSMulStrictMono α β

Tactic:
⟨fun _a ha _b₁ _b₂ hb ↦ (smul_le_smul_of_nonneg_left hb.le ha.le).lt_of_ne <|
    (smul_right_injective _ ha.ne').ne hb.ne⟩

Premises used: Function.Injective.ne, LT.lt.le, smul_right_injective, LE.le.lt_of_ne, LT.lt.ne', PosSMulStrictMono.mk, LT.lt.ne, 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₂ : β
inst : Semiring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
inst_5 : Preorder α
inst_6 : PartialOrder β
inst_7 : PosSMulReflectLT α β
⊢ PosSMulReflectLE α β

Tactic:
⟨fun _a ha _b₁ _b₂ h ↦ h.eq_or_lt.elim
    (fun h ↦ (smul_right_injective _ ha.ne' h).le) fun h' ↦
    (lt_of_smul_lt_smul_left h' ha.le).le⟩

Premises used: LE.le.eq_or_lt, LT.lt.le, Eq.le, smul_right_injective, LT.lt.ne', lt_of_smul_lt_smul_left, Or.elim, PosSMulReflectLE.mk
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
inst_5 : PartialOrder α
inst_6 : PartialOrder β
⊢ PosSMulMono α β ↔ PosSMulStrictMono α β

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

Premises used: inferInstance, PosSMulMono.toPosSMulStrictMono, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
inst_5 : PartialOrder α
inst_6 : PartialOrder β
⊢ PosSMulReflectLE α β ↔ PosSMulReflectLT α β

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ PosSMulReflectLT.toPosSMulReflectLE⟩

Premises used: inferInstance, PosSMulReflectLT.toPosSMulReflectLE, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid α
inst_6 : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
⊢ ∀ (ha : a₁ ≤ a₂), a₁ • _b ≤ a₂ • _b

Tactic:
simpa [sub_nonneg, sub_smul] using (h (a₂ - a₁) · _ hb)

Premises used: HSub.hSub, sub_smul, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsDomain α
inst_6 : Module.IsTorsionFree α β
inst_7 : SMulPosMono α β
⊢ SMulPosStrictMono α β

Tactic:
⟨fun _b hb _a₁ _a₂ ha ↦ (smul_le_smul_of_nonneg_right ha.le hb.le).lt_of_ne <|
    (smul_left_injective _ hb.ne').ne ha.ne⟩

Premises used: smul_le_smul_of_nonneg_right, Function.Injective.ne, LT.lt.le, smul_left_injective, LE.le.lt_of_ne, LT.lt.ne', SMulPosStrictMono.mk, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsDomain α
inst_6 : Module.IsTorsionFree α β
⊢ SMulPosMono α β ↔ SMulPosStrictMono α β

Tactic:
⟨fun _ ↦ SMulPosMono.toSMulPosStrictMono, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, SMulPosMono.toSMulPosStrictMono
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsDomain α
inst_6 : Module.IsTorsionFree α β
inst_7 : SMulPosReflectLT α β
⊢ SMulPosReflectLE α β

Tactic:
⟨fun _b hb _a₁ _a₂ h ↦ h.eq_or_lt.elim (fun h ↦ (smul_left_injective _ hb.ne' h).le) fun h' ↦
    (lt_of_smul_lt_smul_right h' hb.le).le⟩

Premises used: LE.le.eq_or_lt, SMulPosReflectLE.mk, lt_of_smul_lt_smul_right, LT.lt.le, Eq.le, smul_left_injective, LT.lt.ne', Or.elim
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : IsDomain α
inst_6 : Module.IsTorsionFree α β
⊢ SMulPosReflectLE α β ↔ SMulPosReflectLT α β

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ SMulPosReflectLT.toSMulPosReflectLE⟩

Premises used: inferInstance, SMulPosReflectLT.toSMulPosReflectLE, Iff.intro
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
rw : a • a⁻¹ • b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
rw₁ rw₂ : b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Premises used: smul_le_smul_iff_of_pos_left, smul_inv_smul₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
rw : a • b₁ ≤ a • a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
rw₁ rw₂ : a • b₁ ≤ b₂ ↔ a • b₁ ≤ b₂
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Premises used: smul_le_smul_iff_of_pos_left, smul_inv_smul₀, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
rw : a • a⁻¹ • b₁ < a • b₂ ↔ b₁ < a • b₂
rw₁ rw₂ : b₁ < a • b₂ ↔ b₁ < a • b₂
⊢ a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂

Tactic:
rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Premises used: smul_inv_smul₀, LT.lt.ne', smul_lt_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
rw : a • b₁ < a • a⁻¹ • b₂ ↔ a • b₁ < b₂
rw₁ rw₂ : a • b₁ < b₂ ↔ a • b₁ < b₂
⊢ b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂

Tactic:
rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Premises used: smul_inv_smul₀, LT.lt.ne', smul_lt_smul_iff_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
rw : a₂ • -_b ≤ a₁ • -_b
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]

Premises used: smul_neg, neg_le_neg_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₂ • -_b ≤ a₁ • -_b

Tactic:
smul_le_smul_of_nonneg_right (β := β) ha <| neg_nonneg.2 hb

Premises used: Iff.mpr, smul_le_smul_of_nonneg_right, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₂ • -_b ≤ a₁ • -_b

Tactic:
exact smul_le_smul_of_nonneg_right (β := β) ha <| neg_nonneg.2 hb

Premises used: Iff.mpr, smul_le_smul_of_nonneg_right, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
rw : a₂ • -_b < a₁ • -_b
⊢ a₁ • _b < a₂ • _b

Tactic:
rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg]

Premises used: neg_lt_neg_iff, smul_neg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₂ • -_b < a₁ • -_b

Tactic:
smul_lt_smul_of_pos_right (β := β) ha <| neg_pos.2 hb

Premises used: Iff.mpr, neg_pos, smul_lt_smul_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₂ • -_b < a₁ • -_b

Tactic:
exact smul_lt_smul_of_pos_right (β := β) ha <| neg_pos.2 hb

Premises used: Iff.mpr, neg_pos, smul_lt_smul_of_pos_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₁ • _b < a₂ • _b
⊢ a₂ • -_b < a₁ • -_b

Tactic:
rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg] at h

Premises used: neg_lt_neg_iff, smul_neg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₂ • -_b < a₁ • -_b
⊢ a₁ < a₂

Tactic:
lt_of_smul_lt_smul_right (β := β) h <| neg_nonneg.2 hb

Premises used: Iff.mpr, lt_of_smul_lt_smul_right, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₂ • -_b < a₁ • -_b
⊢ a₁ < a₂

Tactic:
exact lt_of_smul_lt_smul_right (β := β) h <| neg_nonneg.2 hb

Premises used: Iff.mpr, lt_of_smul_lt_smul_right, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₁ • _b ≤ a₂ • _b
⊢ a₂ • -_b ≤ a₁ • -_b

Tactic:
rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg] at h

Premises used: smul_neg, neg_le_neg_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₂ • -_b ≤ a₁ • -_b
⊢ a₁ ≤ a₂

Tactic:
le_of_smul_le_smul_right (β := β) h <| neg_pos.2 hb

Premises used: Iff.mpr, neg_pos, le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₂ • -_b ≤ a₁ • -_b
⊢ a₁ ≤ a₂

Tactic:
exact le_of_smul_le_smul_right (β := β) h <| neg_pos.2 hb

Premises used: Iff.mpr, neg_pos, le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
obtain : ∀ (a : α) (ha₀ : 0 ≤ a) (ha : a₁ ≤ a₁ + a), a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha

Premises used: exists_nonneg_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
rw : a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂

Tactic:
rw [add_smul, add_smul, add_left_comm]

Premises used: add_left_comm, add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
bc : 0 ≤ a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
simp_rw : a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]

Premises used: add_comm, HSMul.hSMul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁

Tactic:
smul_add_smul_le_smul_add_smul ha hb

Premises used: smul_add_smul_le_smul_add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁

Tactic:
exact smul_add_smul_le_smul_add_smul ha hb

Premises used: smul_add_smul_le_smul_add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ < a₂
hb : b₁ < b₂
obtain : ∀ (a : α) (ha₀ : 0 < a) (ha : a₁ < a₁ + a), a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
obtain ⟨a, ha₀, rfl⟩ := lt_iff_exists_pos_add.1 ha

Premises used: lt_iff_exists_pos_add, Iff.mp, rfl
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
rw : a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)
⊢ a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂

Tactic:
rw [add_smul, add_smul, add_left_comm]

Premises used: add_left_comm, add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
bc : 0 < a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
simp_rw : a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]

Premises used: add_comm, HSMul.hSMul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁

Tactic:
smul_add_smul_lt_smul_add_smul ha hb

Premises used: smul_add_smul_lt_smul_add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁

Tactic:
exact smul_add_smul_lt_smul_add_smul ha hb

Premises used: smul_add_smul_lt_smul_add_smul
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
rw : -a • b₁ ≤ -a • b₂
⊢ a • b₂ ≤ a • b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]

Premises used: neg_smul, neg_neg, Neg.neg, neg_le_neg_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ -a • b₁ ≤ -a • b₂

Tactic:
smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Premises used: neg_nonneg_of_nonpos, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ -a • b₁ ≤ -a • b₂

Tactic:
exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Premises used: neg_nonneg_of_nonpos, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
ha : a ≤ 0
⊢ Antitone (β := β) fun (x : β) ↦ a • x

Tactic:
fun _ _ h ↦ smul_le_smul_of_nonpos_left h ha

Premises used: Antitone, smul_le_smul_of_nonpos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
rw : 0 ≤ (a₂ - a₁) • _b
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
rw [← sub_nonneg, ← sub_smul]

Premises used: sub_smul, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b

Tactic:
smul_nonneg (sub_nonneg.2 ha) hb

Premises used: Iff.mpr, smul_nonneg, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b

Tactic:
exact smul_nonneg (sub_nonneg.2 ha) hb

Premises used: Iff.mpr, smul_nonneg, sub_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
rw : -a • b₁ < -a • b₂
⊢ a • b₂ < a • b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, neg_smul, neg_neg, Neg.neg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂

Tactic:
smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha)

Premises used: neg_pos_of_neg, smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂

Tactic:
exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha)

Premises used: neg_pos_of_neg, smul_lt_smul_of_pos_left