awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : MulPosStrictMono α
⊢ MulPosMono α

Tactic:
mulPosMono_iff_covariant_pos.2 (covariantClass_le_of_lt _ _ _)

Premises used: Iff.mpr, mulPosMono_iff_covariant_pos, covariantClass_le_of_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MulZeroClass α
a_1 b_1 c d : α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLE α
a : α>0
b : α
h : (↑a : α) * b < (↑a : α) * b
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MulZeroClass α
a_1 b_1 c d : α
inst_1 : PartialOrder α
inst_2 : MulPosReflectLE α
a : α>0
b : α
h : b * (↑a : α) < b * (↑a : α)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c : α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLE α
a0 : 0 < a
⊢ a * b = a * c ↔ b = c

Tactic:
⟨fun h => (le_of_mul_le_mul_of_pos_left h.le a0).antisymm <|
    le_of_mul_le_mul_of_pos_left h.ge a0, congr_arg _⟩

Premises used: Eq.ge, LE.le.antisymm, Eq.le, le_of_mul_le_mul_of_pos_left, congr_arg, Iff.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c : α
inst_1 : PartialOrder α
inst_2 : MulPosReflectLE α
b0 : 0 < b
⊢ a * b = c * b ↔ a = c

Tactic:
⟨fun h => (le_of_mul_le_mul_of_pos_right h.le b0).antisymm <|
    le_of_mul_le_mul_of_pos_right h.ge b0, congr_arg (· * b)⟩

Premises used: le_of_mul_le_mul_of_pos_right, Eq.ge, HMul.hMul, LE.le.antisymm, Eq.le, congr_arg, Iff.intro
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a c : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
refine : ∀ (h : a * c = b * d), a = b ∧ c = d
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
simp : ¬a < b ∧ ¬c < d
⊢ a = b ∧ c = d

Tactic:
simp only [eq_iff_le_not_lt, hab, hcd, true_and]

Premises used: eq_iff_le_not_lt, true_and
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d

Tactic:
⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩

Premises used: And.intro, Eq.not_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
refine_1 : ∀ (hab : a < b), a * c < b * d
refine_2 : ∀ (hcd : c < d), a * c < b * d
⊢ ¬a < b ∧ ¬c < d

Tactic:
refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab_1 : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
(mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)

Premises used: LT.lt.le, mul_lt_mul_of_pos_right, LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab_1 : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)

Premises used: LT.lt.le, mul_lt_mul_of_pos_right, LE.le.trans_lt, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd_1 : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

Premises used: mul_lt_mul_of_pos_left, LT.lt.le, mul_le_mul_of_nonneg_right, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd_1 : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

Premises used: mul_lt_mul_of_pos_left, LT.lt.le, mul_le_mul_of_nonneg_right, LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a c : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ c
⊢ a * c = a * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
refine : ∀ (h : a * c = b * d), a = b ∧ c = d
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
simp : ¬a < b ∧ ¬c < d
⊢ a = b ∧ c = d

Tactic:
simp only [eq_iff_le_not_lt, hab, hcd, true_and]

Premises used: eq_iff_le_not_lt, true_and
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d

Tactic:
⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩

Premises used: And.intro, Eq.not_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
refine_1 : ∀ (hab : a < b), a * c < b * d
refine_2 : ∀ (hcd : c < d), a * c < b * d
⊢ ¬a < b ∧ ¬c < d

Tactic:
refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab_1 : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
(mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)

Premises used: LT.lt.le, mul_lt_mul_of_pos_right, LT.lt.trans_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab_1 : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)

Premises used: LT.lt.le, mul_lt_mul_of_pos_right, LT.lt.trans_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd_1 : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
(mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

Premises used: mul_lt_mul_of_pos_left, LT.lt.le, mul_le_mul_of_nonneg_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b c d : α
inst_1 : PartialOrder α
inst_2 : PosMulStrictMono α
inst_3 : MulPosStrictMono α
hab : a ≤ b
hcd_1 : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

Premises used: mul_lt_mul_of_pos_left, LT.lt.le, mul_le_mul_of_nonneg_right, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
inr : ∀ (hab : 0 < 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:
rcases lt_trichotomy a 0 with (ha | rfl | ha)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg ha.le hb

Premises used: mul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ha.le hb

Premises used: mul_nonpos_of_nonpos_of_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < 0 * b
⊢ LT.lt.{u_1} (α := α) 0 0

Tactic:
rw [zero_mul] at hab

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : LT.lt.{u_1} (α := α) 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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : LT.lt.{u_1} (α := α) 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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
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.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : 0 < a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos ha.le hb

Premises used: LT.lt.le, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
ha : 0 < a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

Premises used: LT.lt.le, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
h : 0 < a * b
ha : a ≤ 0
⊢ b < 0

Tactic:
((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_left fun h => h.1.not_ge ha).2

Premises used: pos_and_pos_or_neg_and_neg_of_mul_pos, Or.resolve_left, And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
h : 0 < a * b
ha : b ≤ 0
⊢ a < 0

Tactic:
((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_left fun h => h.2.not_ge ha).1

Premises used: pos_and_pos_or_neg_and_neg_of_mul_pos, Or.resolve_left, And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
inst_3 : MulPosMono α
hab : 0 < a * b
⊢ a < 0 ↔ b < 0

Tactic:
⟨neg_of_mul_pos_right hab ∘ le_of_lt, neg_of_mul_pos_left hab ∘ le_of_lt⟩

Premises used: le_of_lt, Function.comp, neg_of_mul_pos_right, Iff.intro, neg_of_mul_pos_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
h : a * b < 0
a0 : 0 ≤ a
⊢ b < 0

Tactic:
lt_of_not_ge fun b0 : b ≥ 0 => (Left.mul_nonneg a0 b0).not_gt h

Premises used: lt_of_not_ge, Left.mul_nonneg, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : MulPosMono α
h : a * b < 0
a0 : 0 ≤ a
⊢ b < 0

Tactic:
lt_of_not_ge fun b0 : b ≥ 0 => (Right.mul_nonneg a0 b0).not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt, Right.mul_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : PosMulMono α
h : a * b < 0
b0 : 0 ≤ b
⊢ a < 0

Tactic:
lt_of_not_ge fun a0 : a ≥ 0 => (Left.mul_nonneg a0 b0).not_gt h

Premises used: lt_of_not_ge, Left.mul_nonneg, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
a b : α
inst_1 : LinearOrder α
inst_2 : MulPosMono α
h : a * b < 0
b0 : 0 ≤ b
⊢ a < 0

Tactic:
lt_of_not_ge fun a0 : a ≥ 0 => (Right.mul_nonneg a0 b0).not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt, Right.mul_nonneg
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulReflectLT α
ha : 0 ≤ a
h : a < a * b
⊢ a * 1 < a * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosReflectLT α
hb : 0 ≤ b
h : b < a * b
⊢ 1 * b < a * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulReflectLE α
ha : 0 < a
h : a ≤ a * b
⊢ a * 1 ≤ a * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosReflectLE α
hb : 0 < b
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
inst_4 : PosMulReflectLE α
a0 : 0 < a
rw rw₁ : a ≤ a * b ↔ a ≤ a * b
⊢ a ≤ a * b ↔ a * 1 ≤ a * b

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
inst_4 : PosMulReflectLT α
a0 : 0 < a
rw rw₁ : a < a * b ↔ a < a * b
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
inst_4 : PosMulReflectLE α
a0 : 0 < a
rw rw₁ : a * b ≤ a ↔ a * b ≤ a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
inst_4 : PosMulReflectLT α
a0 : 0 < a
rw rw₁ : a * b < a ↔ a * b < a
⊢ a * b < a ↔ a * b < a * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
inst_4 : MulPosReflectLE α
a0 : 0 < a
rw rw₁ : a ≤ b * a ↔ a ≤ b * a
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
inst_4 : MulPosReflectLT α
a0 : 0 < a
rw rw₁ : a < b * a ↔ a < b * a
⊢ a < b * a ↔ 1 * a < b * a

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
inst_4 : MulPosReflectLE α
b0 : 0 < b
rw rw₁ : a * b ≤ b ↔ a * b ≤ b
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
inst_4 : MulPosReflectLT α
b0 : 0 < b
rw rw₁ : a * b < b ↔ a * b < b
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
hb : 0 ≤ b
h : a ≤ 1
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Premises used: mul_le_mul_of_nonneg_right, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Premises used: mul_le_mul_of_nonneg_right, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Premises used: mul_one, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Premises used: mul_one, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
hb : 0 < b
h : a < 1
⊢ a * b < b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Premises used: mul_lt_mul_of_pos_right, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Premises used: mul_lt_mul_of_pos_right, one_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
ha : 0 < a
h : b < 1
⊢ a * b < a

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Premises used: mul_lt_mul_of_pos_left, mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Zero α
a b : α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
ha : 0 < a
h : 1 < b
⊢ a < a * b

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Premises used: mul_lt_mul_of_pos_left, mul_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Preorder M₀
inst_3 : Preorder α
f g : α → M₀
inst_4 : PosMulMono M₀
inst_5 : MulPosMono M₀
hf : Monotone f
hg : Monotone g
hf₀ : ∀ (x : α), 0 ≤ f x
hg₀ : ∀ (x : α), 0 ≤ g x
⊢ Monotone (f * g)

Tactic:
fun _ _ h ↦ mul_le_mul (hf h) (hg h) (hg₀ _) (hf₀ _)

Premises used: Monotone, mul_le_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
α : Type u_1
M₀ : Type u_2
inst : Mul M₀
inst_1 : Zero M₀
inst_2 : Preorder M₀
inst_3 : Preorder α
f g : α → M₀
inst_4 : PosMulMono M₀
inst_5 : MulPosMono M₀
s : Set α
hf : MonotoneOn f s
hg : MonotoneOn g s
hf₀ : ∀ (x : α), x ∈ s → 0 ≤ f x
hg₀ : ∀ (x : α), x ∈ s → 0 ≤ g x
⊢ MonotoneOn (f * g) s

Tactic:
fun _ ha _ hb h ↦ mul_le_mul (hf ha hb h) (hg ha hb h) (hg₀ _ ha) (hf₀ _ hb)

Premises used: MonotoneOn, mul_le_mul
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
inst_2 : ZeroLEOneClass M₀
n : ℕ
rw : LE.le.{u_2} (α := M₀) 0 1
⊢ HPow.hPow (α := M₀) 0 (n + 1) ≤ 1

Tactic:
rw [zero_pow n.succ_ne_zero]

Premises used: Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
inst_2 : ZeroLEOneClass M₀
n : ℕ
⊢ LE.le.{u_2} (α := M₀) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
inst_2 : ZeroLEOneClass M₀
n : ℕ
⊢ LE.le.{u_2} (α := M₀) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
⊢ ZeroLEOneClass M₀

Tactic:
have : ZeroLEOneClass M₀ := ⟨ha₀.trans ha₁⟩
-- Module: Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
inst_1 : Preorder M₀
a : M₀
inst_2 : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
rw : a ^ n * a ≤ a ^ n * 1
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
rw [← mul_one (a ^ n), pow_succ]

Premises used: pow_succ, HPow.hPow, mul_one