Theorem: MulLECancellable.hMul (ExponentialRamsey/Prereq/Mathlib/Algebra/Order/Monoid/Lemmas.lean)

State before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
⊢ MulLECancellable (a * b)
Tactic:
intro x y h
State after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * b * x ≤ a * b * y
⊢ x ≤ y

State before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * b * x ≤ a * b * y
⊢ x ≤ y
Tactic:
rw [mul_assoc, mul_assoc] at h
State after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * (b * x) ≤ a * (b * y)
⊢ x ≤ y

State before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * (b * x) ≤ a * (b * y)
⊢ x ≤ y
Tactic:
exact hb (ha h)
State after:
no goals