M : Type ?u.12099
N : Type ?u.12102
S : Type ?u.12105
M₀ : Type ?u.12108
M₁ : Type ?u.12111
R : Type ?u.12114
G : Type ?u.12117
G₀ : Type u_1
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : G₀
h : IsIdempotentElem p
hp : ¬p = 0
⊢ p = 1
M : Type ?u.12099
N : Type ?u.12102
S : Type ?u.12105
M₀ : Type ?u.12108
M₁ : Type ?u.12111
R : Type ?u.12114
G : Type ?u.12117
G₀ : Type u_1
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : G₀
⊢ IsIdempotentElem p ↔ p = 0 ∨ p = 1
refine'
  Iff.intro (fun h => or_iff_not_imp_left.mpr fun hp => _) fun h =>
    h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one
no goals
M : Type ?u.12099
N : Type ?u.12102
S : Type ?u.12105
M₀ : Type ?u.12108
M₁ : Type ?u.12111
R : Type ?u.12114
G : Type ?u.12117
G₀ : Type u_1
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : G₀
h : IsIdempotentElem p
hp : ¬p = 0
⊢ p = 1
exact mul_left_cancel₀ hp (h.trans (mul_one p).symm)