-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
i : σ
h : ¬p ∣ (m : (a : σ) → ℕ) i
contrapose! contrapose!₁ :
  ∀ (h : ¬p ∣ (m : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
        R)
      (0 : R)
contrapose!₂ contrapose!₃ contrapose!₄ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
          R)
        (0 : R)),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₅ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₆ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0)
    (d : σ →₀ ℕ)
    (hd :
      Ne.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R)
        (0 : R)),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₇ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0)
    (d : σ →₀ ℕ)
    (hd :
      Ne.{u_3 + 1} (α := R)
        ((coeff m : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R)
        (0 : R))
    (this :
      Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
        ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₈ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0)
    (d : σ →₀ ℕ) (hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0)
    (this :
      Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
        ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)),
    p ∣ (m : (a : σ) → ℕ) i
contrapose!₉ :
  ∀
    (h :
      Ne.{u_3 + 1} (α := R)
        (∑ᶠ (d : σ →₀ ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff m : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R))
        0)
    (d : σ →₀ ℕ) (hd : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0)
    (this :
      Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
        ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1))
    (meq : m = p • d), p ∣ (m : (a : σ) → ℕ) i
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)

Tactic:
classical
  contrapose! h
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h
  obtain ⟨d, hd⟩ : ∃ (d : σ →₀ ℕ), (coeff m) (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) ≠ 0 := by
    by_contra! hc
    rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h
    contradiction
  have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [this, coeff_monomial] at hd
  have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction
  simp [meq]

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_subst, MvPowerSeries.HasSubst.X_pow, MvPowerSeries.coeff_monomial, MvPowerSeries.substAlgHom_apply