α : Type u_1
inst✝ : CommMonoid α
a b c : α
⊢ Finite a (c * b) → Finite a c
α : Type u_1
inst✝ : CommMonoid α
a b c : α
⊢ Finite a (b * c) → Finite a c
rw [mul_comm]
no goals
α : Type u_1
inst✝ : CommMonoid α
a b c : α
⊢ Finite a (c * b) → Finite a c
exact finite_of_finite_mul_right