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
P : { P : M // IsLprojection X P }
⊢ (↑P : M) * (↑Pᶜ : M) = 0
have rw : (↑P : M) * (1 - (↑P : M)) = 0
Tactic: rw [coe_compl, P.prop.proj.mul_one_sub_self]
-- 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
P : { P : M // IsLprojection X P }
rw : (↑P : M) * (1 - (↑P : M)) = 0
⊢ (↑P : M) * (↑Pᶜ : M) = 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [coe_compl, P.prop.proj.mul_one_sub_self]
-- 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 }
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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)
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]
-- 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)
⊢ ((↑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) + (↑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))
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]
-- 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 : { P : M // IsLprojection X P }
⊢ P ≤ P ⊔ Q
have rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
⊢ P ≤ P ⊔ Q
have rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
⊢ P ≤ P ⊔ Q
have rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
⊢ P ≤ P ⊔ Q
have rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]
-- 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 : { P : M // IsLprojection X P }
rw : (↑P : M) = (↑(P ⊓ (P ⊔ Q)) : M)
rw₁ : (↑P : M) = (↑P : M) * (↑(P ⊔ Q) : M)
rw₂ : (↑P : M) = (↑P : M) * ((↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M))
rw₃ : (↑P : M) = (↑P : M) * ((↑P : M) + ((↑Q : M) - (↑P : M) * (↑Q : M)))
⊢ P ≤ P ⊔ Q
have rw₄ : (↑P : M) = (↑P : M) * (↑P : M) + (↑P : M) * ((↑Q : M) - (↑P : M) * (↑Q : M))
Tactic: rw [le_def, coe_inf, coe_sup, ← add_sub, mul_add, mul_sub, ← mul_assoc, P.prop.proj.eq,
      sub_self, add_zero]