-- 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 }
e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw : (↑(P ⊔ Q) : M) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ R) : M) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₂ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) * (↑(P ⊔ Q ⊓ R) : M) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₃ :
  ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₄ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + (↑R : M) - (↑P : M) * (↑R : M)) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + (↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₆ :
  ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M))) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₇ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑R : M))) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₈ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) *
      ((↑P : M) + ((↑(Q ⊓ R) : M) - (↑P : M) * (↑(Q ⊓ R) : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₉ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑(Q ⊓ R) : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₀ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) * ((↑P : M) + (↑(Q ⊓ R) : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₁ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : 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) * (↑Q : 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) * (↑Q : M)) * ((↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₄ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + (↑R : M) * (↑Q : M) * (↑Pᶜ : M)) =
    (↑P : M) + (↑R : M) * (↑Q : M) * (↑Pᶜ : M)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₅ : (↑P : M) + (↑R : M) * (↑Q : M) * (↑Pᶜ : M) = (↑P : M) + (↑R : M) * (↑Q : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
        distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]