-- 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₁
⊢ 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))))

Tactic:
simp only [← add_assoc, ← add_smul]

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)⁻¹ + 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
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q ^ 2

Tactic:
simpa only [Q_sa, sq] using star_mul_self_nonneg Q

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 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (A₁ * B₀) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (A₀ * B₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • 1) +
      (((√2)⁻¹ * 2⁻¹) • 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (A₁ * B₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (A₀ * B₁)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • 1))

Tactic:
abel_nf

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 : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
let P := (√2)⁻¹ • (A₁ + A₀) - B₀

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₀
⊢ 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₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by
  rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]

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
⊢ 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₀
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
let Q := (√2)⁻¹ • (A₁ - A₀) + B₁

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

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₁) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      (((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))

Tactic:
simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]

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⁻¹) • 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • 1) +
      (((√2)⁻¹ * 2⁻¹) • 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√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
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
Q2_nonneg : 0 ≤ Q ^ 2
⊢ 0 ≤ (√2)⁻¹

Tactic:
positivity

Result:
no goals