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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ P * (1 - Q) = (1 - Q) * P * (1 - Q)
have rw : (1 - Q) * P * (1 - Q) = (1 - Q) * P * (1 - Q)
Tactic: rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ (1 - Q) * P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
have noncomm_ring : P + -(Q * P) + -(P * Q + -(Q * (P * Q))) = P + -(P * Q) + -(Q * P + -(Q * (P * Q)))
Tactic: noncomm_ring
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Q * P = Q * P * Q
have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
Tactic: have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
      calc
        P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
        _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
⊢ Q * P = Q * P * Q
have rwa : ∀ (e1 : P * (1 - Q) + (Q * P - Q * P * Q) = P * (1 - Q)), Q * P = Q * P * Q
Tactic: rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
Cleared hypotheses: e1
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
rwa : ∀ (e1 : P * (1 - Q) + (Q * P - Q * P * Q) = P * (1 - Q)), Q * P = Q * P * Q
⊢ Q * P = Q * P * Q
have rwa₁ : ∀ (e1 : Q * P - Q * P * Q = 0), Q * P = Q * P * Q
Tactic: rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
Cleared hypotheses: e1
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)
rwa : ∀ (e1 : P * (1 - Q) + (Q * P - Q * P * Q) = P * (1 - Q)), Q * P = Q * P * Q
rwa₁ : ∀ (e1 : Q * P - Q * P * Q = 0), Q * P = Q * P * Q
⊢ Q * P = Q * P * Q
have rwa₂ : ∀ (e1 : Q * P = Q * P * Q), Q * P = Q * P * Q
Tactic: rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
Cleared hypotheses: e1
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
⊢ Commute P Q
have QP_eq_QPQ : Q * P = Q * P * Q
Tactic: have QP_eq_QPQ : Q * P = Q * P * Q := by
    have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
      calc
        P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
        _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
    rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
⊢ P * Q = Q * P
have rw : P * Q = Q * P * Q
Tactic: rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
PR_eq_RPR : ∀ (R : M), IsLprojection X R → P * R = R * P * R
QP_eq_QPQ : Q * P = Q * P * Q
rw : P * Q = Q * P * Q
⊢ P * Q = Q * P
have rw₁ : Q * P * Q = Q * P * Q
Tactic: rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P * Q)
have refine : ∀ (x : X), ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
Tactic: refine ⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, ?_⟩
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have refine_1 : ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
Tactic: refine le_antisymm ?_ ?_
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
refine_1 : ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
⊢ ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have refine_2 : ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
Tactic: refine le_antisymm ?_ ?_
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
have rw : ‖x‖ = ‖x‖
Tactic: rw [add_sub_cancel ((P * Q) • x) x]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw : ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - (P * Q) • x‖
Tactic: rw [sub_smul, one_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - (P * Q) • x‖
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw₁ : ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
Tactic: rw [sub_smul, one_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have x₁ : ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
Tactic: calc
      ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel ((P * Q) • x) x]
      _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
x₁ : ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
⊢ ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have x₂ : ‖(P * Q) • x + (x - (P * Q) • x)‖ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
Tactic: calc
      ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel ((P * Q) • x) x]
      _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
x₁ : ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖
x₂ : ‖(P * Q) • x + (x - (P * Q) • x)‖ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
⊢ ‖x‖ ≤ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have x₃ : ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
Tactic: calc
      ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖ := by rw [add_sub_cancel ((P * Q) • x) x]
      _ ≤ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ := by apply norm_add_le
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by rw [sub_smul, one_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₂ : ‖P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (Q • x) - P • Q • x‖ + ‖(1 - Q) • x‖ =
  ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₂ :
  ‖P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (Q • x) - P • Q • x‖ + ‖(1 - Q) • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₃ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₂ :
  ‖P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (Q • x) - P • Q • x‖ + ‖(1 - Q) • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₃ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₄ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - Q • x‖ =
  ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₂ :
  ‖P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (Q • x) - P • Q • x‖ + ‖(1 - Q) • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₃ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₄ :
  ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - Q • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₅ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖x - Q • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₁ : ‖P • Q • x‖ + ‖(1 - P) • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₂ :
  ‖P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (Q • x) - P • Q • x‖ + ‖(1 - Q) • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₃ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖(1 - Q) • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₄ :
  ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - Q • x‖ =
    ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
rw₅ : ‖P • Q • x‖ + ‖Q • x - P • Q • x‖ + ‖x - Q • x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
have rw₆ : ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
Tactic: rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw₁ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - (P * Q) • x‖
Tactic: rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
rw₁ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - (P * Q) • x‖
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw₂ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
Tactic: rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
rw : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
rw₁ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 x - (P * Q) • x‖
rw₂ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
⊢ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
have rw₃ : ‖P • Q • x‖ + ‖x - P • Q • x‖ = ‖P • Q • x‖ + ‖x - P • Q • x‖
Tactic: rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
have Q₁ : ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
Tactic: calc
      ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
        rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
      _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
        ((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by
        rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
Q₁ : ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖)
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
have Q₂ : ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
Tactic: calc
      ‖x‖ = ‖P • Q • x‖ + (‖Q • x - P • Q • x‖ + ‖x - Q • x‖) := by
        rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]
      _ ≥ ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ :=
        ((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))
      _ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ := by
        rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)
have h : P + Q - P * Q = 1 - (1 - P) * (1 - Q)
Tactic: convert! (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1
-- 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 : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)
have h : P + Q + -(P * Q) = 1 + -(1 + -P + -(Q + -(P * Q)))
Tactic: noncomm_ring
-- 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 }
h₁ : (↑P : M) = (↑(P ⊓ Q) : M)
h₂ : (↑Q : M) = (↑(Q ⊓ R) : M)
⊢ (↑P : M) = (↑(P ⊓ R) : M)
have simp : (↑P : M) = (↑P : M) * (↑R : M)
Tactic: simp only [coe_inf] at h₁ h₂ ⊢
-- 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 }
h₁ : (↑P : M) = (↑P : M) * (↑Q : M)
h₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
⊢ (↑P : M) = (↑P : M) * (↑R : M)
have rw : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑R : M)
Tactic: rw [h₁, mul_assoc, ← h₂]
-- 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 }
h₁ : (↑P : M) = (↑P : M) * (↑Q : M)
h₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
rw : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑R : M)
⊢ (↑P : M) = (↑P : M) * (↑R : M)
have rw₁ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑R : M))
Tactic: rw [h₁, mul_assoc, ← h₂]
-- 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 }
h₁ : (↑P : M) = (↑P : M) * (↑Q : M)
h₂ : (↑Q : M) = (↑Q : M) * (↑R : M)
rw : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M) * (↑R : M)
rw₁ : (↑P : M) * (↑Q : M) = (↑P : M) * ((↑Q : M) * (↑R : M))
⊢ (↑P : M) = (↑P : M) * (↑R : M)
have rw₂ : (↑P : M) * (↑Q : M) = (↑P : M) * (↑Q : M)
Tactic: rw [h₁, mul_assoc, ← h₂]
-- 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
⊢ IsIdempotentElem.{u_2} (M := M) 0
have rw : HMul.hMul (α := M) 0 0 = 0
Tactic: rw [IsIdempotentElem, zero_mul]
-- 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
rw : HMul.hMul (α := M) 0 0 = 0
⊢ IsIdempotentElem.{u_2} (M := M) 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [IsIdempotentElem, zero_mul]
-- 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 }
Q : M
⊢ (↑Pᶜ : M) * Q = Q - (↑P : M) * Q
have rw : (1 - (↑P : M)) * Q = Q - (↑P : M) * Q
Tactic: rw [coe_compl, sub_mul, one_mul]
-- 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 }
Q : M
rw : (1 - (↑P : M)) * Q = Q - (↑P : M) * Q
⊢ (↑Pᶜ : M) * Q = Q - (↑P : M) * Q
have rw₁ : 1 * Q - (↑P : M) * Q = Q - (↑P : M) * Q
Tactic: rw [coe_compl, sub_mul, one_mul]
-- 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 }
Q : M
rw : (1 - (↑P : M)) * Q = Q - (↑P : M) * Q
rw₁ : 1 * Q - (↑P : M) * Q = Q - (↑P : M) * Q
⊢ (↑Pᶜ : M) * Q = Q - (↑P : M) * Q
have rw₂ : Q - (↑P : M) * Q = Q - (↑P : M) * Q
Tactic: rw [coe_compl, sub_mul, one_mul]