α : Type u_1
β : Type ?u.84683
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c
α : Type u_1
β : Type ?u.84683
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ (fun x x_1 => x * x_1) a b = (fun x x_1 => x * x_1) a c
dsimp
no goals
α : Type u_1
β : Type ?u.84683
inst✝¹ : CommSemigroup α
inst✝ : PartialOrder α
a : α
ha : MulLECancellable a
b c : α
h : (fun x => x * a) b = (fun x => x * a) c
⊢ a * b = a * c
rwa [mul_comm a, mul_comm a]