case zero
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ X s ^ Nat.zero = ↑(monomial R (single s Nat.zero)) 1

case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = ↑(monomial R (single s n)) 1
⊢ X s ^ Nat.succ n = ↑(monomial R (single s (Nat.succ n))) 1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
⊢ X s ^ n = ↑(monomial R (single s n)) 1
induction' n with n ih
no goals
case zero
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ X s ^ Nat.zero = ↑(monomial R (single s Nat.zero)) 1
simp
no goals
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = ↑(monomial R (single s n)) 1
⊢ X s ^ Nat.succ n = ↑(monomial R (single s (Nat.succ n))) 1
rw [pow_succ', ih, Nat.succ_eq_add_one, Finsupp.single_add, X, monomial_mul_monomial, one_mul]