awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖

Tactic:
abel
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖ ≤
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖

Tactic:
have :=
              add_le_add_left (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
this :
  ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖ ≤
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖
⊢ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖ ≤
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(1 - R) • P • R • x‖

Tactic:
simpa only [mul_smul, sub_smul, one_smul] using this

Premises used: sub_smul, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ ≥ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖

Tactic:
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_iff_le]
            have :=
              add_le_add_left (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
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ ≥ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖
⊢ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖

Tactic:
rw [ge_iff_le] at e1

Premises used: ge_iff_le
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖
⊢ ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖ + 0

Tactic:
nth_rewrite 2 [← add_zero ‖R • x‖] at e1

Premises used: Norm.norm, HSMul.hSMul, add_zero
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : ‖R • x‖ + HSMul.hSMul (α := ℕ) 2 ‖(P * R) • x - (R * P * R) • x‖ ≤ ‖R • x‖ + 0
⊢ 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0

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

Premises used: add_le_add_iff_left, two_smul, two_mul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
rw : ‖(P * R) • x - (R * P * R) • x‖ ≤ 0 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖
⊢ ‖(P * R) • x - (R * P * R) • x‖ = 0

Tactic:
rw [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
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 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖

Tactic:
⟨?_, norm_nonneg _⟩

Premises used: And.intro, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
refine : ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0 ∧ 0 ≤ ‖(P * R) • x - (R * P * R) • x‖

Tactic:
refine ⟨?_, norm_nonneg _⟩
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ HMul.hMul (α := ℝ) 2 0
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
R : M
h₃ : IsLprojection X R
x : X
e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
rwa : ∀ (e1 : 2 * ‖(P * R) • x - (R * P * R) • x‖ ≤ HMul.hMul (α := ℝ) 2 0), ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (e1 : ‖(P * R) • x - (R * P * R) • x‖ ≤ 0), ‖(P * R) • x - (R * P * R) • x‖ ≤ 0
⊢ ‖(P * R) • x - (R * P * R) • x‖ ≤ 0

Tactic:
rwa [← mul_zero (2 : ℝ), mul_le_mul_iff_right₀ (show (0 : ℝ) < 2 by simp)] at e1

Premises used: MulZeroClass.mul_zero, OfNat.ofNat, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
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_iff_le]
            have :=
              add_le_add_left (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_iff_le] 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_iff_right₀ (show (0 : ℝ) < 2 by simp)] at e1

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
⊢ ∀ (R : M), IsLprojection X R → P * R = R * P * R

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_iff_le]
            have :=
              add_le_add_left (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_iff_le] 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_iff_right₀ (show (0 : ℝ) < 2 by simp)] at e1
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw rw₁ : (1 - Q) * P * (1 - Q) = (1 - Q) * P * (1 - Q)
⊢ P * (1 - Q) = (1 - Q) * P * (1 - Q)

Tactic:
rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]

Premises used: IsLprojection.Lcomplement, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ :
  P + -(Q * P) + -(P * Q + -(Q * (P * Q))) = P + -(P * Q) + -(Q * P + -(Q * (P * Q)))
⊢ (1 - Q) * P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q)

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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) = 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
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (e1 : Q * P = Q * P * Q), 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

Premises used: sub_eq_zero, eq_sub_iff_add_eq, add_eq_left
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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

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
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw₁ rw₂ : Q * P * Q = Q * P * Q
⊢ P * Q = Q * P

Tactic:
rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)

Tactic:
⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, ?_⟩

Premises used: IsLprojection.mk, IsLprojection.commute, IsIdempotentElem.mul_of_commute, IsLprojection.proj
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
refine : ∀ (x : X), ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
⊢ IsLprojection X (P * Q)

Tactic:
refine ⟨IsIdempotentElem.mul_of_commute (h₁.commute h₂) h₁.proj h₂.proj, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖
refine_2 : ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖x‖
⊢ ‖x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 rw₁ : ‖x‖ = ‖x‖
⊢ ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖

Tactic:
rw [add_sub_cancel ((P * Q) • x) x]

Premises used: HMul.hMul, add_sub_cancel, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖ + ‖x - (P * Q) • x‖

Tactic:
apply norm_add_le

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖
rw₁ rw₂ : ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖
⊢ ‖(P * Q) • x‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖

Tactic:
rw [sub_smul, one_smul]

Premises used: sub_smul, one_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖ + ‖x - (P * Q) • x‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
⊢ ‖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]

Premises used: HMul.hMul, HSub.hSub, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖)
rw₆ 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‖)

Tactic:
rw [h₂.Lnorm x, h₁.Lnorm (Q • x), sub_smul, one_smul, sub_smul, one_smul, add_assoc]

Premises used: IsLprojection.Lnorm, add_assoc, sub_smul, one_smul, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖ + ‖Q • x - P • Q • x + (x - Q • x)‖

Tactic:
((add_le_add_iff_left ‖P • Q • x‖).mpr (norm_add_le (Q • x - P • Q • x) (x - Q • x)))

Premises used: Iff.mpr, Norm.norm, add_le_add_iff_left, HSub.hSub, norm_add_le, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖
rw₃ 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‖

Tactic:
rw [sub_add_sub_cancel', sub_smul, one_smul, mul_smul]

Premises used: sub_add_sub_cancel', sub_smul, one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖)
Q₂ : ‖P • Q • x‖ + ‖Q • x - P • Q • x + (x - Q • x)‖ = ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖
⊢ ‖(P * Q) • x‖ + ‖(1 - P * Q) • x‖ ≤ ‖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]

Premises used: Iff.mpr, Norm.norm, HMul.hMul, add_le_add_iff_left, HSub.hSub, norm_add_le, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 (1 - (1 - P) * (1 - Q))

Tactic:
(Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement)

Premises used: IsLprojection.Lcomplement, IsLprojection.mul, IsLprojection.Lcomplement_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
h : P + Q - P * Q = 1 - (1 - P) * (1 - Q)
⊢ IsLprojection X (P + Q - P * Q)

Tactic:
convert! (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1

Premises used: IsLprojection.Lcomplement, IsLprojection.mul, IsLprojection.Lcomplement_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
h h₃ h₄ h₅ : P + Q + -(P * Q) = 1 + -(1 + -P + -(Q + -(P * Q)))
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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) = 1 - (↑P : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 ⊓ Q) : M) = (↑P : M) * (↑Q : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 ⊔ Q) : M) = (↑P : M) + (↑Q : M) - (↑P : M) * (↑Q : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 \ Q) : M) = (↑P : M) * (1 - (↑Q : M))

Tactic:
rfl

Premises used: rfl