awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
inst_3 : Invertible (star r)
rw :
  star (r * @Invertible.invOf _ MulOne.toMul MulOne.toOne r _) *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _ =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _
⊢ star (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _

Tactic:
rw [← mul_one (star (⅟r)), ← mul_invOf_self (star r), ← mul_assoc, ← star_mul]

Premises used: mul_assoc, Invertible.invOf, mul_invOf_self, StarMul.star_mul, mul_one, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
inst_3 : Invertible (star r)
⊢ star (r * @Invertible.invOf _ MulOne.toMul MulOne.toOne r _) *
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _ =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
hx : IsLeftRegular x
a b : R
h : Eq.{u + 1} (α := R) ((fun (x_1 : R) ↦ x_1 * star x) a) ((fun (x_1 : R) ↦ x_1 * star x) b)
⊢ Eq.{u + 1} (α := R) ((fun (x_1 : R) ↦ x * x_1) (star a)) ((fun (x_1 : R) ↦ x * x_1) (star b))

Tactic:
simpa using congr_arg Star.star h

Premises used: congr_arg, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
hx : IsRightRegular x
a b : R
h : Eq.{u + 1} (α := R) ((fun (x_1 : R) ↦ star x * x_1) a) ((fun (x_1 : R) ↦ star x * x_1) b)
⊢ Eq.{u + 1} (α := R) ((fun (x_1 : R) ↦ x_1 * x) (star a)) ((fun (x_1 : R) ↦ x_1 * x) (star b))

Tactic:
simpa using congr_arg Star.star h

Premises used: congr_arg, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
hx : IsRegular x
⊢ IsRegular (star x)

Tactic:
⟨hx.right.star, hx.left.star⟩

Premises used: IsLeftRegular.star, IsRegular.right, IsRegular.mk, IsRightRegular.star, IsRegular.left
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
⊢ IsRightRegular (star x) ↔ IsLeftRegular x

Tactic:
⟨fun h => star_star x ▸ h.star, (·.star)⟩

Premises used: star_star, IsLeftRegular.star, Eq.rec, IsRightRegular.star, Iff.intro
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
⊢ IsLeftRegular (star x) ↔ IsRightRegular x

Tactic:
⟨fun h => star_star x ▸ h.star, (·.star)⟩

Premises used: star_star, IsLeftRegular.star, Eq.rec, IsRightRegular.star, Iff.intro
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
rw : IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsRegular x
rw₁ : IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsLeftRegular x ∧ IsRightRegular x
rw₂ : IsLeftRegular (star x) ∧ IsLeftRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
rw₃ : IsRightRegular x ∧ IsLeftRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
rw₄ rw₅ : IsLeftRegular x ∧ IsRightRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
⊢ IsRegular (star x) ↔ IsRegular x

Tactic:
rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]

Premises used: isRightRegular_star_iff, isRegular_iff, and_comm, isLeftRegular_star_iff
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Star R
r : Rᵐᵒᵖ
⊢ unop (star r) = star (unop r)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Star R
r : R
⊢ op (star r) = star (op r)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommMonoid R
inst_1 : StarMul R
⊢ StarModule Rᵐᵒᵖ R

Tactic:
⟨fun r s => star_mul' s r.unop⟩

Premises used: StarModule.mk, MulOpposite.unop, star_mul'
-- Module: Mathlib.Algebra.Star.BigOperators
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : StarMul R
α : Type u_2
s : Finset α
f : α → R
⊢ Eq.{u_1 + 1} (α := R) (star (∏ x ∈ s, f x)) (∏ x ∈ s, star (f x))

Tactic:
map_prod (starMulAut : R ≃* R) _ _

Premises used: map_prod, starMulAut
-- Module: Mathlib.Algebra.Star.BigOperators
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : StarAddMonoid R
α : Type u_2
s : Finset α
f : α → R
⊢ Eq.{u_1 + 1} (α := R) (star (∑ x ∈ s, f x)) (∑ x ∈ s, star (f x))

Tactic:
map_sum (starAddEquiv : R ≃+ R) _ _

Premises used: map_sum, starAddEquiv
-- Module: Mathlib.Algebra.Star.BigOperators
Goal:
R : Type u_1
ι : Type u_2
inst : AddCommMonoid R
inst_1 : StarAddMonoid R
s : Finset ι
x : ι → R
h : ∀ i ∈ s, IsSelfAdjoint (x i)
⊢ IsSelfAdjoint.{u_1} (R := R) (∑ i ∈ s, x i)

Tactic:
simpa [IsSelfAdjoint, star_sum] using Finset.sum_congr rfl fun _ hi => h _ hi

Premises used: IsSelfAdjoint, star_sum, Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Star.BigOperators
Goal:
R : Type u_1
ι : Type u_2
M : Type u_3
inst : Zero M
inst_1 : AddCommMonoid R
inst_2 : StarAddMonoid R
s : ι →₀ M
f : ι → M → R
⊢ star (s.sum f) = s.sum fun (i : ι) (m : M) ↦ star f i m

Tactic:
simp [Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.Algebra.Star.BigOperators
Goal:
R : Type u_1
ι : Type u_2
M : Type u_3
inst : Zero M
inst_1 : CommMonoid R
inst_2 : StarMul R
s : ι →₀ M
f : ι → M → R
⊢ star (s.prod f) = s.prod fun (i : ι) (m : M) ↦ star f i m

Tactic:
simp [Finsupp.prod]

Premises used: Finsupp.prod
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : HPow.hPow (β := ℕ) A₀ 2 = 1
A₁_inv : HPow.hPow (β := ℕ) A₁ 2 = 1
B₀_inv : HPow.hPow (β := ℕ) B₀ 2 = 1
B₁_inv : HPow.hPow (β := ℕ) 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₁)

Tactic:
grind
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ P * P = 4 * P

Tactic:
have idem : P * P = 4 * P := CHSH_id T.A₀_inv T.A₁_inv T.B₀_inv T.B₁_inv
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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 = HSMul.hSMul (α := ℝ) 4 P

Tactic:
simp [map_ofNat, Algebra.smul_def]

Premises used: map_ofNat, Algebra.smul_def
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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 = HSMul.hSMul (α := ℝ) 4 P

Tactic:
have h : 4 * P = (4 : ℝ) • P := by simp [map_ofNat, Algebra.smul_def]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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 = HSMul.hSMul (α := ℝ) 4 P
rw : P = (1 / 4 * 4) • P
⊢ P = (1 / 4) • (P * P)

Tactic:
rw [idem, h, ← mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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 = HSMul.hSMul (α := ℝ) 4 P
⊢ P = (1 / 4 * 4) • P

Tactic:
simp
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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)

Tactic:
have idem' : P = (1 / 4 : ℝ) • (P * P) := by
      have h : 4 * P = (4 : ℝ) • P := by simp [map_ofNat, Algebra.smul_def]
      rw [idem, h, ← mul_smul]
      simp
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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)
dsimp : star (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
⊢ star P = P

Tactic:
dsimp [P]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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₁

Tactic:
simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa,
        T.B₁_sa, mul_comm B₀, mul_comm B₁]

Premises used: star_ofNat, IsCHSHTuple.B₀_sa, IsCHSHTuple.B₁_sa, StarAddMonoid.star_add, IsCHSHTuple.A₁_sa, IsCHSHTuple.A₀_sa, mul_comm, StarMul.star_mul, star_sub
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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

Tactic:
have sa : star P = P := by
      dsimp [P]
      simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa,
        T.B₁_sa, mul_comm B₀, mul_comm B₁]
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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

Tactic:
simp
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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

Tactic:
simpa only [← idem', sa]
      using smul_nonneg (by simp : (0 : ℝ) ≤ 1 / 4) (star_mul_self_nonneg P)

Premises used: smul_nonneg, star_mul_self_nonneg
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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

Tactic:
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 [map_ofNat, Algebra.smul_def]
      rw [idem, h, ← mul_smul]
      simp
    have sa : star P = P := by
      dsimp [P]
      simp only [star_add, star_sub, star_mul, star_ofNat, T.A₀_sa, T.A₁_sa, T.B₀_sa,
        T.B₁_sa, mul_comm B₀, mul_comm B₁]
    simpa only [← idem', sa]
      using smul_nonneg (by simp : (0 : ℝ) ≤ 1 / 4) (star_mul_self_nonneg P)
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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 : 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2

Tactic:
apply le_of_sub_nonneg

Premises used: le_of_sub_nonneg
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
R : Type u
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : StarRing R
inst_3 : StarOrderedRing R
inst_4 : Algebra ℝ R
inst_5 : IsOrderedModule ℝ 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₁)

Tactic:
simpa only [sub_add_eq_sub_sub, ← sub_add] using i₁

Premises used: sub_add, sub_add_eq_sub_sub
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
rw : (√2 * √2)⁻¹ = 2⁻¹
⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

Tactic:
rw [← mul_inv]

Premises used: mul_inv
-- Module: Mathlib.Algebra.Star.CHSH
Goal:
⊢ (√2 * √2)⁻¹ = 2⁻¹

Tactic:
simp
-- 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 : ℤ
a : ℝ
x : R
rw : HSMul.hSMul (α := ℝ) (↑m : ℝ) (a • x) = ((↑m : ℝ) * a) • x
rw₁ rw₂ : ((↑m : ℝ) * a) • x = ((↑m : ℝ) * a) • x
⊢ m • a • x = ((↑m : ℝ) * a) • x

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

Premises used: Real, Int.cast_smul_eq_zsmul, SemigroupAction.mul_smul
-- 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 : ℤ) (a : ℝ) (x : R), m • a • x = ((↑m : ℝ) * a) • x

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]
-- 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₁
dsimp :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) ((√2)⁻¹ • (A₁ + A₀) - B₀) 2 + HPow.hPow (β := ℕ) ((√2)⁻¹ • (A₁ - A₀) + B₁) 2)
⊢ 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:
dsimp [P, 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₁
simp :
  HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√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₁)))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • (HPow.hPow (β := ℕ) ((√2)⁻¹ • (A₁ + A₀) - B₀) 2 + HPow.hPow (β := ℕ) ((√2)⁻¹ • (A₁ - A₀) + B₁) 2)

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

Premises used: add_mul, mul_sub, sq, sub_mul, smul_sub, mul_add, smul_add
-- 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 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₀)) -
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀) + HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      (((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₀)) +
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√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₁)))

Tactic:
simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]

Premises used: TsirelsonInequality.sqrt_two_inv_mul_self, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, SemigroupAction.mul_smul
-- 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 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₀)) -
        (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⁻¹ (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₀)) +
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁) + HSMul.hSMul (β := R) (√2)⁻¹ 1))
⊢ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₀)) -
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₀) + HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      (((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₀)) +
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))

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

Premises used: IsCHSHTuple.A₁_inv, sq, IsCHSHTuple.B₀_inv, IsCHSHTuple.B₁_inv, IsCHSHTuple.A₀_inv
-- 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 - 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))
⊢ 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⁻¹ (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 - HSMul.hSMul (α := ℝ) 2⁻¹ (B₀ * A₀)) -
        (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⁻¹ (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - HSMul.hSMul (β := R) ((√2)⁻¹ * 2⁻¹) 1 + HSMul.hSMul (α := ℝ) 2⁻¹ (B₁ * A₀)) +
        (HSMul.hSMul (α := ℝ) 2⁻¹ (A₁ * B₁) - HSMul.hSMul (α := ℝ) 2⁻¹ (A₀ * B₁) + HSMul.hSMul (β := R) (√2)⁻¹ 1))

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

Premises used: IsCHSHTuple.A₀B₀_commutes, IsCHSHTuple.A₁B₁_commutes, IsCHSHTuple.A₀B₁_commutes, IsCHSHTuple.A₁B₀_commutes