awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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₁
abel_nf :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 +
      (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₀) +
        (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₁) + (HSMul.hSMul (α := ℤ) (-1) (A₁ * B₀) + A₁ * B₁))) =
    HSMul.hSMul (α := ℤ) 4 (HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1) +
      (HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀)) +
        (HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀)) +
          (HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul (β := R) (√2)⁻¹ 1) +
            (HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁)) +
              HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁))))))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀)) -
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀) + HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀) - HSMul.hSMul (β := R) (√2)⁻¹ 1) +
      (HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 + HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁)) +
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁) + HSMul.hSMul (β := R) (√2)⁻¹ 1))

Tactic:
abel_nf
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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₁
simp :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 +
      (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₀) +
        (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₁) + (HSMul.hSMul (α := ℤ) (-1) (A₁ * B₀) + A₁ * B₁))) =
    HSMul.hSMul (β := R) ((↑4 : ℝ) * ((√2)⁻¹ * 2⁻¹)) 1 +
      (HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₁ * B₀) +
        (HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₀ * B₀) +
          (HSMul.hSMul (β := R) ((↑2 : ℝ) * (√2)⁻¹) 1 +
            (HMul.hMul (α := ℝ) (↑2 : ℝ) 2⁻¹ • (A₁ * B₁) + HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₀ * B₁)))))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 +
      (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₀) +
        (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₁) + (HSMul.hSMul (α := ℤ) (-1) (A₁ * B₀) + A₁ * B₁))) =
    HSMul.hSMul (α := ℤ) 4 (HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1) +
      (HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀)) +
        (HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀)) +
          (HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul (β := R) (√2)⁻¹ 1) +
            (HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁)) +
              HSMul.hSMul (α := ℤ) (-2) (HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁))))))

Tactic:
simp only [M]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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₁
simp :
  A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1))) =
    A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + HSMul.hSMul (β := R) (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹)) 1)))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 +
      (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₀) +
        (HSMul.hSMul (α := ℤ) (-1) (A₀ * B₁) + (HSMul.hSMul (α := ℤ) (-1) (A₁ * B₀) + A₁ * B₁))) =
    HSMul.hSMul (β := R) ((↑4 : ℝ) * ((√2)⁻¹ * 2⁻¹)) 1 +
      (HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₁ * B₀) +
        (HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₀ * B₀) +
          (HSMul.hSMul (β := R) ((↑2 : ℝ) * (√2)⁻¹) 1 +
            (HMul.hMul (α := ℝ) (↑2 : ℝ) 2⁻¹ • (A₁ * B₁) + HMul.hMul (α := ℝ) (↑(-2) : ℝ) 2⁻¹ • (A₀ * B₁)))))

Tactic:
simp only [neg_mul, mul_inv_cancel_of_invertible, add_assoc, add_comm,
      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.cast_ofNat, ← add_smul]

Premises used: mul_inv_cancel_of_invertible, Int.cast_neg, neg_smul, add_left_comm, add_assoc, Int.cast_ofNat, add_comm, one_smul, add_smul, neg_mul
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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₀) + HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1))) =
    A₁ * B₁ + (-(A₀ * B₀) + (-(A₀ * B₁) + (-(A₁ * B₀) + HSMul.hSMul (β := R) (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹)) 1)))

Tactic:
grind
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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₁
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)

Tactic:
have w : √2 ^ 3 • (1 : R) - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2) := by
    dsimp [P, Q]
    -- 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, mul_inv_cancel_of_invertible, add_assoc, add_comm,
      add_left_comm, one_smul, Int.cast_neg, neg_smul, Int.cast_ofNat, ← add_smul]
    grind
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
⊢ star P = P

Tactic:
simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]

Premises used: IsCHSHTuple.B₀_sa, StarAddMonoid.star_add, StarModule.star_smul, IsCHSHTuple.A₁_sa, IsCHSHTuple.A₀_sa, star_id_of_comm, star_sub
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
⊢ star P = P

Tactic:
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]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
⊢ star Q = Q

Tactic:
simp only [Q, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₁_sa]

Premises used: IsCHSHTuple.B₁_sa, StarAddMonoid.star_add, StarModule.star_smul, IsCHSHTuple.A₁_sa, IsCHSHTuple.A₀_sa, star_id_of_comm, star_sub
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
⊢ star Q = Q

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]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ HPow.hPow (β := ℕ) P 2

Tactic:
simpa only [P_sa, sq] using star_mul_self_nonneg P

Premises used: sq, star_mul_self_nonneg
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ HPow.hPow (β := ℕ) P 2

Tactic:
have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ HPow.hPow (β := ℕ) P 2
⊢ 0 ≤ HPow.hPow (β := ℕ) Q 2

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

Premises used: sq, star_mul_self_nonneg
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ HPow.hPow (β := ℕ) P 2
⊢ 0 ≤ HPow.hPow (β := ℕ) Q 2

Tactic:
have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ HPow.hPow (β := ℕ) P 2
Q2_nonneg : 0 ≤ HPow.hPow (β := ℕ) Q 2
⊢ 0 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)

Tactic:
positivity
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
⊢ 0 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)

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]
    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]
    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
    positivity
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
pos : 0 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
a : 0 ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1

Tactic:
apply le_of_sub_nonneg

Premises used: le_of_sub_nonneg
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
inst_6 : 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 :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
pos : 0 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
⊢ 0 ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)

Tactic:
simpa only [sub_add_eq_sub_sub, ← sub_add, w, Nat.cast_zero] using pos

Premises used: sub_add, sub_add_eq_sub_sub, Nat.cast_zero
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
⊢ ∀ (a_1 : R), Commute (star a) a_1

Tactic:
simpa only [star_mul, star_star] using fun g =>
    congr_arg star ((mem_center_iff.1 ha).comm <| star g).symm

Premises used: star_star, IsMulCentral.comm, Set.mem_center_iff, congr_arg, Commute.symm, Iff.mp, StarMul.star_mul, Star.star
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : star a * (b * c) = star a * (b * star (star c))
rw₁ rw₂ : star a * (b * c) = star a * (b * c)
⊢ star a * (b * c) = star a * (star (star b) * star (star c))

Tactic:
rw [star_star, star_star]

Premises used: star_star
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw rw₁ : star a * (star (star b) * star (star c)) = star a * (star (star b) * star (star c))
⊢ star a * (star (star b) * star (star c)) = star a * star (star c * star b)

Tactic:
rw [star_mul]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw rw₁ : star (star c * star b * a) = star (star c * star b * a)
⊢ star a * star (star c * star b) = star (star c * star b * a)

Tactic:
rw [← star_mul]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw rw₁ : star (star c * (star b * a)) = star (star c * (star b * a))
⊢ star (star c * star b * a) = star (star c * (star b * a))

Tactic:
rw [ha.right_assoc]

Premises used: IsMulCentral.right_assoc
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : star (star b * a) * star (star c) = star (star b * a) * c
rw₁ rw₂ : star (star b * a) * c = star (star b * a) * c
⊢ star (star c * (star b * a)) = star (star b * a) * c

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : star a * star (star b) * c = star a * b * c
rw₁ rw₂ : star a * b * c = star a * b * c
⊢ star (star b * a) * c = star a * b * c

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : b * c * star a = star (star (b * c)) * star a
rw₁ rw₂ : b * c * star a = b * c * star a
⊢ b * c * star a = star (a * star (b * c))

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw rw₁ : star (a * (star c * star b)) = star (a * (star c * star b))
⊢ star (a * star (b * c)) = star (a * (star c * star b))

Tactic:
rw [star_mul b]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw rw₁ : star (a * star c * star b) = star (a * star c * star b)
⊢ star (a * (star c * star b)) = star (a * star c * star b)

Tactic:
rw [ha.left_assoc]

Premises used: IsMulCentral.left_assoc
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : star (star b) * star (a * star c) = b * star (a * star c)
rw₁ rw₂ : b * star (a * star c) = b * star (a * star c)
⊢ star (a * star c * star b) = b * star (a * star c)

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
rw : b * (star (star c) * star a) = b * (c * star a)
rw₁ rw₂ : b * (c * star a) = b * (c * star a)
⊢ b * star (a * star c) = b * (c * star a)

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
simp : {a : R | ∀ m ∈ s, Commute (star m) a}
| star {c : R | ∀ m ∈ s, Commute m c}

Tactic:
simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]

Premises used: Set.preimage_setOf_eq, commute_star_comm, Set.star_preimage
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
conv_lhs : Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}
⊢ Eq.{u_1 + 1} (α := Set R) (star {c : R | ∀ m ∈ s, Commute m c}) {c : R | ∀ m ∈ star s, Commute m c}

Tactic:
conv_lhs => simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]

Premises used: Set.preimage_setOf_eq, commute_star_comm, Set.star_preimage
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
simp : {c : R | ∀ ⦃x : R⦄, x ∈ s → Commute (star x) c}
| {c : R | ∀ m ∈ star s, Commute m c}

Tactic:
simp only [← image_star, forall_mem_image]

Premises used: Set.image_star, Set.forall_mem_image
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
conv_rhs : Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}
conv_rhs₁ :
  Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ ⦃x : R⦄, x ∈ s → Commute (star x) c}
⊢ Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}

Tactic:
conv_rhs => simp only [← image_star, forall_mem_image]

Premises used: Set.image_star, Set.forall_mem_image
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
change : s ∪ star s ⊆ (s ∪ star s).centralizer
⊢ ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y

Tactic:
change s ∪ star s ⊆ (s ∪ star s).centralizer

Premises used: Set.centralizer, Union.union, Star.star
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
simp_rw : (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer

Tactic:
simp_rw [centralizer_union, ← star_centralizer, union_subset_iff, subset_inter_iff,
    star_subset_star, star_subset]

Premises used: Set.star_centralizer, Set.union_subset_iff, Set.subset_inter_iff, Set.star_subset, Set.star_subset_star, Set.centralizer_union
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer

Tactic:
⟨⟨hcomm, hcomm_star⟩, ⟨hcomm_star, hcomm⟩⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer

Tactic:
exact ⟨⟨hcomm, hcomm_star⟩, ⟨hcomm_star, hcomm⟩⟩
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y

Tactic:
simpa using congr_arg star (ha _ (h _ hy)).symm

Premises used: congr_arg, Eq.symm, Star.star