awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (subst
          (HSMul.hSMul (β := MvPowerSeries σ R) a
            ((Polynomial.aeval p : (a : Polynomial R) → MvPowerSeries σ R) Polynomial.X : MvPowerSeries σ R))
          f) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw₃ : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst
        (fun (s : Unit) ↦
          MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
        f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (subst
          (HSMul.hSMul (β := MvPowerSeries σ R) a
            ((Polynomial.aeval p : (a : Polynomial R) → MvPowerSeries σ R) Polynomial.X : MvPowerSeries σ R))
          f) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₃ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw₄ : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst
        (fun (s : Unit) ↦ (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) p)
        f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₂ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (subst
          (HSMul.hSMul (β := MvPowerSeries σ R) a
            ((Polynomial.aeval p : (a : Polynomial R) → MvPowerSeries σ R) Polynomial.X : MvPowerSeries σ R))
          f) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₃ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₄ :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) p)
          f) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw₅ : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • p) f) : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst (fun (s : Unit) ↦ HPow.hPow (β := ℕ) a 1 • p) f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (n + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have zero : Eq (α := R)
  ((coeff 0 : (a : R⟦X⟧) → R)
      (HSub.hSub (α := MvPowerSeries Unit R)
        (subst
          (∑ i : Fin (0 + 1),
            HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
              (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
          P)
        X) :
    R)
  (0 : R)
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
zero :
  Eq (α := R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (n + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have succ : Eq (α := R)
  ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
      (HSub.hSub (α := MvPowerSeries Unit R)
        (subst
          (∑ i : Fin (0 + 1 + 1),
            HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
              (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
          P)
        X) :
    R)
  (0 : R)
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
zero :
  Eq (α := R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
succ :
  Eq (α := R)
    ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (n + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have succ₁ : ∀ (n : ℕ),
  Eq (α := R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (n + 1 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
Tactic: obtain (_ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ Eq (α := R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have zero : HSub.hSub (α := R) (β := R)
    (∑ᶠ (d : ℕ),
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
          ((coeff 0 : (a : R⟦X⟧) → R)
              (HPow.hPow (α := R⟦X⟧)
                (∑ i : Fin (0 + 1),
                  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                    (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                d) :
            R) :
      R)
    ((coeff 0 : (a : R⟦X⟧) → R) X : R) =
  0
Tactic: rw [map_sub, coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
zero :
  HSub.hSub (α := R) (β := R)
      (∑ᶠ (d : ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff 0 : (a : R⟦X⟧) → R)
                (HPow.hPow (α := R⟦X⟧)
                  (∑ i : Fin (0 + 1),
                    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                      (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                  d) :
              R) :
        R)
      ((coeff 0 : (a : R⟦X⟧) → R) X : R) =
    0
⊢ Eq (α := R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have zero₁ : HasSubst.{0, u_2} (τ := Unit) (S := R)
  (∑ i : Fin (0 + 1),
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
Tactic: rw [map_sub, coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ Eq (α := R)
    ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have succ : HSub.hSub (α := R) (β := R)
    (∑ᶠ (d : ℕ),
        HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
          ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
              (HPow.hPow (α := R⟦X⟧)
                (∑ i : Fin (0 + 1 + 1),
                  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                    (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                d) :
            R) :
      R)
    ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
  0
Tactic: rw [map_sub, coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
succ :
  HSub.hSub (α := R) (β := R)
      (∑ᶠ (d : ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
                (HPow.hPow (α := R⟦X⟧)
                  (∑ i : Fin (0 + 1 + 1),
                    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                      (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                  d) :
              R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
    0
⊢ Eq (α := R)
    ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (0 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have succ₁ : HasSubst.{0, u_2} (τ := Unit) (S := R)
  (∑ i : Fin (0 + 1 + 1),
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
Tactic: rw [map_sub, coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ HSub.hSub (α := R) (β := R)
      (∑ᶠ (d : ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
                (HPow.hPow (α := R⟦X⟧)
                  (∑ i : Fin (0 + 1 + 1),
                    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                      (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                  d) :
              R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
    0
have succ : HSub.hSub (β := R)
    (HSMul.hSMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
      ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
          (HPow.hPow (α := R⟦X⟧) (β := ℕ)
            (∑ i : Fin (0 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            1) :
        R))
    ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
  0
Tactic: rw [finsum_eq_single (a := 1)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
succ :
  HSub.hSub (β := R)
      (HSMul.hSMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
        ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
            (HPow.hPow (α := R⟦X⟧) (β := ℕ)
              (∑ i : Fin (0 + 1 + 1),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
              1) :
          R))
      ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
    0
⊢ HSub.hSub (α := R) (β := R)
      (∑ᶠ (d : ℕ),
          HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
                (HPow.hPow (α := R⟦X⟧)
                  (∑ i : Fin (0 + 1 + 1),
                    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                      (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                  d) :
              R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R) X : R) =
    0
have succ₁ : ∀ (x : ℕ),
  x ≠ 1 →
    HSMul.hSMul (α := R) (β := R) ((coeff x : (a : R⟦X⟧) → R) P : R)
        ((coeff (HAdd.hAdd (α := ℕ) 0 1) : (a : R⟦X⟧) → R)
            (HPow.hPow (α := R⟦X⟧)
              (∑ i : Fin (0 + 1 + 1),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
              x) :
          R) =
      0
Tactic: rw [finsum_eq_single (a := 1)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
⊢ Eq (α := R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        (HSub.hSub (α := MvPowerSeries Unit R)
          (subst
            (∑ i : Fin (n + 1 + 1 + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            P)
          X) :
      R)
    (0 : R)
have succ : Eq (α := R)
  ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      (subst
          (∑ i : Fin (n + 2),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i.castSucc : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i.castSucc : ℕ)) +
            HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑(Fin.last (n + 2)) : ℕ)) : R⟦X⟧)
              (HPow.hPow (α := R⟦X⟧) X (↑(Fin.last (n + 2)) : ℕ)))
          P -
        X) :
    R)
  (0 : R)
Tactic: rw [Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
⊢ Eq (α := R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        (subst
            (∑ i : Fin (n + 2),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i.castSucc : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑i.castSucc : ℕ)) +
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑(Fin.last (n + 2)) : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑(Fin.last (n + 2)) : ℕ)))
            P -
          X) :
      R)
    (0 : R)
have succ : HSub.hSub (α := R) (β := R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        (subst
          (∑ x : Fin (n + 2),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑x : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑x : ℕ)) +
            HMul.hMul (α := R⟦X⟧)
              ((C : (a : R) → R⟦X⟧)
                  (HMul.hMul (α := R) (β := R)
                    (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
                    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
                        (subst
                          (∑ i : Fin (n + 1 + 1),
                            HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                              (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                          P) :
                      R)) :
                R⟦X⟧)
              (HPow.hPow (α := R⟦X⟧) X (n + 2)))
          P) :
      R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
  0
Tactic: simp only [Fin.val_castSucc, Fin.val_last, map_sub, substInvFun]