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 = 𝟙
hac : a ⋄ c = 𝟙
⊢ b = c
Tactic:
rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]
State after:
no goals