awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
φ : MvPowerSeries σ S
⊢ Eq (α := MvPowerSeries τ S)
    ((expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        ((substAlgHom hf : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ) :
      MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
have rw : Eq (α := MvPowerSeries τ S)
  ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
  ((substAlgHom sorry : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
Tactic: rw [← AlgHom.comp_apply, expand_comp_substAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
S : Type u_4
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ S
hf : HasSubst f
φ : MvPowerSeries σ S
rw :
  Eq (α := MvPowerSeries τ S)
    ((AlgHom.comp (expand p hp) (substAlgHom hf) : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
⊢ Eq (α := MvPowerSeries τ S)
    ((expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        ((substAlgHom hf : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ) :
      MvPowerSeries τ S)
    ((substAlgHom ⋯ : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
have rw₁ : Eq (α := MvPowerSeries τ S) ((substAlgHom sorry : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
  ((substAlgHom sorry : (a : MvPowerSeries σ S) → MvPowerSeries τ S) φ : MvPowerSeries τ S)
Tactic: rw [← AlgHom.comp_apply, expand_comp_substAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (subst f φ) : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
have rw : Eq (α := MvPowerSeries τ R)
  ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R)
      ((substAlgHom hf : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ) :
    MvPowerSeries τ R)
  (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
Tactic: rw [← substAlgHom_apply hf, expand_substAlgHom, substAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
rw :
  Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R)
        ((substAlgHom hf : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ) :
      MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
⊢ Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (subst f φ) : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
have rw₁ : Eq (α := MvPowerSeries τ R) ((substAlgHom sorry : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ : MvPowerSeries τ R)
  (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
Tactic: rw [← substAlgHom_apply hf, expand_substAlgHom, substAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : σ → MvPowerSeries τ R
hf : HasSubst f
φ : MvPowerSeries σ R
rw :
  Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R)
        ((substAlgHom hf : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ) :
      MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
rw₁ :
  Eq (α := MvPowerSeries τ R) ((substAlgHom ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries τ R) φ : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
⊢ Eq (α := MvPowerSeries τ R)
    ((expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (subst f φ) : MvPowerSeries τ R)
    (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ : MvPowerSeries τ R)
have rw₂ : Eq (α := MvPowerSeries τ R) (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ)
  (subst (fun (i : σ) ↦ (expand p hp : (a : MvPowerSeries τ R) → MvPowerSeries τ R) (f i)) φ)
Tactic: rw [← substAlgHom_apply hf, expand_substAlgHom, substAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) (expand (p * q) ⋯) (AlgHom.comp (expand p hp) (expand q hq))
have H : ∀ (i : MvPowerSeries σ R),
  Eq (α := MvPowerSeries σ R) ((expand (p * q) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
    ((AlgHom.comp (expand p hp) (expand q hq) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) i : MvPowerSeries σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: simp only [expand, substAlgHom_apply, coeff_subst (HasSubst.X_pow hp), smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: have {d : σ →₀ ℕ} : (d.prod fun s e ↦ (X s (R := R) ^ p) ^ e) = monomial (p • d) 1 := by
    simp [monomial_smul_eq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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)
have 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) φ
Tactic: rw [finsum_eq_single _ m]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ
⊢ 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)
have 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
Tactic: rw [finsum_eq_single _ m]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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) φ
have 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) φ
Tactic: rw [this, coeff_monomial, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ
⊢ 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) φ
have 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) φ
Tactic: rw [this, coeff_monomial, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ
⊢ 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) φ
have rw₂ : HMul.hMul (α := R) (β := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (1 : R) =
  (coeff m : (a : MvPowerSeries σ R) → R) φ
Tactic: rw [this, coeff_monomial, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ
⊢ 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) φ
have rw₃ : Eq.{u_3 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: rw [this, coeff_monomial, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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
⊢ 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
have rw : ¬p • m = p • d
Tactic: rw [this, coeff_monomial, if_neg _, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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)
⊢ 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)
have 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) φ
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
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) φ
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
| ((constantCoeff : (a : MvPowerSeries σ R) → R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
    R)
have rw : ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff, ← smul_zero p, coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ 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)
have conv_lhs : Eq.{u_3 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
  ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← smul_zero p, coeff_expand_smul]