Theorem: MvPowerSeries.coeff_pow (DividedPowers/ForMathlib/MvPowerSeries/Basic.lean)

State before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ (coeff α d) (f ^ n) = ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f
Tactic:
suffices f ^ n = (Finset.range n).prod fun _ => f by
  rw [this, coeff_prod]
State after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f

State before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f
Tactic:
rw [Finset.prod_const, card_range]
State after:
no goals

State before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff α d) (f ^ n) = ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f
Tactic:
rw [this, coeff_prod]
State after:
no goals