mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
⊢ star Q = Q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
⊢ 0 ≤ P ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubsemiring

Goal state before:
pp: A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
p q : NonUnitalStarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubsemiring

Goal state before:
pp: A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = ↑S
x : R
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
p q : StarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S ↔ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S : StarSubsemiring R
s : Set R
hs : s = ↑S
a : R
ha : a ∈ (S.copy s hs).carrier
⊢ a ∈ S.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
S : StarSubsemiring R
a : R
hs : ↑S = ↑S
__Subsemiring✝ : Subsemiring R := S.copy (↑S) hs
ha : a ∈ (S.copy (↑S) hs).carrier
⊢ a ∈ S.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
P_sa : star P = P
Q_sa : star Q = Q
P2_nonneg : 0 ≤ P ^ 2
⊢ 0 ≤ Q ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ 0 ≤ (√2)⁻¹ • (P ^ 2 + Q ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial n) 1 = X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (p.sum fun a₂ b₂ ↦ (monomial (1 + a₂)) (0 * (⇑φ)^[1] b₂)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ), (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (0 * (⇑φ)^[a] b₂)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
⊢ A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) ((b₁ + b₂) * (⇑φ)^[a] b₂_1)) =
      (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (b₁ * (⇑φ)^[a] b₂)) +
        ((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) (b₂ * (⇑φ)^[a] b₂_1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
⊢ star (f (star 0)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
a b : α
⊢ star (f (star (a + b))) = star (f (star a)) + star (f (star b))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
a b : α
⊢ star (f (star (a * b))) = a * star (f (star b))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
a b : α
⊢ star (f (star (a * b))) = star (f (star a)) * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : CentroidHom α
x✝ : α
⊢ (star (star f)) x✝ = f x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X * p = (p.sum fun a b ↦ (monomial a) (φ b)) * X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ g (star (f (star a))) = star ((star g) (f (star a)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star ((star g * ↑f) (star a)) = star ((↑f * star g) (star a))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
⊢ star (f ((star g) (star a))) = star (f (star (g a)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ (star (f * g)) a = (star (g * f)) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ star (g (f (star a))) = star (g (star (star (f (star a)))))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
⊢ star (f * g) = star g * star f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (↑z * star a) = star (star a) * ↑(star z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (star a) * ↑(star z) = a * ↑(star z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * ↑(star z) = ↑(star z) * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
⊢ star (centerToCentroidCenter z) = centerToCentroidCenter (star z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
mul_comm : IsMulCommutative (CentroidHom α)
x✝² x✝¹ : CentroidHom α
x✝ : α
⊢ (star (x✝² * x✝¹)) x✝ = (star x✝¹ * star x✝²) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ T 1 ∈ StarSubsemiring.center α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
z : ↥(StarSubsemiring.center α)
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) (starCenterToCentroid.toFun z)) = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
x✝ : α
⊢ (starCenterToCentroid.toFun ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) ((MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) (a * b) =
    (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) b *
      (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) (a + b) =
    (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) a +
      (MulOpposite.unop ∘ ⇑((lift R) (MulOpposite.op ∘ ι R))) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ), (monomial a) ((⇑φ)^[n] 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : X
⊢ star (ι R x) = ι R x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ star ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ) (b₁ b₂ : R), (monomial a) ((⇑φ)^[n] (b₁ + b₂)) = (monomial a) ((⇑φ)^[n] b₁) + (monomial a) ((⇑φ)^[n] b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ starRingEquiv.toFun ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)ᵐᵒᵖ) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r * X ^ k = (monomial (n + k)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) (φ r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
k n : ℕ
r : R
⊢ X ^ k * (monomial n) r = (monomial (n + k)) ((⇑φ)^[k] r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ 1 = (monomial 0) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ coeff 1 n = if 0 = n then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
⊢ ((monomial (n + 1)) a).coeff 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r).coeff (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
m n : ℕ
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (↑m).coeff n = ↑(if n = 0 then m else 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : MulSemiringAction (Multiplicative ℕ) R
a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff 0 = OfNat.ofNat a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ C a * X ^ (n + 1) = (monomial (n + 1)) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ C a * X = (monomial 1) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ C a = 0 ↔ C a = C 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : 0 = 1
p : SkewPolynomial R
⊢ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial n) a).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
c : R
⊢ (C c * X).support ⊆ {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
c : R
h : c ≠ 0
⊢ (C c * X ^ n).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
c : R
⊢ (C c * X ^ n).support ⊆ {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X ^ n = (monomial n) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) a = (monomial n) (a * 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) (a * 1) = (monomial n) (a • 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ a • (monomial n) 1 = a • X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ a • X ^ n = (monomial n) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (X ^ n).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ X.support = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
⊢ p.sum f = ∑ n ∈ s, f n (p.coeff n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p q : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : SkewPolynomial R
n : ℕ
⊢ (p + q).coeff n = p.coeff n + q.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
p : SkewPolynomial R
f : ℕ → R → S
⊢ (p.sum fun n x ↦ -f n x) = -p.sum f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Type u_2
inst✝ : Ring S
p : SkewPolynomial R
f g : ℕ → R → S
⊢ (p.sum fun n x ↦ f n x - g n x) = p.sum f - p.sum g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : SkewPolynomial R
n : ℕ
⊢ (-p).coeff n = -p.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : SkewPolynomial R
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) (-a) = -(monomial n) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : SkewPolynomial R
⊢ (-p).support = p.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℤ
⊢ C ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (erase n p).support = p.support.erase n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (monomial n) (p.coeff n) + erase n p = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ erase n 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ erase n ((monomial n) a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (erase n p).coeff n = 0

Tactic:
by

Goal state after: