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

State before:
R : Type u_1
inst✝ : CommRing R
a : R
h : a * a = a
p : (R ⧸ Ideal.span {1 - a}) × R ⧸ Ideal.span {a}
⊢ (Ideal.Quotient.mk (Ideal.span {1 - a})) ((idempotent_decomp_AddHom h) p) = p.1
Tactic:
rw [idempotent_decomp_AddHom, AddMonoidHom.coprod_apply,
  map_add, quot_self_comp_idempotent_self_mul_part,
  quot_self_comp_idempotent_compl_mul_part, add_zero]
State after:
no goals