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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have rw₁ : ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)) * (↑(P ⊔ 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ 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 : 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ 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 : 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ 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 : 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ 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 : 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ 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 : 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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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 (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)
⊢ (↑((P ⊔ Q) ⊓ (P ⊔ R)) : M) = (↑P : M) + (↑Q : M) * (↑R : M) * (↑Pᶜ : M)
have 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)
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]