awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
h : 1 < b
⊢ a < a * b

Tactic:
calc
    a = a * 1 := (mul_one a).symm
    _ < a * b := mul_lt_mul_right h a

Premises used: Trans.trans, mul_lt_mul_right, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
h : b < 1
⊢ a * b < a

Tactic:
calc
    a * b < a * 1 := mul_lt_mul_right h a
    _ = a := mul_one a

Premises used: Trans.trans, mul_lt_mul_right, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
h : 1 < b
⊢ a < b * a

Tactic:
calc
    a = 1 * a := (one_mul a).symm
    _ < b * a := mul_lt_mul_left h a

Premises used: Trans.trans, mul_lt_mul_left, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
h : b < 1
⊢ b * a < a

Tactic:
calc
    b * a < 1 * a := mul_lt_mul_left h a
    _ = a := one_mul a

Premises used: Trans.trans, mul_lt_mul_left, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftReflectLT α
a b : α
h : a < a * b
⊢ a * 1 < a * b

Tactic:
simpa only [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftReflectLT α
a b : α
h : a * b < a
⊢ a * b < a * 1

Tactic:
simpa only [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightReflectLT α
a b : α
h : b < a * b
⊢ 1 * b < a * b

Tactic:
simpa only [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightReflectLT α
a b : α
h : a * b < b
⊢ a * b < 1 * b

Tactic:
simpa only [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulLeftReflectLT α
a b : α
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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
inst_3 : MulRightReflectLT α
a b : α
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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulLeftReflectLT α
a b : α
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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LT α
inst_2 : MulRightStrictMono α
inst_3 : MulRightReflectLT α
a 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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b ≤ c
ha : a ≤ 1
⊢ b * a ≤ c

Tactic:
calc
    b * a ≤ b * 1 := mul_le_mul_right ha b
    _ = b := mul_one b
    _ ≤ c := hbc

Premises used: Trans.trans, mul_le_mul_right, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c : α
hbc : b ≤ c
ha : a < 1
⊢ b * a < c

Tactic:
calc
    b * a < b * 1 := mul_lt_mul_right ha b
    _ = b := mul_one b
    _ ≤ c := hbc

Premises used: Trans.trans, mul_lt_mul_right, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b < c
ha : a ≤ 1
⊢ b * a < c

Tactic:
calc
    b * a ≤ b * 1 := mul_le_mul_right ha b
    _ = b := mul_one b
    _ < c := hbc

Premises used: Trans.trans, mul_le_mul_right, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c : α
hbc : b < c
ha : a < 1
⊢ b * a < c

Tactic:
calc
    b * a < b * 1 := mul_lt_mul_right ha b
    _ = b := mul_one b
    _ < c := hbc

Premises used: Trans.trans, mul_lt_mul_right, mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b < c
ha : a < 1
⊢ b * a < c

Tactic:
mul_lt_of_lt_of_le_one hbc ha.le

Premises used: mul_lt_of_lt_of_le_one, LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : a ≤ 1
hb : b ≤ 1
⊢ a * b ≤ 1

Tactic:
mul_le_of_le_of_le_one ha hb

Premises used: mul_le_of_le_of_le_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b : α
ha : a ≤ 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_le_of_lt_one ha hb

Premises used: mul_lt_of_le_of_lt_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : a < 1
hb : b ≤ 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_of_le_one ha hb

Premises used: mul_lt_of_lt_of_le_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b : α
ha : a < 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_of_lt_one ha hb

Premises used: mul_lt_of_lt_of_lt_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : a < 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_of_lt_one' ha hb

Premises used: mul_lt_of_lt_of_lt_one'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b ≤ c
ha : 1 ≤ a
⊢ b ≤ c * a

Tactic:
calc
    b ≤ c := hbc
    _ = c * 1 := (mul_one c).symm
    _ ≤ c * a := mul_le_mul_right ha c

Premises used: Trans.trans, mul_le_mul_right, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c : α
hbc : b ≤ c
ha : 1 < a
⊢ b < c * a

Tactic:
calc
    b ≤ c := hbc
    _ = c * 1 := (mul_one c).symm
    _ < c * a := mul_lt_mul_right ha c

Premises used: Trans.trans, mul_lt_mul_right, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b < c
ha : 1 ≤ a
⊢ b < c * a

Tactic:
calc
    b < c := hbc
    _ = c * 1 := (mul_one c).symm
    _ ≤ c * a := mul_le_mul_right ha c

Premises used: Trans.trans, mul_le_mul_right, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c : α
hbc : b < c
ha : 1 < a
⊢ b < c * a

Tactic:
calc
    b < c := hbc
    _ = c * 1 := (mul_one c).symm
    _ < c * a := mul_lt_mul_right ha c

Premises used: Trans.trans, mul_lt_mul_right, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
hbc : b < c
ha : 1 < a
⊢ b < c * a

Tactic:
lt_mul_of_lt_of_one_le hbc ha.le

Premises used: LT.lt.le, lt_mul_of_lt_of_one_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ a * b

Tactic:
le_mul_of_le_of_one_le ha hb

Premises used: le_mul_of_le_of_one_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b : α
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_le_of_one_lt ha hb

Premises used: lt_mul_of_le_of_one_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : IsBotOneClass α
inst_3 : MulLeftStrictMono α
b : α
hb : 1 < b
a : α
⊢ 1 < a * b

Tactic:
Left.one_lt_mul_of_le_of_lt one_le hb

Premises used: one_le, Left.one_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
lt_mul_of_lt_of_one_le ha hb

Premises used: lt_mul_of_lt_of_one_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : IsBotOneClass α
inst_3 : MulLeftMono α
a : α
ha : 1 < a
b : α
⊢ 1 < a * b

Tactic:
Left.one_lt_mul_of_lt_of_le ha one_le

Premises used: Left.one_lt_mul_of_lt_of_le, one_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b : α
ha : 1 < a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_lt_of_one_lt ha hb

Premises used: lt_mul_of_lt_of_one_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b : α
ha : 1 < a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_lt_of_one_lt' ha hb

Premises used: lt_mul_of_lt_of_one_lt'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : a ≤ 1
hbc : b ≤ c
⊢ a * b ≤ c

Tactic:
calc
    a * b ≤ 1 * b := mul_le_mul_left ha b
    _ = b := one_mul b
    _ ≤ c := hbc

Premises used: Trans.trans, mul_le_mul_left, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b c : α
ha : a < 1
hbc : b ≤ c
⊢ a * b < c

Tactic:
calc
    a * b < 1 * b := mul_lt_mul_left ha b
    _ = b := one_mul b
    _ ≤ c := hbc

Premises used: Trans.trans, mul_lt_mul_left, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : a ≤ 1
hb : b < c
⊢ a * b < c

Tactic:
calc
    a * b ≤ 1 * b := mul_le_mul_left ha b
    _ = b := one_mul b
    _ < c := hb

Premises used: Trans.trans, mul_le_mul_left, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b c : α
ha : a < 1
hb : b < c
⊢ a * b < c

Tactic:
calc
    a * b < 1 * b := mul_lt_mul_left ha b
    _ = b := one_mul b
    _ < c := hb

Premises used: Trans.trans, mul_lt_mul_left, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : a < 1
hbc : b < c
⊢ a * b < c

Tactic:
mul_lt_of_le_one_of_lt ha.le hbc

Premises used: mul_lt_of_le_one_of_lt, LT.lt.le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : a ≤ 1
hb : b ≤ 1
⊢ a * b ≤ 1

Tactic:
mul_le_of_le_one_of_le ha hb

Premises used: mul_le_of_le_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b : α
ha : a < 1
hb : b ≤ 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_one_of_le ha hb

Premises used: mul_lt_of_lt_one_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : a ≤ 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_le_one_of_lt ha hb

Premises used: mul_lt_of_le_one_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b : α
ha : a < 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_one_of_lt ha hb

Premises used: mul_lt_of_lt_one_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : a < 1
hb : b < 1
⊢ a * b < 1

Tactic:
mul_lt_of_lt_one_of_lt' ha hb

Premises used: mul_lt_of_lt_one_of_lt'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : 1 ≤ a
hbc : b ≤ c
⊢ b ≤ a * c

Tactic:
calc
    b ≤ c := hbc
    _ = 1 * c := (one_mul c).symm
    _ ≤ a * c := mul_le_mul_left ha c

Premises used: Trans.trans, mul_le_mul_left, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b c : α
ha : 1 < a
hbc : b ≤ c
⊢ b < a * c

Tactic:
calc
    b ≤ c := hbc
    _ = 1 * c := (one_mul c).symm
    _ < a * c := mul_lt_mul_left ha c

Premises used: Trans.trans, mul_lt_mul_left, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : 1 ≤ a
hbc : b < c
⊢ b < a * c

Tactic:
calc
    b < c := hbc
    _ = 1 * c := (one_mul c).symm
    _ ≤ a * c := mul_le_mul_left ha c

Premises used: Trans.trans, mul_le_mul_left, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b c : α
ha : 1 < a
hbc : b < c
⊢ b < a * c

Tactic:
calc
    b < c := hbc
    _ = 1 * c := (one_mul c).symm
    _ < a * c := mul_lt_mul_left ha c

Premises used: Trans.trans, mul_lt_mul_left, Eq.symm, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
ha : 1 < a
hbc : b < c
⊢ b < a * c

Tactic:
lt_mul_of_one_le_of_lt ha.le hbc

Premises used: LT.lt.le, lt_mul_of_one_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 ≤ a * b

Tactic:
le_mul_of_one_le_of_le ha hb

Premises used: le_mul_of_one_le_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b : α
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
lt_mul_of_one_lt_of_le ha hb

Premises used: lt_mul_of_one_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : IsBotOneClass α
inst_3 : MulRightStrictMono α
a : α
ha : 1 < a
b : α
⊢ 1 < a * b

Tactic:
Right.one_lt_mul_of_lt_of_le ha one_le

Premises used: Right.one_lt_mul_of_lt_of_le, one_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_one_le_of_lt ha hb

Premises used: lt_mul_of_one_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : IsBotOneClass α
inst_3 : MulRightMono α
b : α
hb : 1 < b
a : α
⊢ 1 < a * b

Tactic:
Right.one_lt_mul_of_le_of_lt one_le hb

Premises used: one_le, Right.one_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a b : α
ha : 1 < a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_one_lt_of_lt ha hb

Premises used: lt_mul_of_one_lt_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b : α
ha : 1 < a
hb : 1 < b
⊢ 1 < a * b

Tactic:
lt_mul_of_one_lt_of_lt' ha hb

Premises used: lt_mul_of_one_lt_of_lt'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
h : a * b < c
hle : 1 ≤ b
⊢ a < c

Tactic:
(le_mul_of_one_le_right' hle).trans_lt h

Premises used: le_mul_of_one_le_right', LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
h : a * b ≤ c
hle : 1 ≤ b
⊢ a ≤ c

Tactic:
(le_mul_of_one_le_right' hle).trans h

Premises used: LE.le.trans, le_mul_of_one_le_right'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
h : a < b * c
hle : c ≤ 1
⊢ a < b

Tactic:
h.trans_le (mul_le_of_le_one_right' hle)

Premises used: mul_le_of_le_one_right', LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c : α
h : a ≤ b * c
hle : c ≤ 1
⊢ a ≤ b

Tactic:
h.trans (mul_le_of_le_one_right' hle)

Premises used: mul_le_of_le_one_right', LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
h : a * b < c
hle : 1 ≤ a
⊢ b < c

Tactic:
(le_mul_of_one_le_left' hle).trans_lt h

Premises used: le_mul_of_one_le_left', LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
h : a * b ≤ c
hle : 1 ≤ a
⊢ b ≤ c

Tactic:
(le_mul_of_one_le_left' hle).trans h

Premises used: le_mul_of_one_le_left', LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
h : a < b * c
hle : b ≤ 1
⊢ a < c

Tactic:
h.trans_le (mul_le_of_le_one_left' hle)

Premises used: mul_le_of_le_one_left', LT.lt.trans_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c : α
h : a ≤ b * c
hle : b ≤ 1
⊢ a ≤ c

Tactic:
h.trans (mul_le_of_le_one_left' hle)

Premises used: mul_le_of_le_one_left', LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
ha hb : LE.le.{u_1} (α := α) 1 1
rw rw₁ : Eq.{u_1 + 1} (α := α) 1 1
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulLeftMono α
a b : α
ha : a ≤ 1
hb : b ≤ 1
hab : 1 ≤ a * b
⊢ a = 1

Tactic:
ha.eq_of_not_lt fun h => hab.not_gt <| mul_lt_one_of_lt_of_le h hb

Premises used: mul_lt_one_of_lt_of_le, LE.le.eq_of_not_lt, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulLeftMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
hab : a * b ≤ 1
⊢ a = 1

Tactic:
ha.eq_of_not_lt' fun h => hab.not_gt <| one_lt_mul_of_lt_of_le' h hb

Premises used: LE.le.eq_of_not_lt', LE.le.not_gt, one_lt_mul_of_lt_of_le'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulRightMono α
a b : α
ha : a ≤ 1
hb : b ≤ 1
hab : 1 ≤ a * b
⊢ b = 1

Tactic:
hb.eq_of_not_lt fun h => hab.not_gt <| Right.mul_lt_one_of_le_of_lt ha h

Premises used: LE.le.eq_of_not_lt, Right.mul_lt_one_of_le_of_lt, LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
hab : a * b ≤ 1
⊢ b = 1

Tactic:
hb.eq_of_not_lt' fun h => hab.not_gt <| Right.one_lt_mul_of_le_of_lt ha h

Premises used: LE.le.eq_of_not_lt', LE.le.not_gt, Right.one_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
pos : ∀ (h : a < 1), ∃ (b : α), b * b ≤ a
neg : ∀ (h : 1 ≤ a), ∃ (b : α), b * b ≤ a
⊢ ∃ (b : α), b * b ≤ a

Tactic:
by_cases! h : a < 1
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
h₁ : a * a ≤ a
⊢ ∃ (b : α), b * b ≤ a

Tactic:
use a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a < a * 1

Tactic:
have : a * a < a * 1 := mul_lt_mul_right h a
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a < a

Tactic:
rw [mul_one] at this

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a

Tactic:
le_of_lt this

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a
⊢ a * a ≤ a

Tactic:
exact le_of_lt this

Premises used: le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : 1 ≤ a
h₁ : HMul.hMul (α := α) 1 1 ≤ a
⊢ ∃ (b : α), b * b ≤ a

Tactic:
use 1
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a : α
h : 1 ≤ a
h₁ h₂ h₃ h₄ : 1 ≤ a
⊢ HMul.hMul (α := α) 1 1 ≤ a

Tactic:
rwa [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
inst_3 : MulLeftMono α
hf : Monotone f
a : α
⊢ Monotone.{u_2, u_1} (β := α) fun (x : β) ↦ a * f x

Tactic:
mul_right_mono.comp hf

Premises used: Monotone.comp, mul_right_mono
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
s : Set β
inst_3 : MulLeftMono α
hf : MonotoneOn f s
a : α
⊢ MonotoneOn.{u_2, u_1} (β := α) (fun (x : β) ↦ a * f x) s

Tactic:
mul_right_mono.comp_monotoneOn hf

Premises used: mul_right_mono, Monotone.comp_monotoneOn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
inst_3 : MulLeftMono α
hf : Antitone f
a : α
⊢ Antitone.{u_2, u_1} (β := α) fun (x : β) ↦ a * f x

Tactic:
mul_right_mono.comp_antitone hf

Premises used: mul_right_mono, Monotone.comp_antitone
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
s : Set β
inst_3 : MulLeftMono α
hf : AntitoneOn f s
a : α
⊢ AntitoneOn.{u_2, u_1} (β := α) (fun (x : β) ↦ a * f x) s

Tactic:
mul_right_mono.comp_antitoneOn hf

Premises used: mul_right_mono, Monotone.comp_antitoneOn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
inst_3 : MulRightMono α
hf : Monotone f
a : α
⊢ Monotone.{u_2, u_1} (β := α) fun (x : β) ↦ f x * a

Tactic:
mul_left_mono.comp hf

Premises used: Monotone.comp, mul_left_mono
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f : β → α
s : Set β
inst_3 : MulRightMono α
hf : MonotoneOn f s
a : α
⊢ MonotoneOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * a) s

Tactic:
mul_left_mono.comp_monotoneOn hf

Premises used: mul_left_mono, Monotone.comp_monotoneOn