awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((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))) ^
              d) :
          R))
    0
succ₁ :
  HasSubst
    (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)))
⊢ 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)

Tactic:
rw [coeff_subst']

Premises used: 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)
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.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((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))) ^
              d) :
          R))
    0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((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))) ^
              d) :
          R))
    0

Tactic:
simp only [smul_eq_mul, ← map_mul]

Premises used: map_mul, smul_eq_mul
-- 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 :
  ∀ (k : R)
    (hk :
      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) =
        k),
    Eq.{u_2 + 1} (α := R)
      (∑ᶠ (d : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
              ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ d) :
            R))
      0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((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))) ^
              d) :
          R))
    0

Tactic:
generalize hk : ⅟(P.coeff 1) * coeff (n + 1 + 1) (subst B P) = k

Premises used: PowerSeries.subst, PowerSeries.coeff, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- 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)
k : R
hk :
  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) =
    k
trans :
  Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ d) :
          R))
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R) (if d = 1 then k else 0)))
trans₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R) (if d = 1 then k else 0)))
    0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ d) :
          R))
    0

Tactic:
trans ∑ᶠ d, P.coeff d * (coeff (n + 1 + 1) (B ^ d) - if d = 1 then k else 0)
-- 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)
k : R
hk :
  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) =
    k
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ d) :
          R))
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R) (if d = 1 then k else 0)))

Tactic:
finsum_congr fun i ↦ ?_

Premises used: finsum_congr
-- 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)
k : R
hk :
  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) =
    k
refine :
  ∀ (i : ℕ),
    HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ i) :
          R) =
      HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
        (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) (if i = 1 then k else 0))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
            ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ d) :
          R))
    (∑ᶠ (d : ℕ),
      HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R) (if d = 1 then k else 0)))

Tactic:
refine finsum_congr fun i ↦ ?_

Premises used: finsum_congr
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
e_a :
  (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ i) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) (if i = 1 then k else 0)
⊢ HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ i) :
        R) =
    HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
      (HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) (if i = 1 then k else 0))

Tactic:
congr 1
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
e_a :
  (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2)))
        0) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) B 0) : R)
      (if Eq (α := ℕ) 0 1 then k else 0)
e_a₁ :
  (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^
        HAdd.hAdd (α := ℕ) 0 1) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ HAdd.hAdd (α := ℕ) 0 1) : R)
      (if HAdd.hAdd (α := ℕ) 0 1 = 1 then k else 0)
e_a₂ :
  ∀ (i : ℕ),
    (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
        ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 1 + 1)) =
      HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ (i + 1 + 1)) : R) (if i + 1 + 1 = 1 then k else 0)
⊢ (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ i) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) (if i = 1 then k else 0)

Tactic:
obtain (_ | _ | i) := i
-- 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)
k : R
hk :
  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) =
    k
⊢ (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2)))
        0) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) B 0) : R)
      (if Eq (α := ℕ) 0 1 then k else 0)

Tactic:
simp
-- 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)
k : R
hk :
  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) =
    k
⊢ (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^
        HAdd.hAdd (α := ℕ) 0 1) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ HAdd.hAdd (α := ℕ) 0 1) : R)
      (if HAdd.hAdd (α := ℕ) 0 1 = 1 then k else 0)

Tactic:
simp [← sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
e_a :
  (coeff (n + 2) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 2)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
⊢ (coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 1 + 1)) =
    HSub.hSub (α := R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ (i + 1 + 1)) : R) (if i + 1 + 1 = 1 then k else 0)

Tactic:
simp only [add_assoc, Nat.reduceAdd]

Premises used: add_assoc, Nat.reduceAdd
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
e_a :
  (coeff (n + 2) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) 0 *
          B ^ (i + 2 - 0) *
        (↑((i + 2).choose 0) : R⟦X⟧)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
e_a₁ :
  ∀ b ∈ Finset.range (i + 2 + 1),
    b ≠ 0 →
      Eq (α := R)
        ((coeff (n + 2) : (a : R⟦X⟧) → R)
            ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ b *
                B ^ (i + 2 - b) *
              (↑((i + 2).choose b) : R⟦X⟧)) :
          R)
        (0 : R)
e_a₂ :
  0 ∉ Finset.range (i + 2 + 1) →
    Eq (α := R)
      ((coeff (n + 2) : (a : R⟦X⟧) → R)
          (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2)))
                0 *
              B ^ (i + 2 - 0) *
            (↑((i + 2).choose 0) : R⟦X⟧)) :
        R)
      (0 : R)
⊢ (coeff (n + 2) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 2)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)

Tactic:
rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 0)]

Premises used: map_sum, add_comm, Finset.sum_eq_single, add_pow, OfNat.ofNat
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
⊢ (coeff (n + 2) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) 0 *
          B ^ (i + 2 - 0) *
        (↑((i + 2).choose 0) : R⟦X⟧)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)

Tactic:
simp
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
hj : 0 ∈ Finset.range (i + 2 + 1)
hj' : Ne (α := ℕ) 0 0
⊢ Eq (α := R)
    ((coeff (n + 2) : (a : R⟦X⟧) → R)
        (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2)))
              0 *
            B ^ (i + 2 - 0) *
          (↑((i + 2).choose 0) : R⟦X⟧)) :
      R)
    (0 : R)

Tactic:
simp at hj'
-- 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)
k : R
hk :
  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) =
    k
i : ℕ
hj : HAdd.hAdd (α := ℕ) 0 1 ∈ Finset.range (i + 2 + 1)
hj' : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ Eq (α := R)
    ((coeff (n + 2) : (a : R⟦X⟧) → R)
        ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^
              HAdd.hAdd (α := ℕ) 0 1 *
            B ^ (i + 2 - HAdd.hAdd (α := ℕ) 0 1) *
          (↑((i + 2).choose (HAdd.hAdd (α := ℕ) 0 1)) : R⟦X⟧)) :
      R)
    (0 : R)

Tactic:
simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']

Premises used: mul_assoc, PowerSeries.C, mul_comm, PowerSeries.coeff_X_pow_mul', DFunLike.coe
-- 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)
k : R
hk :
  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) =
    k
i j : ℕ
hj : j + 1 + 1 ∈ Finset.range (i + 2 + 1)
hj' : j + 1 + 1 ≠ 0
e_a :
  Eq (α := R)
    ((coeff (n + 2) : (a : R⟦X⟧) → R)
        (HPow.hPow (α := R⟦X⟧) X ((n + 2) * (j + 1 + 1)) *
              HPow.hPow (α := R⟦X⟧) (-(C : (a : R) → R⟦X⟧) k : R⟦X⟧) (j + 1 + 1) *
            B ^ (i + 2 - (j + 1 + 1)) *
          (↑((i + 2).choose (j + 1 + 1)) : R⟦X⟧)) :
      R)
    (0 : R)
⊢ Eq (α := R)
    ((coeff (n + 2) : (a : R⟦X⟧) → R)
        ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (j + 1 + 1) *
            B ^ (i + 2 - (j + 1 + 1)) *
          (↑((i + 2).choose (j + 1 + 1)) : R⟦X⟧)) :
      R)
    (0 : R)

Tactic:
rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]

Premises used: pow_mul, HPow.hPow, mul_comm, neg_mul, mul_pow