-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q R : { P : M // IsLprojection X P }
rw :
  (↑P : M) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) +
      (↑Pᶜ : M) * (↑R : M) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M)) +
      (↑Pᶜ : M) * (↑R : M) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₂ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M)) +
      ((↑Pᶜ : M) * (↑R : M) * (↑P : M) + (↑Pᶜ : M) * (↑R : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₃ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M)) +
      ((↑Pᶜ : M) * (↑R : M) * (↑P : M) + (↑Pᶜ : M) * ((↑R : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M)))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₄ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) * (↑R : M) * (↑Pᶜ : M)) +
      ((↑Pᶜ : M) * (↑R : M) * (↑P : M) + (↑Pᶜ : M) * ((↑R : M) * ((↑Q : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑(Q ⊓ R) : M) * (↑Pᶜ : M)) +
      ((↑Pᶜ : M) * (↑R : M) * (↑P : M) + (↑Pᶜ : M) * ((↑R : M) * (↑(Q ⊓ R) : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)
rw₆ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑(Q ⊓ R) : M) * (↑Pᶜ : M)) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑R : M) * (↑(Q ⊓ R) : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)
rw₇ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * (↑(Q ⊓ R) : M)) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑R : M) * (↑(Q ⊓ R) : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)
rw₈ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * (↑(Q ⊓ R) : M)) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑(Q ⊓ R) : M) * (↑R : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)
rw₉ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * ((↑Q : M) * (↑R : M))) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M) * (↑R : M) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₀ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * ((↑Q : M) * (↑R : M))) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₁ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * ((↑Q : M) * (↑R : M)) +
      ((↑R : M) * (↑Pᶜ : M) * (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₂ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * ((↑Q : M) * (↑R : M)) +
      ((↑R : M) * ((↑Pᶜ : M) * (↑P : M)) + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₃ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * ((↑Q : M) * (↑R : M)) +
      ((↑R : M) * ((↑P : M) * (↑Pᶜ : M)) + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₄ :
  (↑P : M) * (↑P : M) + 0 * ((↑Q : M) * (↑R : M)) +
      ((↑R : M) * 0 + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
rw₁₅ :
  (↑P : M) * (↑P : M) + 0 + ((↑R : M) * 0 + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
    (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
⊢ ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₆ : (↑P : M) * (↑P : M) + 0 + (0 + (↑Pᶜ : M) * ((↑Q : M) * ((↑R : M) * (↑R : M)) * (↑Pᶜ : M))) =
  (↑P : M) + (↑Pᶜ : M) * ((↑Q : M) * (↑R : M))
Tactic: 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,
    zero_mul, 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]