awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PosSMulStrictMono α β
ha : a < 0
⊢ StrictAnti (β := β) fun (x : β) ↦ a • x

Tactic:
fun _ _ h ↦ smul_lt_smul_of_neg_left h ha

Premises used: smul_lt_smul_of_neg_left, StrictAnti
-- 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 : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
rw : 0 < (a₂ - a₁) • _b
⊢ a₁ • _b < a₂ • _b

Tactic:
rw [← sub_pos, ← sub_smul]

Premises used: sub_pos, sub_smul
-- 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 : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b

Tactic:
smul_pos (sub_pos.2 ha) hb

Premises used: Iff.mpr, sub_pos, smul_pos
-- 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 : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b

Tactic:
exact smul_pos (sub_pos.2 ha) hb

Premises used: Iff.mpr, sub_pos, smul_pos
-- 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 : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ -a • b₂ ≤ -a • b₁

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

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 : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
h₁ : -a • b₂ ≤ -a • b₁
⊢ a < 0

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

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 : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Premises used: Iff.mpr, neg_pos, le_of_smul_le_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 : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
exact le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Premises used: Iff.mpr, neg_pos, le_of_smul_le_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 : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
⊢ -a • b₂ < -a • b₁

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

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 : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
h₁ : -a • b₂ < -a • b₁
⊢ a ≤ 0

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

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 : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Premises used: lt_of_smul_lt_smul_of_nonneg_left, neg_nonneg_of_nonpos
-- 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 : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Premises used: lt_of_smul_lt_smul_of_nonneg_left, neg_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : Module α β
inst_6 : SMulPosMono α β
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a • b

Tactic:
smul_nonpos_of_nonpos_of_nonneg (β := βᵒᵈ) ha hb

Premises used: smul_nonpos_of_nonpos_of_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 : PosSMulMono α β
inst_8 : PosSMulReflectLE α β
ha : a < 0
rw : -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ 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 α β
inst_8 : PosSMulReflectLE α β
ha : a < 0
⊢ -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁

Tactic:
smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha)

Premises used: smul_le_smul_iff_of_pos_left, neg_pos_of_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 : PosSMulMono α β
inst_8 : PosSMulReflectLE α β
ha : a < 0
⊢ -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁

Tactic:
exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha)

Premises used: smul_le_smul_iff_of_pos_left, neg_pos_of_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 α β
inst_8 : PosSMulReflectLT α β
ha : a < 0
rw : -a • b₂ < -a • b₁ ↔ b₂ < b₁
⊢ a • b₁ < a • b₂ ↔ b₂ < 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 α β
inst_8 : PosSMulReflectLT α β
ha : a < 0
⊢ -a • b₂ < -a • b₁ ↔ b₂ < b₁

Tactic:
smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha)

Premises used: neg_pos_of_neg, smul_lt_smul_iff_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 α β
inst_8 : PosSMulReflectLT α β
ha : a < 0
⊢ -a • b₂ < -a • b₁ ↔ b₂ < b₁

Tactic:
exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha)

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

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₁ := (0 : β))

Premises used: smul_zero, smul_lt_smul_iff_of_neg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
inst_8 : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

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

Premises used: smul_zero, smul_lt_smul_iff_of_neg_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
a : α
ha : a ≤ 0
b₁ b₂ : β
⊢ a • max b₁ b₂ = min (a • b₁) (a • b₂)

Tactic:
(antitone_smul_left ha : Antitone (_ : β → β)).map_max

Premises used: Antitone.map_max, antitone_smul_left
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
a : α
ha : a ≤ 0
b₁ b₂ : β
⊢ a • min b₁ b₂ = max (a • b₁) (a • b₂)

Tactic:
(antitone_smul_left ha : Antitone (_ : β → β)).map_min

Premises used: antitone_smul_left, Antitone.map_min
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
simp : (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp only [Decidable.or_iff_not_not_and_not, not_and, not_le]

Premises used: not_le, Decidable.or_iff_not_not_and_not, not_and
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Tactic:
fun ab nab ↦ hab.not_gt ?_

Premises used: LE.le.not_gt, Not
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
refine : ∀ (ab : 0 ≤ a → b < 0) (nab : a ≤ 0 → 0 < b), a • b < 0
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Tactic:
refine fun ab nab ↦ hab.not_gt ?_

Premises used: LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a • b < 0
inr :
  ∀ (hab : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b) (ab : LE.le.{u_1} (α := α) 0 0 → b < 0)
    (nab : LE.le.{u_1} (α := α) 0 0 → 0 < b), HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b < 0
inr₁ : ∀ (ha : a < 0), a • b < 0
⊢ a • b < 0

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

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a • b < 0

Tactic:
smul_neg_of_pos_of_neg ha (ab ha.le)

Premises used: LT.lt.le, smul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
b : β
hab : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b
ab : LE.le.{u_1} (α := α) 0 0 → b < 0
nab : LE.le.{u_1} (α := α) 0 0 → 0 < b
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b < 0

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

Premises used: le_rfl, False.elim, LT.lt.asymm
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a • b < 0

Tactic:
smul_neg_of_neg_of_pos ha (nab ha.le)

Premises used: smul_neg_of_neg_of_pos, LT.lt.le
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a • b < 0

Tactic:
exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim,
    smul_neg_of_neg_of_pos ha (nab ha.le)]

Premises used: False.elim, LT.lt.le, LT.lt.asymm, smul_neg_of_pos_of_neg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg,
    fun h ↦ h.elim (and_imp.2 smul_nonneg) (and_imp.2 smul_nonneg_of_nonpos_of_nonpos)⟩

Premises used: Iff.mpr, smul_nonneg, nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg, and_imp, smul_nonneg_of_nonpos_of_nonpos, Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₄ rw₅ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]

Premises used: neg_nonpos, smul_neg, neg_nonneg, smul_nonneg_iff
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
⊢ 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Premises used: neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Premises used: smul_neg, neg_nonneg, smul_nonneg_iff_pos_imp_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]

Premises used: neg_smul, neg_nonneg, smul_nonneg_iff_pos_imp_nonneg
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Premises used: neg_pos, neg_nonneg
-- 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 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
inl : ∀ (h₁ : 0.1 < _b.1), _a₁ ≤ _a₂
inr : ∀ (h₁ : 0.2 < _b.2), _a₁ ≤ _a₂
⊢ _a₁ ≤ _a₂

Tactic:
rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩

Premises used: Prod.lt_iff, Iff.mp
-- 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 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.1 < _b.1
⊢ _a₁ ≤ _a₂

Tactic:
le_of_smul_le_smul_right h.1 h₁

Premises used: le_of_smul_le_smul_right, And.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 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.1 < _b.1
⊢ _a₁ ≤ _a₂

Tactic:
exact le_of_smul_le_smul_right h.1 h₁

Premises used: le_of_smul_le_smul_right, And.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 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂

Tactic:
le_of_smul_le_smul_right h.2 h₁

Premises used: le_of_smul_le_smul_right, And.right
-- 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 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂

Tactic:
exact le_of_smul_le_smul_right h.2 h₁

Premises used: le_of_smul_le_smul_right, And.right
-- 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 α γ
simp_rw :
  ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β × γ⦄ (hb : b₁.1 < b₂.1 ∧ b₁.2 ≤ b₂.2 ∨ b₁.1 ≤ b₂.1 ∧ 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
⊢ ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β × γ⦄ (hb : b₁ < b₂), 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 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:
.inl ⟨smul_lt_smul_of_pos_left h₁ ha, smul_le_smul_of_nonneg_left h₂ ha.le⟩

Premises used: LT.lt.le, And.intro, Or.inl, smul_lt_smul_of_pos_left, 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 .inl ⟨smul_lt_smul_of_pos_left h₁ ha, smul_le_smul_of_nonneg_left h₂ ha.le⟩