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

State before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
x : R
⊢ (idempotent_decomp_AddHom h) ((Ideal.Quotient.mk (Ideal.span {1 - a})) x, (Ideal.Quotient.mk (Ideal.span {a})) x) = x
Tactic:
rw [idempotent_decomp_AddHom_map_quot, ← mul_add, add_sub_cancel, mul_one]
State after:
no goals