no goals
ι : Type u_2
M : ι → Type u_1
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.240831
inst✝ : Monoid N
i : ι
⊢ Function.Injective ↑of
classical exact (of_leftInverse i).injective
no goals
ι : Type u_2
M : ι → Type u_1
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.240831
inst✝ : Monoid N
i : ι
⊢ Function.Injective ↑of
exact (of_leftInverse i).injective