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)
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
⊢ 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)

Tactic:
simp [mul_assoc, coeff_X_pow_mul']

Premises used: mul_assoc, PowerSeries.coeff_X_pow_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)
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 : ℕ
⊢ 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)

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
simp_rw :
  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 ^ d) : R) -
        HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 1 then k else 0)))
    0
⊢ 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

Tactic:
simp_rw [mul_sub]

Premises used: mul_sub
-- 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
rw :
  HSub.hSub (α := R)
      (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
      (∑ᶠ (i : ℕ), HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R) (if i = 1 then k else 0)) =
    0
hf :
  Function.HasFiniteSupport.{0, u_2} (M := R) fun (d : ℕ) ↦
    HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R)
hg :
  Function.HasFiniteSupport.{0, u_2} (M := R) fun (d : ℕ) ↦
    HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 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 ^ d) : R) -
        HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 1 then k else 0)))
    0

Tactic:
rw [finsum_sub_distrib]

Premises used: finsum_sub_distrib
-- 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
simp :
  HSub.hSub (α := R)
      (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
      (∑ᶠ (i : ℕ), if i = 1 then HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R) k else 0) =
    0
⊢ HSub.hSub (α := R)
      (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
      (∑ᶠ (i : ℕ), HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R) (if i = 1 then k else 0)) =
    0

Tactic:
simp only [mul_ite, mul_zero]

Premises used: mul_ite, MulZeroClass.mul_zero
-- 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
nth_rw :
  (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) -
      if Eq (α := ℕ) 1 1 then HMul.hMul (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) k else 0) =
    0
ha : ∀ (x : ℕ), x ≠ 1 → (if x = 1 then HMul.hMul (α := R) ((coeff x : (a : R⟦X⟧) → R) P : R) k else 0) = 0
⊢ HSub.hSub (α := R)
      (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
      (∑ᶠ (i : ℕ), if i = 1 then HMul.hMul (α := R) ((coeff i : (a : R⟦X⟧) → R) P : R) k else 0) =
    0

Tactic:
nth_rw 2 [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)
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
simp :
  Eq (α := R)
    (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) :
      R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R)
⊢ (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) -
      if Eq (α := ℕ) 1 1 then HMul.hMul (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) k else 0) =
    0

Tactic:
simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_zero]

Premises used: sub_eq_zero, reduceIte, mul_invOf_cancel_left'
-- 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
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ᶠ (i : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R))
hb : HasSubst B
⊢ Eq (α := R)
    (∑ᶠ (i : ℕ),
        HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R) :
      R)
    ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : 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)
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)
    (∑ᶠ (i : ℕ),
      HMul.hMul (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) P : R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ i) : R))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R))

Tactic:
rfl
-- 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
⊢ HasSubst B

Tactic:
simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

Premises used: PowerSeries.HasSubst, PowerSeries.constantCoeff.eq_def
-- 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
⊢ ∀ (x : ℕ), x ≠ 1 → (if x = 1 then HMul.hMul (α := R) ((coeff x : (a : R⟦X⟧) → R) P : R) k else 0) = 0

Tactic:
simp +contextual
-- 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
⊢ Function.HasFiniteSupport.{0, u_2} (M := R) fun (d : ℕ) ↦
    HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R)

Tactic:
.subset (Set.finite_Iio (n + 3)) fun i ↦ ?_

Premises used: Function.HasFiniteSupport, Set.finite_Iio, Set.Finite.subset, HAdd.hAdd, 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
hf :
  ∀ (i : ℕ),
    Membership.mem (γ := Set ℕ)
        (Function.support.{0, u_2} (M := R) fun (d : ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R))
        i →
      i ∈ Set.Iio (n + 3)
⊢ Function.HasFiniteSupport.{0, u_2} (M := R) fun (d : ℕ) ↦
    HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R)

Tactic:
refine .subset (Set.finite_Iio (n + 3)) fun 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
i : ℕ
rwa rwa₁ rwa₂ rwa₃ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)
⊢ X ∣ B

Tactic:
rwa [X_dvd_iff]

Premises used: PowerSeries.X_dvd_iff
-- 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 : ℕ
hf :
  ∀ (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 : ℕ)) =
        X * B)
    (hB' : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (X * B) : R) (0 : 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 (X * B) P) : R) =
        k),
    Membership.mem (γ := Set ℕ)
        (Function.support.{0, u_2} (M := R) fun (d : ℕ) ↦
          HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
            ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) ((X * B) ^ d) : R))
        i →
      i ∈ Set.Iio (n + 3)
⊢ Membership.mem (γ := Set ℕ)
      (Function.support.{0, u_2} (M := R) fun (d : ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (B ^ d) : R))
      i →
    i ∈ Set.Iio (n + 3)

Tactic:
obtain ⟨B, rfl⟩ : X ∣ B := by rwa [X_dvd_iff]

Premises used: PowerSeries.X, rfl
-- 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 : ℕ
k : R
i : ℕ
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 : ℕ)) =
    X * B
hB' : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (X * B) : R) (0 : 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 (X * B) P) : R) =
    k
⊢ Membership.mem (γ := Set ℕ)
      (Function.support.{0, u_2} (M := R) fun (d : ℕ) ↦
        HMul.hMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
          ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) ((X * B) ^ d) : R))
      i →
    i ∈ Set.Iio (n + 3)

Tactic:
simp +contextual [mul_pow, coeff_X_pow_mul', Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff, PowerSeries.coeff_X_pow_mul', 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 : ℕ
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
x : ℕ
⊢ Membership.mem (γ := Set ℕ)
      (Function.support.{0, u_2} (M := R) fun (d : ℕ) ↦
        HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 1 then k else 0))
      x →
    Membership.mem (γ := Set ℕ) {1} x

Tactic:
simp +contextual
-- 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
⊢ Function.HasFiniteSupport.{0, u_2} (M := R) fun (d : ℕ) ↦
    HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 1 then k else 0)

Tactic:
exact .subset (Set.finite_singleton 1) (fun _ ↦ by simp +contextual)
-- 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)
⊢ 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)))

Tactic:
simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

Premises used: PowerSeries.HasSubst, PowerSeries.constantCoeff.eq_def
-- 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 : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
⊢ subst P.substInv P = X

Tactic:
ext 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)
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)

Tactic:
have := coeff_subst_sum_C_substInvFun_mul_X_pow_sub_X P hP 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)
n : ℕ
this :
  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)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → 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) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) X : R)

Tactic:
rw [map_sub, sub_eq_zero] at this

Premises used: map_sub, sub_eq_zero