[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
[PROOFSTEP]
repeat'
  ring_nf
  simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
    sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero,
    sub_eq_add_neg, A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) -
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    0
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ -4 + (A₀ * B₀ ^ 2 * A₁ * 2 - A₀ * B₁ ^ 2 * A₁ * 2) + A₀ ^ 2 * B₀ * B₁ * 2 + A₀ ^ 2 * B₀ ^ 2 +
          (A₀ ^ 2 * B₁ ^ 2 - B₀ * B₁ * A₁ ^ 2 * 2) +
        B₀ ^ 2 * A₁ ^ 2 +
      B₁ ^ 2 * A₁ ^ 2 =
    0
[PROOFSTEP]
simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
  sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero, sub_eq_add_neg,
  A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ -4 + (B₀ * B₁ * 2 + (1 ^ 2 + (1 ^ 2 + (-(B₀ * B₁ * 2) + (1 ^ 2 + 1 ^ 2))))) = 0
[PROOFSTEP]
ring_nf
[GOAL]

[PROOFSTEP]
simp only [A₁_inv, B₁_inv, sub_eq_add_neg, add_mul, mul_add, sub_mul, mul_sub, add_assoc, neg_add, neg_sub, sub_add,
  sub_sub, neg_mul, ← sq, A₀_inv, B₀_inv, ← sq, ← mul_assoc, one_mul, mul_one, add_right_neg, add_zero, sub_eq_add_neg,
  A₀_inv, mul_one, add_right_neg, zero_mul]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
let P := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
have i₁ : 0 ≤ P := by
  have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
  have idem' : P = (1 / 4 : ℝ) • (P * P) :=
    by
    have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
    rw [idem, h, ← mul_smul]
    norm_num
  have sa : star P = P := by
    dsimp
    simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
      mul_comm B₁]
  rw [idem']
  conv_rhs =>
    arg 2
    arg 1
    rw [← sa]
  convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg P) _
  · simp
  · norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ 0 ≤ P
[PROOFSTEP]
have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 0 ≤ P
[PROOFSTEP]
have idem' : P = (1 / 4 : ℝ) • (P * P) :=
  by
  have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
  rw [idem, h, ← mul_smul]
  norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ P = (1 / 4) • (P * P)
[PROOFSTEP]
have h : 4 * P = (4 : ℝ) • P := by simp [Algebra.smul_def]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
⊢ 4 * P = 4 • P
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4) • (P * P)
[PROOFSTEP]
rw [idem, h, ← mul_smul]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4 * 4) • P
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ 0 ≤ P
[PROOFSTEP]
have sa : star P = P := by
  dsimp
  simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
    mul_comm B₁]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star P = P
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
⊢ star (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
[PROOFSTEP]
simp only [star_add, star_sub, star_mul, star_ofNat, star_one, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa, mul_comm B₀,
  mul_comm B₁]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ P
[PROOFSTEP]
rw [idem']
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ (1 / 4) • (P * P)
[PROOFSTEP]
conv_rhs =>
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
  arg 2
  arg 1
  rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| (1 / 4) • (P * P)
[PROOFSTEP]
arg 2
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| P * P
[PROOFSTEP]
arg 1
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
| P
[PROOFSTEP]
rw [← sa]
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ (1 / 4) • (star P * P)
[PROOFSTEP]
convert smul_le_smul_of_nonneg (R := ℝ) (star_mul_self_nonneg P) _
[GOAL]
case h.e'_3
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 = (1 / 4) • 0
[PROOFSTEP]
simp
[GOAL]
case convert_2
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ 1 / 4
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
i₁ : 0 ≤ P
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
[PROOFSTEP]
apply le_of_sub_nonneg
[GOAL]
case a
R : Type u
inst✝³ : OrderedCommRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : OrderedSMul ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
i₁ : 0 ≤ P
⊢ 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
[PROOFSTEP]
simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁
[GOAL]
R : Type u
⊢ Real.sqrt 2 * Real.sqrt 2 ^ 3 = Real.sqrt 2 * (2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹))
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 * (Real.sqrt 2)⁻¹ * 4
[PROOFSTEP]
rw [mul_inv_cancel (ne_of_gt (Real.sqrt_pos.2 (show (2 : ℝ) > 0 by norm_num)))]
[GOAL]
R : Type u
⊢ 2 > 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
⊢ Real.sqrt 2 ^ 4 = 1 * 4
[PROOFSTEP]
convert congr_arg (· ^ 2) (@Real.sq_sqrt 2 (by norm_num)) using 1
[GOAL]
R : Type u
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = (Real.sqrt 2 ^ 2) ^ 2
[PROOFSTEP]
try simp only [← pow_mul]
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = (Real.sqrt 2 ^ 2) ^ 2
[PROOFSTEP]
simp only [← pow_mul]
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
try simp only [← pow_mul]
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
simp only [← pow_mul]
[GOAL]
case h.e'_2
R : Type u
⊢ Real.sqrt 2 ^ 4 = Real.sqrt 2 ^ (2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
R : Type u
⊢ 1 * 4 = 2 ^ 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
⊢ (Real.sqrt 2)⁻¹ * (Real.sqrt 2)⁻¹ = 2⁻¹
[PROOFSTEP]
rw [← mul_inv]
[GOAL]
R : Type u
⊢ (Real.sqrt 2 * Real.sqrt 2)⁻¹ = 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
  rw [zsmul_eq_smul_cast ℝ, ← mul_smul]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
m : ℤ
a : ℝ
x : R
⊢ m • a • x = (↑m * a) • x
[PROOFSTEP]
rw [zsmul_eq_smul_cast ℝ, ← mul_smul]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
let P := √2⁻¹ • (A₁ + A₀) - B₀
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
let Q := √2⁻¹ • (A₁ - A₀) + B₁
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = √2⁻¹ • (P ^ 2 + Q ^ 2) :=
  by
  dsimp
    -- distribute out all the powers and products appearing on the RHS
  simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
    -- pull all coefficients out to the front, and combine `√2`s where possible
  simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
    -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
  simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
    -- move Aᵢ to the left of Bᵢ
  simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
    -- collect terms, simplify coefficients, and collect terms again:
  abel_nf
    -- all terms coincide, but the last one. Simplify all other terms
  simp only [M]
  simp only [neg_mul, one_mul, mul_inv_cancel_of_invertible, Int.cast_one, add_assoc, add_comm, add_left_comm, one_smul,
    Int.cast_neg, neg_smul, Int.int_cast_ofNat]
  simp only [← add_assoc, ← add_smul]
    -- just look at the coefficients now:
  congr
  exact mul_left_cancel₀ (by norm_num) tsirelson_inequality_aux
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
dsimp
  -- distribute out all the powers and products appearing on the RHS
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (Real.sqrt 2)⁻¹ • (((Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀) ^ 2 + ((Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁) ^ 2)
[PROOFSTEP]
simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
  -- pull all coefficients out to the front, and combine `√2`s where possible
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₁) +
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₁) -
            (Real.sqrt 2)⁻¹ • (B₀ * (Real.sqrt 2)⁻¹ • A₁) +
          ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₀) +
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₀) -
            (Real.sqrt 2)⁻¹ • (B₀ * (Real.sqrt 2)⁻¹ • A₀)) -
        ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * B₀) + (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * B₀) -
          (Real.sqrt 2)⁻¹ • (B₀ * B₀)) +
      ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₁) -
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₁) +
            (Real.sqrt 2)⁻¹ • (B₁ * (Real.sqrt 2)⁻¹ • A₁) -
          ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * (Real.sqrt 2)⁻¹ • A₀) -
              (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * (Real.sqrt 2)⁻¹ • A₀) +
            (Real.sqrt 2)⁻¹ • (B₁ * (Real.sqrt 2)⁻¹ • A₀)) +
        ((Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₁ * B₁) - (Real.sqrt 2)⁻¹ • ((Real.sqrt 2)⁻¹ • A₀ * B₁) +
          (Real.sqrt 2)⁻¹ • (B₁ * B₁)))
[PROOFSTEP]
simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
  -- replace Aᵢ * Aᵢ = 1 and Bᵢ * Bᵢ = 1
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₀) - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • (B₀ * B₀)) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₀) + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • (B₁ * B₁)))
[PROOFSTEP]
simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
  -- move Aᵢ to the left of Bᵢ
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • 1) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • 1))
[PROOFSTEP]
simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
  -- collect terms, simplify coefficients, and collect terms again:
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (A₁ * B₀) +
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (A₀ * B₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (Real.sqrt 2)⁻¹ • 1) +
      (((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 - ((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (A₁ * B₁) -
          (((Real.sqrt 2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (A₀ * B₁)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (Real.sqrt 2)⁻¹ • 1))
[PROOFSTEP]
abel_nf
  -- all terms coincide, but the last one. Simplify all other terms
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    4 • ((Real.sqrt 2)⁻¹ * 2⁻¹) • 1 +
      (-2 • 2⁻¹ • (A₁ * B₀) +
        (-2 • 2⁻¹ • (A₀ * B₀) + (2 • (Real.sqrt 2)⁻¹ • 1 + (2 • 2⁻¹ • (A₁ * B₁) + -2 • 2⁻¹ • (A₀ * B₁)))))
[PROOFSTEP]
simp only [M]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    (↑4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1 +
      ((↑(-2) * 2⁻¹) • (A₁ * B₀) +
        ((↑(-2) * 2⁻¹) • (A₀ * B₀) +
          ((↑2 * (Real.sqrt 2)⁻¹) • 1 + ((↑2 * 2⁻¹) • (A₁ * B₁) + (↑(-2) * 2⁻¹) • (A₀ * B₁)))))
[PROOFSTEP]
simp only [neg_mul, one_mul, mul_inv_cancel_of_invertible, Int.cast_one, add_assoc, add_comm, add_left_comm, one_smul,
  Int.cast_neg, neg_smul, Int.int_cast_ofNat]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + Real.sqrt 2 ^ 3 • 1))) =
    A₁ * B₁ +
      (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + ((2 * (Real.sqrt 2)⁻¹) • 1 + (4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1))))
[PROOFSTEP]
simp only [← add_assoc, ← add_smul]
  -- just look at the coefficients now:
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + -(A₀ * B₀) + -(A₀ * B₁) + -(A₁ * B₀) + Real.sqrt 2 ^ 3 • 1 =
    A₁ * B₁ + -(A₀ * B₀) + -(A₀ * B₁) + -(A₁ * B₀) + (2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)) • 1
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ^ 3 = 2 * (Real.sqrt 2)⁻¹ + 4 * ((Real.sqrt 2)⁻¹ * 2⁻¹)
[PROOFSTEP]
exact mul_left_cancel₀ (by norm_num) tsirelson_inequality_aux
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
⊢ Real.sqrt 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
have pos : 0 ≤ √2⁻¹ • (P ^ 2 + Q ^ 2) :=
  by
  have P_sa : star P = P := by
    simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
  have Q_sa : star Q = Q := by
    simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
  have P2_nonneg : 0 ≤ P ^ 2 := by
    rw [sq]
    conv =>
      congr
      skip
      congr
      rw [← P_sa]
    convert (star_mul_self_nonneg P)
  have Q2_nonneg : 0 ≤ Q ^ 2 := by
    rw [sq]
    conv =>
      congr
      skip
      congr
      rw [← Q_sa]
    convert (star_mul_self_nonneg Q)
  convert
    smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg)
      (le_of_lt (show 0 < √2⁻¹ by norm_num))
        -- `norm_num` can't directly show `0 ≤ √2⁻¹`
  simp
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have P_sa : star P = P := by
  simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ star P = P
[PROOFSTEP]
simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have Q_sa : star Q = Q := by
  simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ star Q = Q
[PROOFSTEP]
simp only [star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa, T.B₁_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have P2_nonneg : 0 ≤ P ^ 2 := by
  rw [sq]
  conv =>
    congr
    skip
    congr
    rw [← P_sa]
  convert (star_mul_self_nonneg P)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ P ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ P * P
[PROOFSTEP]
conv =>
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
  congr
  skip
  congr
  rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0 ≤ P * P
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
skip
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
| P * P
[PROOFSTEP]
rw [← P_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ star P * star P
[PROOFSTEP]
convert (star_mul_self_nonneg P)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
have Q2_nonneg : 0 ≤ Q ^ 2 := by
  rw [sq]
  conv =>
    congr
    skip
    congr
    rw [← Q_sa]
  convert (star_mul_self_nonneg Q)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q * Q
[PROOFSTEP]
conv =>
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
  congr
  skip
  congr
  rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0 ≤ Q * Q
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
skip
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| 0
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
| Q * Q
[PROOFSTEP]
rw [← Q_sa]
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ star Q * star Q
[PROOFSTEP]
convert (star_mul_self_nonneg Q)
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
[PROOFSTEP]
convert
  smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg)
    (le_of_lt (show 0 < √2⁻¹ by norm_num))
      -- `norm_num` can't directly show `0 ≤ √2⁻¹`
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ 0 < (Real.sqrt 2)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ ↑0 = (Real.sqrt 2)⁻¹ • 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ Real.sqrt 2 ^ 3 • 1
[PROOFSTEP]
apply le_of_sub_nonneg
[GOAL]
case a
R : Type u
inst✝⁴ : OrderedRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : OrderedSMul ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (Real.sqrt 2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (Real.sqrt 2)⁻¹ • (A₁ - A₀) + B₁
w : Real.sqrt 2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : ↑0 ≤ (Real.sqrt 2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ Real.sqrt 2 ^ 3 • 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
[PROOFSTEP]
simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos
