-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
            (IsLocalRing.ResidueField A)⟦X⟧)) :
      IsLocalRing.ResidueField A)
rw :
  ∀
    (H2 :
      1 =
        HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
          ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
            IsLocalRing.ResidueField A)
          ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((coeff (n, 0).1 : (a : A⟦X⟧) → A) g) :
            IsLocalRing.ResidueField A)),
    IsUnit (M := IsLocalRing.ResidueField A)
      ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
        IsLocalRing.ResidueField A)
rw₁ :
  ∀
    (H2 :
      Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
        (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
          HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
            ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
              IsLocalRing.ResidueField A)
            ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
              IsLocalRing.ResidueField A)))
    (p : ℕ × ℕ) (hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n) (hnotMem : p ∉ {(n, 0)}),
    HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A) =
      0
⊢ IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)

Tactic:
rw [coeff_mul, ← Finset.sum_subset (s₁ := {(n, 0)}) (by simp) (fun p hp hnotMem ↦ ?_),
    Finset.sum_singleton, coeff_map, coeff_map, coeff_zero_eq_constantCoeff, mul_comm] at H2

Premises used: Finset.sum_singleton, PowerSeries.coeff_mul, PowerSeries.coeff_map, Finset.sum_subset, PowerSeries.coeff_zero_eq_constantCoeff, mul_comm