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

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
⊢ MulLECancellable b
Tactic:
intro x y h
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ x ≤ y

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ x ≤ y
Tactic:
apply hab
State after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * b * x ≤ a * b * y

State before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * b * x ≤ a * b * y
Tactic:
rw [mul_assoc, mul_assoc]
State after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * (b * x) ≤ a * (b * y)

State before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * (b * x) ≤ a * (b * y)
Tactic:
exact mul_le_mul_left' h a
State after:
no goals