awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (β := 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₁)))))
have 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)))
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]
-- 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₁
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
have 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)
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
-- 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₁
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)
have P_sa : 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]
-- 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₁
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
⊢ 0 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
have Q_sa : 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]
-- 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₁
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 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
have P2_nonneg : 0 ≤ HPow.hPow (β := ℕ) P 2
Tactic: have P2_nonneg : 0 ≤ P ^ 2 := by simpa only [P_sa, sq] using star_mul_self_nonneg P
-- 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₁
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 ≤ (√2)⁻¹ • (HPow.hPow (β := ℕ) P 2 + HPow.hPow (β := ℕ) Q 2)
have Q2_nonneg : 0 ≤ HPow.hPow (β := ℕ) Q 2
Tactic: have Q2_nonneg : 0 ≤ Q ^ 2 := by simpa only [Q_sa, sq] using star_mul_self_nonneg Q
-- 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₁
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)
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1
have pos : 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
-- 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₁
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₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1
have a : 0 ≤ HSMul.hSMul (β := R) (HPow.hPow (β := ℕ) (√2) 3) 1 - (A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁)
Tactic: apply le_of_sub_nonneg
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (b * c) = star a * (star (star b) * star (star c))
have rw : star a * (b * c) = star a * (b * star (star c))
Tactic: rw [star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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))
⊢ star a * (b * c) = star a * (star (star b) * star (star c))
have rw₁ : star a * (b * c) = star a * (b * c)
Tactic: rw [star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (star (star b) * star (star c)) = star a * star (star c * star b)
have rw : star a * (star (star b) * star (star c)) = star a * (star (star b) * star (star c))
Tactic: rw [star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * star (star c * star b) = star (star c * star b * a)
have rw : star (star c * star b * a) = star (star c * star b * a)
Tactic: rw [← star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * star b * a) = star (star c * (star b * a))
have rw : star (star c * (star b * a)) = star (star c * (star b * a))
Tactic: rw [ha.right_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * (star b * a)) = star (star b * a) * c
have rw : star (star b * a) * star (star c) = star (star b * a) * c
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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
⊢ star (star c * (star b * a)) = star (star b * a) * c
have rw₁ : star (star b * a) * c = star (star b * a) * c
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star b * a) * c = star a * b * c
have rw : star a * star (star b) * c = star a * b * c
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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
⊢ star (star b * a) * c = star a * b * c
have rw₁ : star a * b * c = star a * b * c
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * c * star a = star (a * star (b * c))
have rw : b * c * star a = star (star (b * c)) * star a
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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
⊢ b * c * star a = star (a * star (b * c))
have rw₁ : b * c * star a = b * c * star a
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * star (b * c)) = star (a * (star c * star b))
have rw : star (a * (star c * star b)) = star (a * (star c * star b))
Tactic: rw [star_mul b]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * (star c * star b)) = star (a * star c * star b)
have rw : star (a * star c * star b) = star (a * star c * star b)
Tactic: rw [ha.left_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * star c * star b) = b * star (a * star c)
have rw : star (star b) * star (a * star c) = b * star (a * star c)
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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)
⊢ star (a * star c * star b) = b * star (a * star c)
have rw₁ : b * star (a * star c) = b * star (a * star c)
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * star (a * star c) = b * (c * star a)
have rw : b * (star (star c) * star a) = b * (c * star a)
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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)
⊢ b * star (a * star c) = b * (c * star a)
have rw₁ : b * (c * star a) = b * (c * star a)
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
| star {c : R | ∀ m ∈ s, Commute m c}
have simp : {a : R | ∀ m ∈ s, Commute (star m) a}
Tactic: simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
⊢ Eq.{u_1 + 1} (α := Set R) (star {c : R | ∀ m ∈ s, Commute m c}) {c : R | ∀ m ∈ star s, Commute m c}
have conv_lhs : Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}
Tactic: conv_lhs => simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
| {c : R | ∀ m ∈ star s, Commute m c}
have simp : {c : R | ∀ ⦃x : R⦄, x ∈ s → Commute (star x) c}
Tactic: simp only [← image_star, forall_mem_image]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
s : Set R
⊢ Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}
have conv_rhs : 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]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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}
⊢ Eq.{u_1 + 1} (α := Set R) {a : R | ∀ m ∈ s, Commute (star m) a} {c : R | ∀ m ∈ star s, Commute m c}
have 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}
Tactic: conv_rhs => simp only [← image_star, forall_mem_image]
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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
⊢ ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y
have change : s ∪ star s ⊆ (s ∪ star s).centralizer
Tactic: change s ∪ star s ⊆ (s ∪ star s).centralizer
-- Lean 4 proof step from Mathlib.Algebra.Star.Center (goal)
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 ∪ star s ⊆ (s ∪ star s).centralizer
have simp_rw : (s ⊆ s.centralizer ∧ s ⊆ star s.centralizer) ∧ s ⊆ star s.centralizer ∧ s ⊆ s.centralizer
Tactic: simp_rw [centralizer_union, ← star_centralizer, union_subset_iff, subset_inter_iff,
    star_subset_star, star_subset]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
x : α
⊢ Eq (α := α) ((star (star f) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw : Eq (α := α) (star ((star f : (a : α) → α) (star x)) : α) ((f : (a : α) → α) x : α)
Tactic: rw [star_apply, star_apply, star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
x : α
rw : Eq (α := α) (star ((star f : (a : α) → α) (star x)) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((star (star f) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw₁ : Eq (α := α) (star (star ((f : (a : α) → α) (star (star x)))) : α) ((f : (a : α) → α) x : α)
Tactic: rw [star_apply, star_apply, star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
x : α
rw : Eq (α := α) (star ((star f : (a : α) → α) (star x)) : α) ((f : (a : α) → α) x : α)
rw₁ : Eq (α := α) (star (star ((f : (a : α) → α) (star (star x)))) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((star (star f) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw₂ : Eq (α := α) ((f : (a : α) → α) (star (star x)) : α) ((f : (a : α) → α) x : α)
Tactic: rw [star_apply, star_apply, star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
x : α
rw : Eq (α := α) (star ((star f : (a : α) → α) (star x)) : α) ((f : (a : α) → α) x : α)
rw₁ : Eq (α := α) (star (star ((f : (a : α) → α) (star (star x)))) : α) ((f : (a : α) → α) x : α)
rw₂ : Eq (α := α) ((f : (a : α) → α) (star (star x)) : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((star (star f) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw₃ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [star_apply, star_apply, star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    (star ((star g : (a : α) → α) ((f : (a : α) → α) (star a) : α)) : α)
have rw : Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
  (star (star ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α))) : α)
Tactic: rw [star_apply, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
rw :
  Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    (star (star ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α))) : α)
⊢ Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    (star ((star g : (a : α) → α) ((f : (a : α) → α) (star a) : α)) : α)
have rw₁ : Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
  ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
Tactic: rw [star_apply, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ Eq (α := α) (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
    (star (((↑f : CentroidHom α) * star g : (a : α) → α) (star a)) : α)
have rw : Eq (α := α) (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
  (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
Tactic: rw [f.property.comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ Eq (α := α) (star ((f : (a : α) → α) ((star g : (a : α) → α) (star a) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
have rw : Eq (α := α) (star ((f : (a : α) → α) (star ((g : (a : α) → α) (star (star a))) : α)) : α)
  (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
Tactic: rw [star_apply, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
rw :
  Eq (α := α) (star ((f : (a : α) → α) (star ((g : (a : α) → α) (star (star a))) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
⊢ Eq (α := α) (star ((f : (a : α) → α) ((star g : (a : α) → α) (star a) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
have rw₁ : Eq (α := α) (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
  (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
Tactic: rw [star_apply, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
⊢ star (f * g) = star g * star f
have a : ∀ (a : α),
  Eq (α := α) (((↑(star (f * g)) : CentroidHom α) : (a : α) → α) a : α)
    (((↑(star g * star f) : CentroidHom α) : (a : α) → α) a : α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ Eq (α := α) ((star (f * g) : (a : α) → α) a : α) ((star (g * f) : (a : α) → α) a : α)
have rw : Eq (α := α) ((star (g * f) : (a : α) → α) a : α) ((star (g * f) : (a : α) → α) a : α)
Tactic: rw [CommMonoid.mul_comm f g]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ Eq (α := α) (((↑(star (f * g)) : CentroidHom α) : (a : α) → α) a : α)
    (((↑(star g * star f) : CentroidHom α) : (a : α) → α) a : α)
have star : Eq (α := α) ((star (f * g) : (a : α) → α) a : α) ((star (g * f) : (a : α) → α) a : α)
Tactic: calc
      star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
star : Eq (α := α) ((Star.star (f * g) : (a : α) → α) a : α) ((Star.star (g * f) : (a : α) → α) a : α)
⊢ Eq (α := α) (((↑(Star.star (f * g)) : CentroidHom α) : (a : α) → α) a : α)
    (((↑(Star.star g * Star.star f) : CentroidHom α) : (a : α) → α) a : α)
have star₁ : Eq (α := α) (Star.star ((g : (a : α) → α) ((f : (a : α) → α) (Star.star a) : α)) : α)
  (Star.star ((g : (a : α) → α) (Star.star (Star.star ((f : (a : α) → α) (Star.star a))) : α)) : α)
Tactic: calc
      star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl