no goals
M : Type ?u.2741
N : Type ?u.2744
S : Type ?u.2747
M₀ : Type ?u.2750
M₁ : Type ?u.2753
R : Type u_1
G : Type ?u.2759
G₀ : Type ?u.2762
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 : R
h : IsIdempotentElem p
⊢ IsIdempotentElem (1 - p)
rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]