internlm/Lean-Github huggingface dataset:
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } = npowRec (Nat.succ n) { toFinsupp := a }
Tactic:
simp [npowRec, pow_succ]
Proof state after:
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } =
    { toFinsupp := a } * npowRec n { toFinsupp := a }
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } =
    { toFinsupp := a } * npowRec n { toFinsupp := a }
Tactic:
rw [<- n_ih, <- ofFinsupp_mul]
Proof state after:
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } =
    { toFinsupp := AddMonoidAlgebra.mul' φ a (SkewPolynomial.AddMonoidAlgebra.pow' φ n a) }
Theorem: SkewPolynomial.ofFinsupp_pow
Proof state before:
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } =
    { toFinsupp := AddMonoidAlgebra.mul' φ a (SkewPolynomial.AddMonoidAlgebra.pow' φ n a) }
Tactic:
rfl
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_add
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b : R[X;φ]
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
Tactic:
cases a
Proof state after:
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q b : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp
Theorem: SkewPolynomial.toFinsupp_add
Proof state before:
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q b : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp
Tactic:
cases b
Proof state after:
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
Theorem: SkewPolynomial.toFinsupp_add
Proof state before:
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_add]
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_neg
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a : S[X;φ]
⊢ (-a).toFinsupp = -a.toFinsupp
Tactic:
cases a
Proof state after:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
toFinsupp✝ : AddMonoidAlgebra S ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
Theorem: SkewPolynomial.toFinsupp_neg
Proof state before:
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
toFinsupp✝ : AddMonoidAlgebra S ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_neg]
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_sub
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : S[X;φ]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
Tactic:
rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
Proof state after:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : S[X;φ]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp
Theorem: SkewPolynomial.toFinsupp_sub
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : S[X;φ]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp
Tactic:
rfl
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_mul
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b : R[X;φ]
⊢ (a * b).toFinsupp = AddMonoidAlgebra.mul' φ a.toFinsupp b.toFinsupp
Tactic:
cases a
Proof state after:
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q b : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp =
    AddMonoidAlgebra.mul' φ { toFinsupp := toFinsupp✝ }.toFinsupp b.toFinsupp
Theorem: SkewPolynomial.toFinsupp_mul
Proof state before:
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q b : R[X;φ]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp =
    AddMonoidAlgebra.mul' φ { toFinsupp := toFinsupp✝ }.toFinsupp b.toFinsupp
Tactic:
cases b
Proof state after:
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    AddMonoidAlgebra.mul' φ { toFinsupp := toFinsupp✝¹ }.toFinsupp { toFinsupp := toFinsupp✝ }.toFinsupp
Theorem: SkewPolynomial.toFinsupp_mul
Proof state before:
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    AddMonoidAlgebra.mul' φ { toFinsupp := toFinsupp✝¹ }.toFinsupp { toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_mul]
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_pow
Proof state before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a : R[X;φ]
n : ℕ
⊢ (a ^ n).toFinsupp = SkewPolynomial.AddMonoidAlgebra.pow' φ n a.toFinsupp
Tactic:
cases a
Proof state after:
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp =
    SkewPolynomial.AddMonoidAlgebra.pow' φ n { toFinsupp := toFinsupp✝ }.toFinsupp
Theorem: SkewPolynomial.toFinsupp_pow
Proof state before:
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp =
    SkewPolynomial.AddMonoidAlgebra.pow' φ n { toFinsupp := toFinsupp✝ }.toFinsupp
Tactic:
rw [← ofFinsupp_pow]
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_eq_zero
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a : R[X;φ]
⊢ a.toFinsupp = 0 ↔ a = 0
Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]
Proof state after:
no goals
Theorem: SkewPolynomial.toFinsupp_eq_one
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a : R[X;φ]
⊢ a.toFinsupp = 1 ↔ a = 1
Tactic:
rw [← toFinsupp_one, toFinsupp_inj]
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_eq_zero
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 0 ↔ a = 0
Tactic:
rw [← ofFinsupp_zero, ofFinsupp_inj]
Proof state after:
no goals
Theorem: SkewPolynomial.ofFinsupp_eq_one
Proof state before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 1 ↔ a = 1
Tactic:
rw [← ofFinsupp_one, ofFinsupp_inj]
Proof state after:
no goals
Theorem: SkewPolynomial.mul_assoc
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ a * b * c = a * (b * c)
Tactic:
rw [←toFinsupp_inj]
Proof state after:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (a * b * c).toFinsupp = (a * (b * c)).toFinsupp
Theorem: SkewPolynomial.mul_assoc
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (a * b * c).toFinsupp = (a * (b * c)).toFinsupp
Tactic:
simp only [toFinsupp_mul, AddMonoidAlgebra.mul'_def]
Proof state after:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (sum (sum a.toFinsupp fun a₁ b₁ => sum b.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₁ b₁ =>
      sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum a.toFinsupp fun a₁ b₁ =>
      sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (sum (sum a.toFinsupp fun a₁ b₁ => sum b.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₁ b₁ =>
      sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum a.toFinsupp fun a₁ b₁ =>
      sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)
Tactic:
rw [sum_sum_index]
Proof state after:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (sum a.toFinsupp fun a b_1 =>
      sum (sum b.toFinsupp fun a₂ b₂ => single (a + a₂) (b_1 * (↑φ)^[a] b₂)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum a.toFinsupp fun a₁ b₁ =>
      sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (sum a.toFinsupp fun a b_1 =>
      sum (sum b.toFinsupp fun a₂ b₂ => single (a + a₂) (b_1 * (↑φ)^[a] b₂)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum a.toFinsupp fun a₁ b₁ =>
      sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
congr
Proof state after:
case e_g
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (fun a b_1 =>
      sum (sum b.toFinsupp fun a₂ b₂ => single (a + a₂) (b_1 * (↑φ)^[a] b₂)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    fun a₁ b₁ =>
    sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
      single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ (fun a b_1 =>
      sum (sum b.toFinsupp fun a₂ b₂ => single (a + a₂) (b_1 * (↑φ)^[a] b₂)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    fun a₁ b₁ =>
    sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
      single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
ext a₁ b₁
Proof state after:
case e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ (sum (sum b.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₁ b₁ =>
      sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
      single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ (sum (sum b.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₁ b₁ =>
      sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum (sum b.toFinsupp fun a₁ b₁ => sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) fun a₂ b₂ =>
      single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
rw [sum_sum_index, sum_sum_index]
Proof state after:
case e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ (sum b.toFinsupp fun a b =>
      sum (single (a₁ + a) (b₁ * (↑φ)^[a₁] b)) fun a₁ b₁ =>
        sum c.toFinsupp fun a₂ b₂ => single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)) =
    sum b.toFinsupp fun a b =>
      sum (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b * (↑φ)^[a] b₂)) fun a₂ b₂ =>
        single (a₁ + a₂) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)
Tactic:
pick_goal 7
Proof state after:
case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)

case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0
Theorem: SkewPolynomial.mul_assoc
Proof state before:
case h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) ((b₁ + b₂) * (↑φ)^[a] b₂_1)) =
      (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (b₁ * (↑φ)^[a] b₂)) +
        sum c.toFinsupp fun a₂ b₂_1 => single (a + a₂) (b₂ * (↑φ)^[a] b₂_1)

case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0
Tactic:
. intros n r1 r2
  simp_rw [add_mul, AddMonoidAlgebra.single_add, sum_add]
Proof state after:
case e_g.h.h.e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
a₃ : ℕ
b₃ : R
⊢ single (a₁ + (a₂ + a₃)) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.e_g.h.h
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ (sum c.toFinsupp fun a₂_1 b₂ => single (a₁ + a₂ + a₂_1) (0 * (↑φ)^[a₁ + a₂] b₂)) = 0

case e_g.h.h.e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), single (a₁ + a) (b₁ * (↑φ)^[a₁] 0) = 0

case e_g.h.h.h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0

case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0