Theorem: l1_1_3_i (AlgebraI/Groups.lean)

State before:
M : Type u_1
A : Type u_2
G : Type u_3
inst✝ : Group G
a b c f : G
h1 : ∀ (g : G), f * g = g
_h2 : ∀ (g : G), g * f = g
⊢ f = 1
Tactic:
rw [← @self_eq_mul_left _ _ _ f, h1]
State after:
no goals