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 : ℕ
this :
  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)
h :
  Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ d) : R))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff n : (a : R⟦X⟧) → R)
            (HPow.hPow (α := R⟦X⟧)
              (∑ i : Fin (n + 1),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
              d) :
          R))
h₁ :
  HasSubst.{0, u_2} (τ := Unit) (S := R)
    (∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
h₂ : HasSubst P.substInv
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)

Tactic:
rw [← this, coeff_subst', 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 : ℕ
this :
  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)
h :
  ∀ (m : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R)
      ((coeff n : (a : R⟦X⟧) → R)
          (HPow.hPow (α := R⟦X⟧)
            (∑ i : Fin (n + 1),
              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
            m) :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ d) : R))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := R) ((coeff d : (a : R⟦X⟧) → R) P : R)
        ((coeff n : (a : R⟦X⟧) → R)
            (HPow.hPow (α := R⟦X⟧)
              (∑ i : Fin (n + 1),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
              d) :
          R))

Tactic:
congr! 3 with m
-- 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)
        (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)
m : ℕ
h :
  ∀ (B : R⟦X⟧)
    (hB :
      ∑ i : Fin (n + 1),
          HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
            (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
        B),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HPow.hPow (α := R⟦X⟧)
          (∑ i : Fin (n + 1),
            HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
              (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
          m) :
      R)

Tactic:
generalize hB : (∑ i : Fin (n + 1), C (substInvFun P ↑i) * X ^ i.1) = B

Premises used: HMul.hMul, Finset.univ, PowerSeries.X, Fin.val, PowerSeries.C, PowerSeries.substInvFun, HPow.hPow, DFunLike.coe, Finset.sum
-- 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)
        (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)
m : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
rw : ∀ m < n + 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (mk P.substInvFun - B) : R) (0 : R)
⊢ HPow.hPow (α := R⟦X⟧) X (n + 1) ∣ mk P.substInvFun - B

Tactic:
rw [X_pow_dvd_iff]

Premises used: PowerSeries.X_pow_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 : ℕ
this :
  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)
m_1 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
m : ℕ
hm : m < n + 1
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (mk P.substInvFun - B) : R) (0 : R)

Tactic:
simp +contextual [← hB, coeff_X_pow, Finset.sum_eq_single (⟨m, hm⟩ : Fin (n + 1)),
        Fin.ext_iff, @eq_comm _ m]

Premises used: Fin.ext_iff, Fin.mk, eq_comm, Finset.sum_eq_single, PowerSeries.coeff_X_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 : ℕ
this :
  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)
m : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
⊢ HPow.hPow (α := R⟦X⟧) X (n + 1) ∣ mk P.substInvFun - B

Tactic:
have : X ^ (n + 1) ∣ mk (substInvFun P) - B := by
      rw [X_pow_dvd_iff]
      intro m hm
      simp +contextual [← hB, coeff_X_pow, Finset.sum_eq_single (⟨m, hm⟩ : Fin (n + 1)),
        Fin.ext_iff, @eq_comm _ m]
-- 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_1 :
  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)
m : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
this : HPow.hPow (α := R⟦X⟧) X (n + 1) ∣ mk P.substInvFun - B
h :
  ∀ (Q : R⟦X⟧) (hQ : mk P.substInvFun ^ m - B ^ m = HPow.hPow (α := R⟦X⟧) X (n + 1) * Q),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)

Tactic:
obtain ⟨Q, hQ⟩ := this.trans (sub_dvd_pow_sub_pow _ _ m)

Premises used: sub_dvd_pow_sub_pow, Dvd.dvd.trans
-- 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_1 :
  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)
m : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 1),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
this : HPow.hPow (α := R⟦X⟧) X (n + 1) ∣ mk P.substInvFun - B
Q : R⟦X⟧
hQ : mk P.substInvFun ^ m - B ^ m = HPow.hPow (α := R⟦X⟧) X (n + 1) * Q
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)

Tactic:
simp [substInv, sub_eq_iff_eq_add.mp hQ, coeff_X_pow_mul']

Premises used: PowerSeries.substInv, sub_eq_iff_eq_add, Iff.mp, 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 : ℕ
this :
  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)
⊢ HasSubst.{0, u_2} (τ := Unit) (S := R)
    (∑ i : Fin (n + 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, zero_pow_eq, C, substInvFun]

Premises used: PowerSeries.HasSubst, PowerSeries.X, PowerSeries.C, 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 : ℕ
this :
  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)
⊢ HasSubst P.substInv

Tactic:
simp [HasSubst, ← constantCoeff.eq_def, substInvFun, substInv]

Premises used: PowerSeries.HasSubst, PowerSeries.substInv, PowerSeries.constantCoeff.eq_def, PowerSeries.substInvFun
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P.substInv : R) (0 : R)

Tactic:
simp [substInv, substInvFun]

Premises used: PowerSeries.substInv, PowerSeries.substInvFun
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ HasSubst P.substInv

Tactic:
simp [HasSubst, ← constantCoeff.eq_def]

Premises used: PowerSeries.HasSubst, PowerSeries.constantCoeff.eq_def
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ Eq (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)

Tactic:
simp [substInv, substInvFun]

Premises used: PowerSeries.substInv, 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)
⊢ Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)

Tactic:
simpa using invertibleInvOf

Premises used: invertibleInvOf
-- 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)
haveI : ∀ (this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)), subst P P.substInv = X
⊢ subst P P.substInv = X

Tactic:
haveI : Invertible (P.substInv.coeff 1) := by simpa using invertibleInvOf
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
⊢ HasSubst Q

Tactic:
have hQ : HasSubst Q := HasSubst.substInv P.substInv
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
⊢ subst Q P.substInv = X

Tactic:
have eq_aux : P.substInv.subst Q = X := subst_substInv_right P.substInv P.constantCoeff_substInv
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
h : Q = P
simp_rw : subst Q P.substInv = X
⊢ subst P P.substInv = X

Tactic:
simp_rw [← h, eq_aux]
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
suffices : Q = P
⊢ subst P P.substInv = X

Tactic:
suffices h : Q = P from by simp_rw [← h, eq_aux]
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
rw : Q = subst (R := R) Q X
rw₁ rw₂ : Q = Q
⊢ Q = subst Q (subst P.substInv P)

Tactic:
rw [subst_substInv_right _ hP, subst_X hQ]

Premises used: PowerSeries.subst_substInv_right, PowerSeries.subst_X
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ subst Q (subst P.substInv P) = P

Tactic:
simp [subst_comp_subst_apply (HasSubst.substInv P) hQ, eq_aux]

Premises used: PowerSeries.subst_comp_subst_apply, PowerSeries.HasSubst.substInv
-- 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)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
_ : Q = subst Q (subst P.substInv P)
_₁ : subst Q (subst P.substInv P) = P
⊢ Q = P

Tactic:
calc
    _ = PowerSeries.subst Q (P.subst P.substInv) := by
      rw [subst_substInv_right _ hP, subst_X hQ]
    _ = P := by
      simp [subst_comp_subst_apply (HasSubst.substInv P) hQ, eq_aux]

Premises used: PowerSeries.substInv, PowerSeries.subst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ P.substInvOfIsUnit hP' = P.substInv

Tactic:
rfl

Premises used: PowerSeries.substInvOfIsUnit, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (P.substInvOfIsUnit hP') : R) (0 : R)

Tactic:
simp [substInvOfIsUnit_eq_substInv]

Premises used: PowerSeries.substInvOfIsUnit_eq_substInv
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ HasSubst (P.substInvOfIsUnit hP')

Tactic:
simp [HasSubst, ← constantCoeff.eq_def]

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' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) := hP'.invertible
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ = (↑hP'.unit⁻¹ : R)
⊢ (coeff 1 : (a : R⟦X⟧) → R) (P.substInvOfIsUnit hP') = (↑hP'.unit⁻¹ : R)

Tactic:
rw [substInvOfIsUnit_eq_substInv, coeff_one_substInv]

Premises used: PowerSeries.coeff_one_substInv, PowerSeries.substInvOfIsUnit_eq_substInv
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) := hP'.invertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ = (↑hP'.unit⁻¹ : R)

Tactic:
Units.mul_eq_one_iff_eq_inv.mp Invertible.invOf_mul_self

Premises used: Invertible.invOf_mul_self, Units.mul_eq_one_iff_eq_inv, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) := hP'.invertible
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ = (↑hP'.unit⁻¹ : R)

Tactic:
exact Units.mul_eq_one_iff_eq_inv.mp Invertible.invOf_mul_self

Premises used: Invertible.invOf_mul_self, Units.mul_eq_one_iff_eq_inv, Iff.mp
-- 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)
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) := hP'.invertible
rw : subst P.substInv P = X
rw₁ rw₂ : Eq.{u_2 + 1} (α := MvPowerSeries Unit R) X X
⊢ subst (P.substInvOfIsUnit hP') P = X

Tactic:
rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_right hP]

Premises used: PowerSeries.subst_substInv_right, PowerSeries.substInvOfIsUnit_eq_substInv
-- 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)
hP' : IsUnit (M := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R) := hP'.invertible
rw : subst P P.substInv = X
rw₁ rw₂ : Eq.{u_2 + 1} (α := MvPowerSeries Unit R) X X
⊢ subst P (P.substInvOfIsUnit hP') = X

Tactic:
rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_left hP]

Premises used: PowerSeries.substInvOfIsUnit_eq_substInv, PowerSeries.subst_substInv_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
x : Unit
⊢ Eq (α := R)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries (Fin 2) R) → R)
        (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
rw :
  ∑ᶠ (d : Unit →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
            (d.prod fun (s : Unit) (e : ℕ) ↦ HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ ^ e) :
          R) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)
⊢ (MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
      (subst (HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁) f) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)

Tactic:
rw [PowerSeries.subst, MvPowerSeries.coeff_subst
    (MvPowerSeries.hasSubst_of_constantCoeff_zero (fun _ ↦ by simp))]

Premises used: MvPowerSeries.hasSubst_of_constantCoeff_zero, PowerSeries.subst, MvPowerSeries.coeff_subst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
simp_rw :
  ∑ᶠ (d : Unit →₀ ℕ),
      HMul.hMul (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        (MvPolynomial.coeff e
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
            ((d : (a : Unit) → ℕ) PUnit.unit : ℕ))) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      HSMul.hSMul (α := R) (β := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries (Fin 2) R) → R)
            (d.prod fun (s : Unit) (e : ℕ) ↦ HAdd.hAdd (α := MvPowerSeries (Fin 2) R) X₀ X₁ ^ e) :
          R) =
    HMul.hMul (α := R) (β := R)
      ((↑((HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)).choose
              ((e : (a : Fin 2) → ℕ) 0)) :
          R) :
        R)
      ((coeff (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
            (a : R⟦X⟧) → R)
          f :
        R)

Tactic:
simp_rw [Finsupp.prod_pow, univ_unique, PUnit.default_eq_unit, prod_singleton,
    smul_eq_mul, ← MvPolynomial.coe_X, ← MvPolynomial.coe_add, ← MvPolynomial.coe_pow,
    MvPolynomial.coeff_coe]

Premises used: Finset.prod_singleton, MvPolynomial.coe_X, Finset.univ_unique, MvPolynomial.coeff_coe, MvPolynomial.coe_add, Finsupp.prod_pow, MvPolynomial.coe_pow, PUnit.default_eq_unit, smul_eq_mul