-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem commute [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) :
    Commute P Q

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Tactic:
rw [GE.ge] at e1

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : 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

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

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : 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

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ Commute P Q

Tactic:
have PR_eq_RPR : ∀ R : M, IsLprojection X R → P * R = R * P * R := fun R h₃ => by
  refine @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
    rw [← norm_sub_eq_zero_iff]
    have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
      calc
        ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
            (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) := by
          rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
            mul_smul]
        _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
            (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) := by
          rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
        _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
            (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
          rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
        _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
        _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ := by
          rw [GE.ge]
          have :=
            add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
          simpa only [mul_smul, sub_smul, one_smul] using this
    rw [GE.ge] at e1
    nth_rewrite 2 [← add_zero ‖R • x‖] at e1
    rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
    rw [le_antisymm_iff]
    refine ⟨?_, norm_nonneg _⟩
    rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : 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

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 2 * 0
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
have :=
  add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
this : ‖R • x‖ + 2 • ‖(1 - R) • P • R • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖ + 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Tactic:
rw [add_le_add_iff_left, two_smul, ← two_mul] at e1

Result:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0

Tactic:
rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
⊢ P * R = R * P * R

Tactic:
refine @eq_of_smul_eq_smul _ X _ _ _ _ fun x => by
  rw [← norm_sub_eq_zero_iff]
  have e1 : ‖R • x‖ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ :=
    calc
      ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
          (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) := by
        rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
          mul_smul]
      _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
          (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖) := by
        rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]
      _ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
          (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) := by
        rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]
      _ = ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖ := by abel
      _ ≥ ‖R • x‖ + 2 • ‖(P * R) • x - (R * P * R) • x‖ := by
        rw [GE.ge]
        have :=
          add_le_add_right (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
        simpa only [mul_smul, sub_smul, one_smul] using this
  rw [GE.ge] at e1
  nth_rewrite 2 [← add_zero ‖R • x‖] at e1
  rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
  rw [le_antisymm_iff]
  refine ⟨?_, norm_nonneg _⟩
  rwa [← mul_zero (2 : ℝ), mul_le_mul_left (show (0 : ℝ) < 2 by norm_num)] at e1

Result:
no goals