awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
f : MvPowerSeries σ R
a b : σ → R
⊢ Eq (α := MvPowerSeries σ R)
    ((rescale b : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
    ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale b : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
          MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a b : σ → R
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale (a * b)) (RingHom.comp (rescale b) (rescale a))
have a₁ : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp (rescale b) (rescale a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
⊢ (rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = r ^ n • f
have h : ∀ (e : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff e : (a : MvPowerSeries σ R) → R)
        ((rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff e : (a : MvPowerSeries σ R) → R) (r ^ n • f) : R)
Tactic: ext e
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff e : (a : MvPowerSeries σ R) → R)
        ((rescale (Function.const σ r) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff e : (a : MvPowerSeries σ R) → R) (r ^ n • f) : R)
have h : HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
    ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
Tactic: simp only [MvPowerSeries.coeff_rescale, map_smul, Finsupp.prod, Function.const_apply,
    Finset.prod_pow_eq_pow_sum, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
have pos : ∀ (he : e ∈ Function.support f),
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
Tactic: by_cases he : e ∈ f.support
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
pos :
  ∀ (he : e ∈ Function.support f),
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
        ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
      HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
have neg : ∀ (he : e ∉ Function.support f),
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
Tactic: by_cases he : e ∈ f.support
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
have pos : HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
    ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) e : ℕ))
    ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
Tactic: rw [← hf e he, Finsupp.degree_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : e ∈ Function.support f
pos :
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) r ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) e : ℕ))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
have pos₁ : HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
    ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
    ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
Tactic: rw [← hf e he, Finsupp.degree_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d = n
e : σ →₀ ℕ
he : e ∉ Function.support f
⊢ HMul.hMul (β := R) (HPow.hPow (β := ℕ) r (∑ i ∈ e.support, (e : (a : σ) → ℕ) i))
      ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (β := R) (r ^ n) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
have he₁ : f e = 0
Tactic: simp only [Function.mem_support, ne_eq, not_not] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b_1 : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a b : σ → R
⊢ rescale (a * b) = HMul.hMul (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale a) (rescale b)
have a₁ : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale (a * b) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((HMul.hMul (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale a) (rescale b) :
              (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            x :
          MvPowerSeries σ R) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
⊢ (rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f =
    subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f) : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale a : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f) : R)
have h : HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
  (coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f)
Tactic: rw [coeff_rescale]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    (coeff n : (a : MvPowerSeries σ R) → R) (subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X) f)
have h : HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
  ∑
    i ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
              R))
        sorry,
    HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (i.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
        R)
Tactic: rw [coeff_subst (HasSubst.smul_X a),
    finsum_eq_sum _ (coeff_subst_finite (HasSubst.smul_X a) f n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
                R))
          ⋯,
      HSMul.hSMul (α := R) (β := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (i.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X s ^ e) :
          R)
have h : HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
  ∑
    d ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        sorry,
    HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R)
Tactic: simp only [Pi.smul_apply', smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      d ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R)
have h : HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
  HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
      R)
Tactic: rw [Finset.sum_eq_single n _ _]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R)
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      d ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R)
have rw : ∀
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      sorry,
  b ≠ n →
    HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R) =
      0
Tactic: rw [Finset.sum_eq_single n _ _]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R)
rw :
  ∀
    b ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
            ((coeff n : (a : MvPowerSeries σ R) → R)
                (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
              R))
        ⋯,
    b ≠ n →
      HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R) =
        0
⊢ HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) f : R) =
    ∑
      d ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
              ((coeff n : (a : MvPowerSeries σ R) → R)
                  (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
                R))
          ⋯,
      HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries σ R) → R)
            (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
          R)
have rw₁ : n ∉
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      sorry →
  HMul.hMul (α := R) (β := R) ((coeff n : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (n.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0
Tactic: rw [Finset.sum_eq_single n _ _]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb :
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
hbn : b ≠ n
⊢ HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0
have rw : HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((monomial b : (a : R) → MvPowerSeries σ R) (b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
      R) =
  0
Tactic: rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb :
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
hbn : b ≠ n
rw :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((monomial b : (a : R) → MvPowerSeries σ R) (b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
        R) =
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0
have rw₁ : HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
    (if n = b then b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n else 0 : R) =
  0
Tactic: rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb :
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
hbn : b ≠ n
rw :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((monomial b : (a : R) → MvPowerSeries σ R) (b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
        R) =
    0
rw₁ :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      (if n = b then b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n else 0 : R) =
    0
⊢ HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0
have rw₂ : HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
Tactic: rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
f : MvPowerSeries σ R
n b : σ →₀ ℕ
hb :
  b ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_1, u_3} (M := R) fun (d : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries σ R) → R)
              (d.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
            R))
      ⋯
hbn : b ≠ n
rw :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((monomial b : (a : R) → MvPowerSeries σ R) (b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n)) :
        R) =
    0
rw₁ :
  HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      (if n = b then b.prod fun (s : σ) (n : ℕ) ↦ a s ^ n else 0 : R) =
    0
rw₂ : HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (b.prod fun (s : σ) (e : ℕ) ↦ HSMul.hSMul (β := MvPowerSeries σ R) (a s) (X s) ^ e) :
        R) =
    0
have rw₃ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [← monomial_eq, coeff_monomial, if_neg (Ne.symm hbn), mul_zero]