awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⊔ Q) : M) * (↑(P ⊔ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁ : ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ 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 : 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 : 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 : M) * (↑R : M) * (↑Pᶜ : M)
rw₅ :
  ((↑P : M) + (↑Pᶜ : M) * (↑Q : M)) * ((↑P : M) + ((↑R : M) - (↑P : M) * (↑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 : M) * (↑R : M) * (↑Pᶜ : M)
rw₇ :
  (↑P : M) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) + (↑Pᶜ : M) * (↑Q : M) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₈ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * (↑R : M)) + (↑Pᶜ : M) * (↑Q : M) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₉ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * (↑R : M)) + (↑Q : M) * (↑Pᶜ : M) * ((↑P : M) + (↑Pᶜ : M) * (↑R : M)) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₀ :
  (↑P : M) * (↑P : M) + (↑P : M) * ((↑Pᶜ : M) * (↑R : M)) +
      ((↑Q : M) * (↑Pᶜ : M) * (↑P : M) + (↑Q : M) * (↑Pᶜ : M) * ((↑Pᶜ : M) * (↑R : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₁ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * (↑R : M) +
      ((↑Q : M) * (↑Pᶜ : M) * (↑P : M) + (↑Q : M) * (↑Pᶜ : M) * ((↑Pᶜ : M) * (↑R : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₂ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * (↑R : M) +
      ((↑Q : M) * ((↑Pᶜ : M) * (↑P : M)) + (↑Q : M) * (↑Pᶜ : M) * ((↑Pᶜ : M) * (↑R : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
rw₁₃ :
  (↑P : M) * (↑P : M) + (↑P : M) * (↑Pᶜ : M) * (↑R : M) +
      ((↑Q : M) * ((↑P : M) * (↑Pᶜ : M)) + (↑Q : M) * (↑Pᶜ : M) * ((↑Pᶜ : M) * (↑R : M))) =
    (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁₄ : (↑P : M) * (↑P : M) + 0 * (↑R : M) + ((↑Q : M) * 0 + (↑Q : M) * (↑Pᶜ : M) * ((↑Pᶜ : M) * (↑R : M))) =
  (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M),
        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (hypothesis)
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 }
⊢ (P ⊔ Q) ⊓ (P ⊔ R) ≤ P ⊔ Q ⊓ R
have e₁ : (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
Tactic: have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
      rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q : M),
        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, zero_mul, mul_zero,
        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw : (↑(P ⊔ Q) : M) * (↑(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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁ : ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]
-- 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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) * (↑(P ⊔ Q ⊓ R) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]