awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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⟧
this : p 0 ≠ 0 → Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (1 : ℕ)
⊢ p 0 = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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⟧
⊢ HasSubst p

Tactic:
have hp : PowerSeries.HasSubst p := by
    apply HasSubst.of_constantCoeff_zero
    rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply]
    have : (p 0 ≠ 0) → (0 : σ →₀ ℕ).degree = 1 := hp_lin 0
    grind
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
rw :
  subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f =
    MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X)
      (subst p f)
⊢ subst (R := R) p ((rescale a : (a : R⟦X⟧) → R⟦X⟧) f) =
    (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (subst p f)

Tactic:
rw [rescale_eq_subst, MvPowerSeries.rescale_eq_subst,
    subst_comp_subst_apply (HasSubst.smul_X' a) hp]

Premises used: PowerSeries.rescale_eq_subst, PowerSeries.HasSubst.smul_X', PowerSeries.subst_comp_subst_apply, MvPowerSeries.rescale_eq_subst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
rw :
  ∀ (n : σ →₀ ℕ),
    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)
⊢ subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f =
    MvPowerSeries.subst (R := R) (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X)
      (MvPowerSeries.subst (fun (x : Unit) ↦ p) f)

Tactic:
rw [MvPowerSeries.subst_comp_subst_apply hp.const (MvPowerSeries.HasSubst.smul_X _),
    MvPowerSeries.ext_iff]

Premises used: MvPowerSeries.subst_comp_subst_apply, MvPowerSeries.ext_iff, MvPowerSeries.HasSubst.smul_X, PowerSeries.HasSubst.const
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
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)
⊢ 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)

Tactic:
obtain (_ | _ | n) := n
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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 : ℕ)))
⊢ 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:
rw [map_sub, coeff_subst']

Premises used: map_sub, PowerSeries.coeff_subst'
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 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:
simp +contextual [finsum_eq_single (a := 0), substInvFun, zero_pow_eq, hP]

Premises used: PowerSeries.substInvFun, zero_pow_eq, OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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:
simp [substInvFun, HasSubst]

Premises used: PowerSeries.HasSubst, PowerSeries.substInvFun
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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 : ℕ)))
⊢ 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:
rw [map_sub, coeff_subst']

Premises used: map_sub, PowerSeries.coeff_subst'
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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
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
⊢ 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 [finsum_eq_single (a := 1)]

Premises used: OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
      (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:
simp [substInvFun]

Premises used: PowerSeries.substInvFun
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
h : Ne (α := ℕ) 0 1
⊢ HSMul.hSMul (α := R) (β := R) ((coeff 0 : (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 : ℕ)))
            0) :
        R) =
    0

Tactic:
simp_all [substInvFun, mul_pow, coeff_mul_X_pow']

Premises used: PowerSeries.substInvFun, PowerSeries.coeff_mul_X_pow', mul_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 1
⊢ HSMul.hSMul (α := R) (β := R) ((coeff (HAdd.hAdd (α := ℕ) 0 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 : ℕ)))
            (HAdd.hAdd (α := ℕ) 0 1)) :
        R) =
    0

Tactic:
simp_all [substInvFun, mul_pow, coeff_mul_X_pow']

Premises used: PowerSeries.substInvFun, PowerSeries.coeff_mul_X_pow', mul_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
h : n + 1 + 1 ≠ 1
⊢ HSMul.hSMul (α := R) (β := R) ((coeff (n + 1 + 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 : ℕ)))
            (n + 1 + 1)) :
        R) =
    0

Tactic:
simp_all [substInvFun, mul_pow, coeff_mul_X_pow']

Premises used: PowerSeries.substInvFun, PowerSeries.coeff_mul_X_pow', mul_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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)
⊢ 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:
simp [HasSubst, X, substInvFun]

Premises used: PowerSeries.HasSubst, PowerSeries.X, PowerSeries.substInvFun
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
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)
⊢ 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:
rw [Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
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
⊢ 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:
simp only [Fin.val_castSucc, Fin.val_last, map_sub, substInvFun]

Premises used: map_sub, PowerSeries.substInvFun, Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
succ :
  ∀ (B : R⟦X⟧)
    (hB :
      ∑ i : Fin (n + 2),
          HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
            (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
        B),
    HSub.hSub (α := R) (β := R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            (subst
              (B +
                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 B P) : R)) :
                    R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (n + 2)))
              P) :
          R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
      0
⊢ 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:
generalize hB : ∑ i : Fin (n + 2), C (substInvFun P i) * X ^ i.1 = B

Premises used: PowerSeries.X, HAdd.hAdd, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 2),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)

Tactic:
simp [← hB, zero_pow_eq, substInvFun]

Premises used: PowerSeries.substInvFun, zero_pow_eq
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 2),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)

Tactic:
have hB' : B.constantCoeff = 0 := by simp [← hB, zero_pow_eq, substInvFun]
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
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 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 2),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
hB' : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)
succ :
  Eq (α := R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        (subst
          (B +
            -(HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧)
                  ((C : (a : R) → R⟦X⟧)
                      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R) :
                    R⟦X⟧)
                  ((C : (a : R) → R⟦X⟧) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R) : R⟦X⟧) *
                HPow.hPow (α := R⟦X⟧) X (n + 2)))
          P) :
      R)
    (0 : R)
⊢ HSub.hSub (α := R) (β := R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          (subst
            (B +
              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 B 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 [neg_mul, map_neg, map_mul, coeff_X, Nat.add_eq_right, Nat.add_eq_zero_iff,
      one_ne_zero, and_false, ↓reduceIte, sub_zero]

Premises used: Nat.add_eq_right, sub_zero, map_neg, map_mul, PowerSeries.coeff_X, reduceIte, neg_mul, and_false, one_ne_zero, Nat.add_eq_zero_iff