Theorem: IMOSL.IMO2011A3.quot_compl_comp_idempotent_compl_mul_part (IMOSLLean4/IMO2011/A3/A3.lean)

State before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_compl_mul_part h) ⟦x⟧ - x = a * -x
Tactic:
change x * (1 - a) - x = _
State after:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ x * (1 - a) - x = a * -x

State before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ x * (1 - a) - x = a * -x
Tactic:
rw [mul_one_sub, sub_sub_cancel_left, mul_neg, mul_comm]
State after:
no goals