awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c d : α
h : a * b < c
hle : d ≤ a
⊢ d * b < c

Tactic:
(mul_le_mul_left hle b).trans_lt h

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

Tactic:
(mul_le_mul_left hle b).trans h

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

Tactic:
h.trans_le (mul_le_mul_right hle b)

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

Tactic:
@rel_act_of_rel_of_rel_act _ _ _ (· ≤ ·) _ _ b _ _ _ hle h

Premises used: rel_act_of_rel_of_rel_act
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulRightMono α
a b c d : α
h : a < b * c
hle : b ≤ d
⊢ a < d * c

Tactic:
h.trans_le (mul_le_mul_left hle c)

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

Tactic:
h.trans (mul_le_mul_left hle c)

Premises used: mul_le_mul_left, LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ MulLeftMono α

Tactic:
haveI := mulLeftMono_of_mulLeftStrictMono α
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this : MulLeftMono α
⊢ MulRightMono α

Tactic:
haveI := mulRightMono_of_mulRightStrictMono α
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ b₁ : α
this_1 : MulLeftMono α
this : MulRightMono α
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁ * b₁ ≤ a₁ * b₁

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
refine : ∀ (h : a₂ * b₂ ≤ a₁ * b₁), a₁ = a₂ ∧ b₁ = b₂
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [eq_iff_le_not_lt, ha, hb, true_and]

Premises used: eq_iff_le_not_lt, true_and
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩

Premises used: LE.le.not_gt, And.intro
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
refine_1 : ∀ (ha : a₁ < a₂), a₁ * b₁ < a₂ * b₂
refine_2 : ∀ (hb : b₁ < b₂), a₁ * b₁ < a₂ * b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂

Tactic:
refine ⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
mul_lt_mul_of_lt_of_le ha hb

Premises used: mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb_1 : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
mul_lt_mul_of_le_of_lt ha hb

Premises used: mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha_1 : a₁ ≤ a₂
hb : b₁ ≤ b₂
this_1 : MulLeftMono α
this : MulRightMono α
h : a₂ * b₂ ≤ a₁ * b₁
ha : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exacts [mul_lt_mul_of_lt_of_le ha hb, mul_lt_mul_of_le_of_lt ha hb]

Premises used: mul_lt_mul_of_le_of_lt, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ MulLeftMono α

Tactic:
haveI := mulLeftMono_of_mulLeftStrictMono α
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this : MulLeftMono α
⊢ MulRightMono α

Tactic:
haveI := mulRightMono_of_mulRightStrictMono α
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this_1 : MulLeftMono α
this : MulRightMono α
rw : a * b ≤ c * d ∧ c * d ≤ a * b ↔ a = c ∧ b = d
rw₁ : True ∧ c * d ≤ a * b ↔ a = c ∧ b = d
rw₂ : c * d ≤ a * b ↔ a = c ∧ b = d
rw₃ rw₄ : a = c ∧ b = d ↔ a = c ∧ b = d
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

Premises used: mul_le_mul_iff_of_ge, le_antisymm_iff, eq_true, mul_le_mul', true_and
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ c * a = b * a ↔ c = b

Tactic:
⟨fun h' => ?_, (· ▸ rfl)⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
refine : ∀ (h' : c * a = b * a), c = b
⊢ c * a = b * a ↔ c = b

Tactic:
refine ⟨fun h' => ?_, (· ▸ rfl)⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : c * a = b * a
contrapose : ∀ (h' : ¬c = b), ¬c * a = b * a
⊢ c = b

Tactic:
contrapose h'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
inl : ∀ (h : b ≤ c), ¬c * a = b * a
inr : ∀ (h : c ≤ b), ¬c * a = b * a
⊢ ¬c * a = b * a

Tactic:
obtain h | h := h
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

Tactic:
mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'

Premises used: LT.lt.ne', mul_lt_mul_left, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'

Premises used: LT.lt.ne', mul_lt_mul_left, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
mul_lt_mul_left (h.lt_of_ne h') a |>.ne

Premises used: LE.le.lt_of_ne, mul_lt_mul_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_left (h.lt_of_ne h') a |>.ne

Premises used: LE.le.lt_of_ne, mul_lt_mul_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ a * c = a * b ↔ c = b

Tactic:
⟨fun h' => ?_, (· ▸ rfl)⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
refine : ∀ (h' : a * c = a * b), c = b
⊢ a * c = a * b ↔ c = b

Tactic:
refine ⟨fun h' => ?_, (· ▸ rfl)⟩
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : a * c = a * b
contrapose : ∀ (h' : ¬c = b), ¬a * c = a * b
⊢ c = b

Tactic:
contrapose h'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
inl : ∀ (h : b ≤ c), ¬a * c = a * b
inr : ∀ (h : c ≤ b), ¬a * c = a * b
⊢ ¬a * c = a * b

Tactic:
obtain h | h := h
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

Tactic:
mul_lt_mul_right (h.lt_of_ne' h') a |>.ne'

Premises used: mul_lt_mul_right, LT.lt.ne', LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

Tactic:
exact mul_lt_mul_right (h.lt_of_ne' h') a |>.ne'

Premises used: mul_lt_mul_right, LT.lt.ne', LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
mul_lt_mul_right (h.lt_of_ne h') a |>.ne

Premises used: mul_lt_mul_right, LE.le.lt_of_ne, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
exact mul_lt_mul_right (h.lt_of_ne h') a |>.ne

Premises used: mul_lt_mul_right, LE.le.lt_of_ne, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
inl : ∀ (hac : a < c), a = c ∧ b = d ∨ a < c ∨ b < d
inr : ∀ (h : a * b = a * d), a = a ∧ b = d ∨ a < a ∨ b < d
inr₁ : ∀ (hca : c < a), a = c ∧ b = d ∨ a < c ∨ b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
obtain hac | rfl | hca := lt_trichotomy a c

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hac : a < c
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = a * d
inr : a = a ∧ b = d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d

Tactic:
left
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d

Tactic:
simpa using mul_right_inj_of_comparable (le_total d b) |>.1 h

Premises used: le_total, Iff.mp, mul_right_inj_of_comparable
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
inr : ∀ (hbd : b < d), a = c ∧ b = d ∨ a < c ∨ b < d
inr₁ : ∀ (h : a * b = c * b), a = c ∧ b = b ∨ a < c ∨ b < b
inr₂ : ∀ (hdb : d < b), a = c ∧ b = d ∨ a < c ∨ b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
obtain hbd | rfl | hdb := lt_trichotomy b d

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hbd : b < d
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

Tactic:
False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm

Premises used: False.elim, mul_lt_mul_left, Eq.symm, ne_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
hca : c < a
h : a * b = c * b
⊢ a = c ∧ b = b ∨ a < c ∨ b < b

Tactic:
exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm

Premises used: False.elim, mul_lt_mul_left, Eq.symm, ne_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

Premises used: False.elim, mul_lt_mul_of_lt_of_lt, Eq.symm, ne_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

Premises used: False.elim, mul_lt_mul_of_lt_of_lt, Eq.symm, ne_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c : α
⊢ a * max b c = max (a * b) (a * c)

Tactic:
mul_right_mono.map_max

Premises used: mul_right_mono, Monotone.map_max
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b c : α
⊢ max a b * c = max (a * c) (b * c)

Tactic:
mul_left_mono.map_max

Premises used: Monotone.map_max, mul_left_mono
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c : α
⊢ a * min b c = min (a * b) (a * c)

Tactic:
mul_right_mono.map_min

Premises used: mul_right_mono, Monotone.map_min
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b c : α
⊢ min a b * c = min (a * c) (b * c)

Tactic:
mul_left_mono.map_min

Premises used: mul_left_mono, Monotone.map_min
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
h : a * b < c * d
simp_rw : (a < c ∨ a < d) ∨ b < c ∨ b < d
⊢ min a b < max c d

Tactic:
simp_rw [min_lt_iff, lt_max_iff]

Premises used: min_lt_iff, lt_max_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
h : a * b < c * d
contrapose! : ∀ (h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b), c * d ≤ a * b
⊢ (a < c ∨ a < d) ∨ b < c ∨ b < d

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b
⊢ c * d ≤ a * b

Tactic:
mul_le_mul' h.1.1 h.2.2

Premises used: And.right, And.left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b
⊢ c * d ≤ a * b

Tactic:
exact mul_le_mul' h.1.1 h.2.2

Premises used: And.right, And.left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
h : a * b ≤ c * d
simp_rw : (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
⊢ min a b ≤ max c d

Tactic:
simp_rw [min_le_iff, le_max_iff]

Premises used: min_le_iff, le_max_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
h : a * b ≤ c * d
contrapose! : ∀ (h : (c < a ∧ d < a) ∧ c < b ∧ d < b), c * d < a * b
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

Premises used: LT.lt.le, And.right, And.left, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

Premises used: LT.lt.le, And.right, And.left, mul_lt_mul_of_le_of_lt
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : a * b ≤ c * d
simp_rw : (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
⊢ min a b ≤ max c d

Tactic:
simp_rw [min_le_iff, le_max_iff]

Premises used: min_le_iff, le_max_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : a * b ≤ c * d
contrapose! : ∀ (h : (c < a ∧ d < a) ∧ c < b ∧ d < b), c * d < a * b
⊢ (a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

Premises used: LT.lt.le, And.right, And.left, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftMono α
inst_3 : MulRightStrictMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
exact mul_lt_mul_of_lt_of_le h.1.1 h.2.2.le

Premises used: LT.lt.le, And.right, And.left, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
a b c d : α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
h : a * b ≤ c * d
⊢ min a b ≤ max c d

Tactic:
haveI := mulRightMono_of_mulRightStrictMono α
  Left.min_le_max_of_mul_le_mul h

Premises used: Left.min_le_max_of_mul_le_mul
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d : α
⊢ max (a * b) (c * d) ≤ max a c * max b d

Tactic:
max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <|
    mul_le_mul' (le_max_right _ _) <| le_max_right _ _

Premises used: le_max_right, max_le, le_max_left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : Mul α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d : α
⊢ min a c * min b d ≤ min (a * b) (c * d)

Tactic:
le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <|
    mul_le_mul' (min_le_right _ _) <| min_le_right _ _

Premises used: le_min, min_le_left, min_le_right, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Goal:
α : Type u_1
inst : MulOneClass α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
h : 1 ≤ b
⊢ a ≤ a * b

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

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 : LE α
inst_2 : MulLeftMono α
a b : α
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
calc
    a * b ≤ a * 1 := mul_le_mul_right h a
    _ = a := mul_one a

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 : LE α
inst_2 : MulRightMono α
a b : α
h : 1 ≤ b
⊢ a ≤ b * a

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

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 : LE α
inst_2 : MulRightMono α
a b : α
h : b ≤ 1
⊢ b * a ≤ a

Tactic:
calc
    b * a ≤ 1 * a := mul_le_mul_left h a
    _ = a := one_mul a

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 : LE α
inst_2 : MulLeftReflectLE α
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 : LE α
inst_2 : MulLeftReflectLE α
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 : LE α
inst_2 : MulRightReflectLE α
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 : LE α
inst_2 : MulRightReflectLE α
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 : LE α
inst_2 : MulLeftMono α
inst_3 : MulLeftReflectLE α
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 : LE α
inst_2 : MulRightMono α
inst_3 : MulRightReflectLE α
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 : LE α
inst_2 : MulLeftMono α
inst_3 : MulLeftReflectLE α
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 : LE α
inst_2 : MulRightMono α
inst_3 : MulRightReflectLE α
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