awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this :
  ∀ {d : σ →₀ ℕ},
    Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
      ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
rw :
  HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
          (m.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R) =
    (coeff m : (a : MvPowerSeries σ R) → R) φ
rw₁ :
  ∀ (x : σ →₀ ℕ),
    x ≠ m →
      HMul.hMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
              (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R) =
        0
⊢ Eq.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
rw [finsum_eq_single _ m]

Premises used: finsum_eq_single
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this :
  ∀ {d : σ →₀ ℕ},
    Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
      ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
rw :
  HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (p • m) : (a : MvPowerSeries σ R) → R) ((monomial (p • m) : (a : R) → MvPowerSeries σ R) 1) : R) =
    (coeff m : (a : MvPowerSeries σ R) → R) φ
rw₁ :
  HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (if p • m = p • m then 1 else 0 : R) =
    (coeff m : (a : MvPowerSeries σ R) → R) φ
rw₂ :
  HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (1 : R) =
    (coeff m : (a : MvPowerSeries σ R) → R) φ
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
          (m.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R) =
    (coeff m : (a : MvPowerSeries σ R) → R) φ

Tactic:
rw [this, coeff_monomial, if_pos rfl, mul_one]

Premises used: if_pos, MvPowerSeries.coeff_monomial, mul_one, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this :
  ∀ {d : σ →₀ ℕ},
    Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
      ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
d : σ →₀ ℕ
hd : d ≠ m
rw : ¬p • m = p • d
⊢ HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
        R) =
    0

Tactic:
rw [this, coeff_monomial, if_neg _, mul_zero]

Premises used: MulZeroClass.mul_zero, MvPowerSeries.coeff_monomial, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
this :
  ∀ {d : σ →₀ ℕ},
    Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
      ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)
d : σ →₀ ℕ
hd : d ≠ m
⊢ ¬p • m = p • d

Tactic:
simp [nsmul_right_inj hp, hd.symm]

Premises used: Ne.symm, nsmul_right_inj
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
simp :
  Eq.{u_3 + 1} (α := R)
    (∑ᶠ (d : σ →₀ ℕ),
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
simp₁ :
  ∀
    (this :
      ∀ {d : σ →₀ ℕ},
        Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
          ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)),
    Eq.{u_3 + 1} (α := R)
      (∑ᶠ (d : σ →₀ ℕ),
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
              R) :
        R)
      ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
simp₂ :
  ∀
    (this :
      ∀ {d : σ →₀ ℕ},
        Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
          ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)),
    HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
            (m.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
          R) =
      (coeff m : (a : MvPowerSeries σ R) → R) φ
simp₃ simp₄ :
  ∀
    (this :
      ∀ {d : σ →₀ ℕ},
        Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
          ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1))
    (x : σ →₀ ℕ),
    x ≠ m →
      HMul.hMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
              (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e) :
            R) =
        0
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff (p • m) : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
classical
  simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp), smul_eq_mul]
  have {d : σ →₀ ℕ} : (d.prod fun s e ↦ (X s (R := R) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
  rw [finsum_eq_single _ m]
  · rw [this, coeff_monomial, if_pos rfl, mul_one]
  · intro d hd
    rw [this, coeff_monomial, if_neg _, mul_zero]
    simp [nsmul_right_inj hp, hd.symm]

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_subst, if_pos, MulZeroClass.mul_zero, MvPowerSeries.HasSubst.X_pow, nsmul_right_inj, MvPowerSeries.coeff_monomial, smul_eq_mul, mul_one, if_neg, finsum_eq_single, MvPowerSeries.substAlgHom_apply, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
rw : ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
| ((constantCoeff : (a : MvPowerSeries σ R) → R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
    R)

Tactic:
rw [← coeff_zero_eq_constantCoeff, ← smul_zero p, coeff_expand_smul]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, smul_zero, MvPowerSeries.coeff_expand_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
conv_lhs :
  Eq.{u_3 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← smul_zero p, coeff_expand_smul]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, smul_zero, MvPowerSeries.coeff_expand_smul
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
⊢ Eq.{u_3 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
simp
-- 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! :
  ∀
    (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
⊢ 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:
contrapose! h
-- 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 :
  Ne.{u_3 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
⊢ 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

Tactic:
simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp)] at h

Premises used: MvPowerSeries.expand, MvPowerSeries.coeff_subst, MvPowerSeries.HasSubst.X_pow, MvPowerSeries.substAlgHom_apply
-- 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 :
  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
by_contra! :
  ∀
    (hc :
      ∀ (d : σ →₀ ℕ),
        Eq.{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)),
    False
⊢ ∃ (d : σ →₀ ℕ),
    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)

Tactic:
by_contra! hc
-- 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 :
  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
hc :
  ∀ (d : σ →₀ ℕ),
    Eq.{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)
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

Tactic:
simp [hc d]
-- 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 :
  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
hc :
  ∀ (d : σ →₀ ℕ),
    Eq.{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)
⊢ Ne.{u_3 + 1} (α := R) 0 0

Tactic:
rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h

Premises used: finsum_eq_zero_of_forall_eq_zero
-- 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 :
  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
hc :
  ∀ (d : σ →₀ ℕ),
    Eq.{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)
h₁ : Ne.{u_3 + 1} (α := R) 0 0
⊢ ∀ (d : σ →₀ ℕ),
    Eq.{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)

Tactic:
rw [finsum_eq_zero_of_forall_eq_zero fun d => by simp [hc d]] at h

Premises used: finsum_eq_zero_of_forall_eq_zero
-- 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 : Ne.{u_3 + 1} (α := R) 0 0
hc :
  ∀ (d : σ →₀ ℕ),
    Eq.{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)
⊢ False

Tactic:
contradiction
-- 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 :
  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
obtain :
  ∀ (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
⊢ p ∣ (m : (a : σ) → ℕ) i

Tactic:
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
-- 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 :
  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)
⊢ Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
simp [monomial_smul_eq]

Premises used: MvPowerSeries.monomial_smul_eq
-- 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 :
  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)
⊢ Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
have : (d.prod fun s e ↦ ((X s (R := R)) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
-- 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 :
  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)
⊢ Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0

Tactic:
rw [this, coeff_monomial] at hd

Premises used: MvPowerSeries.coeff_monomial
-- 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 :
  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)
hd₁ : Ne.{u_3 + 1} (α := R) (if m = p • d then 1 else 0) 0
⊢ Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
rw [this, coeff_monomial] at hd

Premises used: MvPowerSeries.coeff_monomial
-- 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 :
  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)
by_contra : ∀ (hc : ¬m = p • d), False
⊢ m = p • d

Tactic:
by_contra hc
-- 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 :
  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)
hc : ¬m = p • d
⊢ Ne.{u_3 + 1} (α := R) 0 0

Tactic:
rw [if_neg hc] at hd

Premises used: if_neg
-- 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 :
  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)
hc : ¬m = p • d
hd₁ : Ne.{u_3 + 1} (α := R) 0 0
⊢ Eq (α := MvPowerSeries σ R) (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ R) (X s) p ^ e)
    ((monomial (p • d) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
rw [if_neg hc] at hd

Premises used: if_neg
-- 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 :
  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)
hc : ¬m = p • d
hd₁ : Ne.{u_3 + 1} (α := R) 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)
⊢ ¬m = p • d

Tactic:
rw [if_neg hc] at hd

Premises used: if_neg
-- 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 :
  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) 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)
hc : ¬m = p • d
⊢ False

Tactic:
contradiction
-- 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 :
  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)
⊢ m = p • d

Tactic:
have meq : m = p • d := by
    by_contra hc
    rw [if_neg hc] at hd
    contradiction