-- Mathlib/Algebra/Star/CHSH.lean
theorem tsirelson_inequality [OrderedRing R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R]
    [OrderedSMul ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) :
    A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • (1 : R)

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    4 • ((√2)⁻¹ * 2⁻¹) • 1 +
      (-2 • 2⁻¹ • (A₁ * B₀) + (-2 • 2⁻¹ • (A₀ * B₀) + (2 • (√2)⁻¹ • 1 + (2 • 2⁻¹ • (A₁ * B₁) + -2 • 2⁻¹ • (A₀ * B₁)))))

Tactic:
simp only [M]

Result:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    (↑4 * ((√2)⁻¹ * 2⁻¹)) • 1 +
      ((↑(-2) * 2⁻¹) • (A₁ * B₀) +
        ((↑(-2) * 2⁻¹) • (A₀ * B₀) + ((↑2 * (√2)⁻¹) • 1 + ((↑2 * 2⁻¹) • (A₁ * B₁) + (↑(-2) * 2⁻¹) • (A₀ * B₁)))))

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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

Tactic:
rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]

Result:
no goals

Proof state:
case e_a.e_a
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 = 2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹)

Tactic:
exact mul_left_cancel₀ (by norm_num) tsirelson_inequality_aux

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 + (-1 • (A₀ * B₀) + (-1 • (A₀ * B₁) + (-1 • (A₁ * B₀) + A₁ * B₁))) =
    (↑4 * ((√2)⁻¹ * 2⁻¹)) • 1 +
      ((↑(-2) * 2⁻¹) • (A₁ * B₀) +
        ((↑(-2) * 2⁻¹) • (A₀ * B₀) + ((↑2 * (√2)⁻¹) • 1 + ((↑2 * 2⁻¹) • (A₁ * B₁) + (↑(-2) * 2⁻¹) • (A₀ * B₁)))))

Tactic:
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.cast_ofNat]

Result:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + √2 ^ 3 • 1))) =
    A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + ((2 * (√2)⁻¹) • 1 + (4 * ((√2)⁻¹ * 2⁻¹)) • 1))))

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)

Tactic:
have Q_sa : star Q = Q := by
  simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa,
    T.B₁_sa]

Result:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
have pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
  have P_sa : star P = P := by
    simp only [P, 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 [Q, 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 simpa only [P_sa, sq] using star_mul_self_nonneg P
  have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
  exact smul_nonneg (by positivity) (add_nonneg P2_nonneg Q2_nonneg)

Result:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
pos : 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Proof state:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (((√2)⁻¹ • (A₁ + A₀) - B₀) ^ 2 + ((√2)⁻¹ • (A₁ - A₀) + B₁) ^ 2)

Tactic:
simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]

Result:
R : Type u
inst✝⁵ : OrderedRing R
inst✝⁴ : StarRing 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 := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₁) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₁) - (√2)⁻¹ • (B₀ * (√2)⁻¹ • A₁) +
          ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₀) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₀) - (√2)⁻¹ • (B₀ * (√2)⁻¹ • A₀)) -
        ((√2)⁻¹ • ((√2)⁻¹ • A₁ * B₀) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₁) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₁) + (√2)⁻¹ • (B₁ * (√2)⁻¹ • A₁) -
          ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₀) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₀) + (√2)⁻¹ • (B₁ * (√2)⁻¹ • A₀)) +
        ((√2)⁻¹ • ((√2)⁻¹ • A₁ * B₁) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))