Theorem: left_inv_eq_right_inv' (MIL/C07_Hierarchies/S01_Basics.lean)

State before:
M : Type
inst✝ : Monoid₃ M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c
Tactic:
rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]
State after:
no goals