Theorem: SkewPolynomial.ofFinsupp_pow (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = { toFinsupp := a } ^ n
Tactic:
change _ = npowRec n _
State after:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }

State before:
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
Tactic:
induction n with
| zero        => simp [npowRec]; rfl
| succ n n_ih => simp [npowRec, pow_succ]; rw [<- n_ih, <- ofFinsupp_mul]; rfl
State after:
no goals

State before:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ Nat.zero a } = npowRec Nat.zero { toFinsupp := a }
Tactic:
simp [npowRec]
State after:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ 0 a } = 1

State before:
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ 0 a } = 1
Tactic:
rfl
State after:
no goals

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]
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 }

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]
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) }

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
State after:
no goals