no goals
X : Type u_2
inst✝³ : NormedAddCommGroup X
M : Type u_1
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑(Pᶜ) * ↑R) * (↑P + ↑Q * ↑R * ↑(Pᶜ)) = ↑P + ↑Q * ↑R * ↑(Pᶜ)
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑(Pᶜ))),
  ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq,
  ((Q ⊓ R).prop.commute (Pᶜ).prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
  mul_assoc (Q : M), ←mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
  MulZeroClass.zero_mul, MulZeroClass.mul_zero, zero_add, add_zero, ← mul_assoc, P.prop.proj.eq,
  R.prop.proj.eq, ←coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute (Pᶜ).prop).eq, ← mul_assoc,
  Pᶜ.prop.proj.eq]