awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
u : Rˣ
⊢ (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
have pos : (star (↑u : R))⁻¹ʳ = star (↑u⁻¹ : R)
Tactic: rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
u : Rˣ
pos : (star (↑u : R))⁻¹ʳ = star (↑u⁻¹ : R)
⊢ (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
have pos₁ : (↑(star u) : R)⁻¹ʳ = star (↑u⁻¹ : R)
Tactic: rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
u : Rˣ
pos : (star (↑u : R))⁻¹ʳ = star (↑u⁻¹ : R)
pos₁ : (↑(star u) : R)⁻¹ʳ = star (↑u⁻¹ : R)
⊢ (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
have pos₂ : (↑(star u)⁻¹ : R) = star (↑u⁻¹ : R)
Tactic: rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
u : Rˣ
pos : (star (↑u : R))⁻¹ʳ = star (↑u⁻¹ : R)
pos₁ : (↑(star u) : R)⁻¹ʳ = star (↑u⁻¹ : R)
pos₂ : (↑(star u)⁻¹ : R) = star (↑u⁻¹ : R)
⊢ (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
have pos₃ : (↑(star u)⁻¹ : R) = (↑(star u)⁻¹ : R)
Tactic: rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have neg : (star a)⁻¹ʳ = star 0
Tactic: rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : ¬IsUnit a
neg : (star a)⁻¹ʳ = star 0
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have neg₁ : Eq.{u + 1} (α := R) 0 (star 0)
Tactic: rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : ¬IsUnit a
neg : (star a)⁻¹ʳ = star 0
neg₁ : Eq.{u + 1} (α := R) 0 (star 0)
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have neg₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
⊢ star (@invOf _ MulOne.toMul MulOne.toOne r _) * star r = 1
have rw : star (r * @invOf _ MulOne.toMul MulOne.toOne r _) = 1
Tactic: rw [← star_mul, mul_invOf_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (r * @invOf _ MulOne.toMul MulOne.toOne r _) = 1
⊢ star (@invOf _ MulOne.toMul MulOne.toOne r _) * star r = 1
have rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
Tactic: rw [← star_mul, mul_invOf_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (r * @invOf _ MulOne.toMul MulOne.toOne r _) = 1
rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
⊢ star (@invOf _ MulOne.toMul MulOne.toOne r _) * star r = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← star_mul, mul_invOf_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
⊢ star r * star (@invOf _ MulOne.toMul MulOne.toOne r _) = 1
have rw : star (@invOf _ MulOne.toMul MulOne.toOne r _ * r) = 1
Tactic: rw [← star_mul, invOf_mul_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (@invOf _ MulOne.toMul MulOne.toOne r _ * r) = 1
⊢ star r * star (@invOf _ MulOne.toMul MulOne.toOne r _) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
Tactic: rw [← star_mul, invOf_mul_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (@invOf _ MulOne.toMul MulOne.toOne r _ * r) = 1
rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
⊢ star r * star (@invOf _ MulOne.toMul MulOne.toOne r _) = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← star_mul, invOf_mul_self, star_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
inst_3 : Invertible (star r)
⊢ star (@Invertible.invOf _ MulOne.toMul MulOne.toOne r _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne (star r) _
have 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) _
Tactic: rw [← mul_one (star (⅟r)), ← mul_invOf_self (star r), ← mul_assoc, ← star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
⊢ IsRegular (star x) ↔ IsRegular x
have rw : IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsRegular x
Tactic: rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x : R
rw : IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsRegular x
⊢ IsRegular (star x) ↔ IsRegular x
have rw₁ : IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
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
⊢ IsRegular (star x) ↔ IsRegular x
have rw₂ : IsLeftRegular (star x) ∧ IsLeftRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
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
⊢ IsRegular (star x) ↔ IsRegular x
have rw₃ : IsRightRegular x ∧ IsLeftRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
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
⊢ IsRegular (star x) ↔ IsRegular x
have rw₄ : IsLeftRegular x ∧ IsRightRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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
have idem : 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
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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)
have h : 4 * P = HSMul.hSMul (α := ℝ) 4 P
Tactic: have h : 4 * P = (4 : ℝ) • P := by simp [map_ofNat, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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) • (P * P)
have rw : P = (1 / 4 * 4) • P
Tactic: rw [idem, h, ← mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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
⊢ 0 ≤ P
have idem' : 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
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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)
⊢ 0 ≤ P
have sa : 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₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
have i₁ : 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)
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
have a : 0 ≤ 2 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
Tactic: apply le_of_sub_nonneg
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
Goal:
⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹
have rw : (√2 * √2)⁻¹ = 2⁻¹
Tactic: rw [← mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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
have rw : HSMul.hSMul (α := ℝ) (↑m : ℝ) (a • x) = ((↑m : ℝ) * a) • x
Tactic: rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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
⊢ m • a • x = ((↑m : ℝ) * a) • x
have rw₁ : ((↑m : ℝ) * a) • x = ((↑m : ℝ) * a) • x
Tactic: rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (hypothesis)
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₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1
have M : ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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 (β := ℕ) ((√2)⁻¹ • (A₁ + A₀) - B₀) 2 + HPow.hPow (β := ℕ) ((√2)⁻¹ • (A₁ - A₀) + B₁) 2)
have 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₁)))
Tactic: simp only [sq, sub_mul, mul_sub, add_mul, mul_add, smul_add, smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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)⁻¹ • ((√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₁)))
have 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₁)))
Tactic: simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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)⁻¹ * 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₁)))
have 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))
Tactic: simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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₁ =
    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))
have 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))
Tactic: simp only [← T.A₀B₀_commutes, ← T.A₀B₁_commutes, ← T.A₁B₀_commutes, ← T.A₁B₁_commutes]
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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₁ =
    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))
have 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₁))))))
Tactic: abel_nf
-- Lean 4 proof step from Mathlib.Algebra.Star.CHSH (goal)
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 +
      (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₁))))))
have 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₁)))))
Tactic: simp only [M]