awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Antitone f
a : α
⊢ Antitone.{u_2, u_1} (β := α) fun (x : β) ↦ f x * a

Tactic:
mul_left_mono.comp_antitone hf

Premises used: mul_left_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 : MulRightMono α
hf : AntitoneOn f s
a : α
⊢ AntitoneOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * a) s

Tactic:
mul_left_mono.comp_antitoneOn hf

Premises used: mul_left_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 g : β → α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
hf : Monotone f
hg : Monotone g
⊢ Monotone.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ h => mul_le_mul' (hf h) (hg h)

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

Tactic:
fun _ hx _ hy h =>
  mul_le_mul' (hf hx hy h) (hg hx hy h)

Premises used: MonotoneOn, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
hf : Antitone f
hg : Antitone g
⊢ Antitone.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ h => mul_le_mul' (hf h) (hg h)

Premises used: Antitone, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
s : Set β
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
hf : AntitoneOn f s
hg : AntitoneOn g s
⊢ AntitoneOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ hx _ hy h => mul_le_mul' (hf hx hy h) (hg hx hy h)

Premises used: AntitoneOn, mul_le_mul'
-- 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 : MulLeftStrictMono α
hf : StrictMono f
c : α
⊢ StrictMono.{u_2, u_1} (β := α) fun (x : β) ↦ c * f x

Tactic:
fun _ _ ab => mul_lt_mul_right (hf ab) c

Premises used: StrictMono, mul_lt_mul_right
-- 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 : MulLeftStrictMono α
hf : StrictMonoOn f s
c : α
⊢ StrictMonoOn.{u_2, u_1} (β := α) (fun (x : β) ↦ c * f x) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_right (hf ha hb ab) c

Premises used: mul_lt_mul_right, StrictMonoOn
-- 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 : MulLeftStrictMono α
hf : StrictAnti f
c : α
⊢ StrictAnti.{u_2, u_1} (β := α) fun (x : β) ↦ c * f x

Tactic:
fun _ _ ab => mul_lt_mul_right (hf ab) c

Premises used: mul_lt_mul_right, StrictAnti
-- 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 : MulLeftStrictMono α
hf : StrictAntiOn f s
c : α
⊢ StrictAntiOn.{u_2, u_1} (β := α) (fun (x : β) ↦ c * f x) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_right (hf ha hb ab) c

Premises used: StrictAntiOn, mul_lt_mul_right
-- 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 : MulRightStrictMono α
hf : StrictMono f
c : α
⊢ StrictMono.{u_2, u_1} (β := α) fun (x : β) ↦ f x * c

Tactic:
fun _ _ ab => mul_lt_mul_left (hf ab) c

Premises used: StrictMono, mul_lt_mul_left
-- 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 : MulRightStrictMono α
hf : StrictMonoOn f s
c : α
⊢ StrictMonoOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * c) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_left (hf ha hb ab) c

Premises used: mul_lt_mul_left, StrictMonoOn
-- 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 : MulRightStrictMono α
hf : StrictAnti f
c : α
⊢ StrictAnti.{u_2, u_1} (β := α) fun (x : β) ↦ f x * c

Tactic:
fun _ _ ab => mul_lt_mul_left (hf ab) c

Premises used: StrictAnti, mul_lt_mul_left
-- 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 : MulRightStrictMono α
hf : StrictAntiOn f s
c : α
⊢ StrictAntiOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * c) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_left (hf ha hb ab) c

Premises used: StrictAntiOn, mul_lt_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
hf : StrictMono f
hg : StrictMono g
⊢ StrictMono.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ ab =>
  mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

Premises used: StrictMono, mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
s : Set β
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
hf : StrictMonoOn f s
hg : StrictMonoOn g s
⊢ StrictMonoOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

Premises used: mul_lt_mul_of_lt_of_lt, StrictMonoOn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
hf : StrictAnti f
hg : StrictAnti g
⊢ StrictAnti.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ ab => mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

Premises used: StrictAnti, mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
s : Set β
inst_3 : MulLeftStrictMono α
inst_4 : MulRightStrictMono α
hf : StrictAntiOn f s
hg : StrictAntiOn g s
⊢ StrictAntiOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

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

Tactic:
fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)

Premises used: StrictMono, LT.lt.le, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
s : Set β
inst_3 : MulLeftStrictMono α
inst_4 : MulRightMono α
f g : β → α
hf : MonotoneOn f s
hg : StrictMonoOn g s
⊢ StrictMonoOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)

Premises used: LT.lt.le, mul_lt_mul_of_le_of_lt, StrictMonoOn
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulLeftStrictMono α
inst_4 : MulRightMono α
f g : β → α
hf : Antitone f
hg : StrictAnti g
⊢ StrictAnti.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ h => mul_lt_mul_of_le_of_lt (hf h.le) (hg h)

Premises used: LT.lt.le, StrictAnti, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
s : Set β
inst_3 : MulLeftStrictMono α
inst_4 : MulRightMono α
f g : β → α
hf : AntitoneOn f s
hg : StrictAntiOn g s
⊢ StrictAntiOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ hx _ hy h => mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)

Premises used: StrictAntiOn, LT.lt.le, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
hf : StrictMono f
hg : Monotone g
⊢ StrictMono.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ h => mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

Premises used: StrictMono, LT.lt.le, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
s : Set β
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
hf : StrictMonoOn f s
hg : MonotoneOn g s
⊢ StrictMonoOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ hx _ hy h => mul_lt_mul_of_lt_of_le (hf hx hy h) (hg hx hy h.le)

Premises used: LT.lt.le, StrictMonoOn, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
hf : StrictAnti f
hg : Antitone g
⊢ StrictAnti.{u_2, u_1} (β := α) fun (x : β) ↦ f x * g x

Tactic:
fun _ _ h => mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

Premises used: LT.lt.le, StrictAnti, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : Preorder α
inst_2 : Preorder β
f g : β → α
s : Set β
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
hf : StrictAntiOn f s
hg : AntitoneOn g s
⊢ StrictAntiOn.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) s

Tactic:
fun _ hx _ hy h => mul_lt_mul_of_lt_of_le (hf hx hy h) (hg hx hy h.le)

Premises used: StrictAntiOn, LT.lt.le, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_3
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ cmp (a * b) (a * c) = cmp b c

Tactic:
(strictMono_id.const_mul' a).cmp_map_eq b c

Premises used: strictMono_id, StrictMono.const_mul', StrictMono.cmp_map_eq
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_3
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulRightStrictMono α
a b c : α
⊢ cmp (a * c) (b * c) = cmp a b

Tactic:
(strictMono_id.mul_const' c).cmp_map_eq a b

Premises used: strictMono_id, StrictMono.cmp_map_eq, StrictMono.mul_const'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LE α
inst_2 : MulLeftReflectLE α
a : α
⊢ _root_.MulLECancellable a

Tactic:
fun _ _ => le_of_mul_le_mul_left'

Premises used: MulLECancellable, le_of_mul_le_mul_left'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
a b : α
⊢ 1 * a ≤ 1 * b → a ≤ b

Tactic:
simpa only [one_mul] using id

Premises used: id, one_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
a : α
ha : MulLECancellable a
⊢ Injective (β := α) fun (x : α) ↦ a * x

Tactic:
fun _ _ h => le_antisymm (ha h.le) (ha h.ge)

Premises used: Eq.ge, Eq.le, le_antisymm, Function.Injective
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
a : α
ha : MulLECancellable a
⊢ IsLeftRegular a

Tactic:
ha.Injective

Premises used: MulLECancellable.Injective
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
a b c : α
ha : MulLECancellable a
⊢ a * b = a * c ↔ b = c

Tactic:
ha.Injective.eq_iff

Premises used: Function.Injective.eq_iff, MulLECancellable.Injective
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : IsMulCommutative α
inst_2 : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : Eq.{u_1 + 1} (α := α) ((fun (x : α) ↦ x * a) b) ((fun (x : α) ↦ x * a) c)
rwa : b * a = a * c
rwa₁ rwa₂ rwa₃ rwa₄ : b * a = c * a
⊢ a * b = a * c

Tactic:
rwa [mul_comm' a, mul_comm' a]

Premises used: mul_comm'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : IsMulCommutative α
inst_2 : PartialOrder α
a b c : α
hc : MulLECancellable c
⊢ a * c = b * c ↔ a = b

Tactic:
hc.injective_left.eq_iff

Premises used: Function.Injective.eq_iff, MulLECancellable.injective_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Mul α
inst_2 : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ a * b ≤ a * c ↔ b ≤ c

Tactic:
⟨fun h => ha h, fun h => mul_le_mul_right h a⟩

Premises used: mul_le_mul_right, Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Mul α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b c : α
ha : MulLECancellable a
rw : a * b ≤ c * a ↔ b ≤ c
rw₁ : a * b ≤ a * c ↔ b ≤ c
rw₂ rw₃ : b ≤ c ↔ b ≤ c
⊢ b * a ≤ c * a ↔ b ≤ c

Tactic:
rw [mul_comm' b, mul_comm' c, ha.mul_le_mul_iff_left]

Premises used: mul_comm', MulLECancellable.mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
a b : α
ha : MulLECancellable 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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : MulLeftMono α
a b : α
ha : MulLECancellable 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.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
rw : a ≤ a * b ↔ 1 ≤ b
rw₁ rw₂ : 1 ≤ b ↔ 1 ≤ b
⊢ a ≤ b * a ↔ 1 ≤ b

Tactic:
rw [mul_comm', ha.le_mul_iff_one_le_right]

Premises used: mul_comm', MulLECancellable.le_mul_iff_one_le_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : MulOneClass α
inst_2 : IsMulCommutative α
inst_3 : MulLeftMono α
a b : α
ha : MulLECancellable a
rw : a * b ≤ a ↔ b ≤ 1
rw₁ rw₂ : b ≤ 1 ↔ b ≤ 1
⊢ b * a ≤ a ↔ b ≤ 1

Tactic:
rw [mul_comm', ha.mul_le_iff_le_one_right]

Premises used: mul_comm', MulLECancellable.mul_le_iff_le_one_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
c d : α
hcd : a * b * c ≤ a * b * d
rwa : a * b * c ≤ a * (b * d)
rwa₁ rwa₂ rwa₃ rwa₄ : a * b * c ≤ a * b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
rwa [← mul_assoc, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
inst_2 : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
rw : a * (b * c) ≤ a * (b * d)
⊢ a * b * c ≤ a * b * d

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
inst_2 : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
mul_le_mul_right hcd _

Premises used: mul_le_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : Semigroup α
inst_2 : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
exact mul_le_mul_right hcd _

Premises used: mul_le_mul_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : LE α
inst_1 : CommSemigroup α
inst_2 : MulLeftMono α
a b : α
⊢ MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b

Tactic:
⟨fun h ↦ ⟨h.of_mul_left, h.of_mul_right⟩, fun h ↦ h.1.mul h.2⟩

Premises used: MulLECancellable.mul, MulLECancellable.of_mul_right, And.right, And.left, And.intro, Iff.intro, MulLECancellable.of_mul_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
hcov : Covariant M N μ r
hcontra : Contravariant M N μ r
m : M
a b : N
⊢ r (μ m a) (μ m b) ↔ r a b

Tactic:
⟨hcontra m, hcov m⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
inst_1 : ContravariantClass M N μ r
m : M
a b : N
⊢ r (μ m a) (μ m b) ↔ r a b

Tactic:
rel_iff_cov' CovariantClass.elim ContravariantClass.elim

Premises used: CovariantClass.elim, rel_iff_cov', ContravariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
h : Covariant M N μ r
⊢ Covariant M N μ (_root_.flip r)

Tactic:
fun a _ _ ↦ h a

Premises used: Covariant
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
h : Contravariant M N μ r
⊢ Contravariant M N μ (_root_.flip r)

Tactic:
fun a _ _ ↦ h a

Premises used: Contravariant
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
m : M
a b : N
ab : r a b
⊢ r (μ m a) (μ m b)

Tactic:
CovariantClass.elim _ ab

Premises used: CovariantClass.elim
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
⊢ Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r ↔ Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
refine_1 :
  ∀ (h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
    (bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)), r b c
refine_2 :
  ∀ (h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N) (bc : r b c),
    r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r ↔ Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
refine_1 : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r b c

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Tactic:
h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Tactic:
exact h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc

Premises used: inv_mul_cancel_left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)

Tactic:
h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Contravariant N N (fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun (x1 x2 : N) ↦ x1 * x2) a b) ((fun (x1 x2 : N) ↦ x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
M : Type u_1
N : Type u_2
μ : M → N → N
r : N → N → Prop
inst : CovariantClass M N μ r
inst_1 : Group N
inst_2 : CovariantClass N N (fun (x1 x2 : N) ↦ x1 * x2) r
⊢ ContravariantClass N N (fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
⟨Group.covariant_iff_contravariant.mp CovariantClass.elim⟩

Premises used: Group.covariant_iff_contravariant, CovariantClass.elim, ContravariantClass.mk, Iff.mp
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
inst : Group N
inst_1 : LT N
inst_2 : MulLeftStrictMono N
⊢ MulLeftReflectLT N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
⊢ Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r ↔
    Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
refine_1 :
  ∀ (h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N)
    (bc :
      r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
        (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)),
    r b c
refine_2 :
  ∀ (h : Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r) (a b c : N) (bc : r b c),
    r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
      (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r ↔
    Contravariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc :
  r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
    (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)
refine_1 : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r b c

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]

Premises used: mul_inv_cancel_right
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc :
  r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
    (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Tactic:
h a⁻¹ bc

Premises used: Inv.inv
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Goal:
N : Type u_2
r : N → N → Prop
inst : Group N
h : Covariant N N (swap (φ := fun (a a_1 : N) ↦ N) fun (x1 x2 : N) ↦ x1 * x2) r
a b c : N
bc :
  r (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a b)
    (swap (φ := fun (a a_1 : N) ↦ N) (fun (x1 x2 : N) ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)

Tactic:
exact h a⁻¹ bc

Premises used: Inv.inv