-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)
rw₁₅ rw₁₆ : (↑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)

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]

Premises used: Compl.compl, add_sub, mul_assoc, IsLprojection.commute, Subtype.prop, IsLprojection.distrib_lattice_lemma, IsLprojection.coe_sup, IsLprojection.coe_inf, Commute.eq, Min.min, IsLprojection.compl_mul