Theorem: IMOSL.IMO2011A3.quot_self_comp_idempotent_self_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_self_mul_part h) ⟦x⟧ - x = (1 - a) * -x
Tactic:
rw [mul_neg, ← neg_mul, neg_sub, sub_one_mul, mul_comm]
State after:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_self_mul_part h) ⟦x⟧ - x = x * a - x

State before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_self_mul_part h) ⟦x⟧ - x = x * a - x
Tactic:
rfl
State after:
no goals