awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
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 P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
have 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)
Tactic: rw [map_sub, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
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)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
have 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))
Tactic: rw [← this, coeff_subst', coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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))
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
have 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 : ℕ)))
Tactic: rw [← this, coeff_subst', coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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 : ℕ)))
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
have h₂ : HasSubst P.substInv
Tactic: rw [← this, coeff_subst', coeff_subst']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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)
⊢ 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))
have 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)
Tactic: congr! 3 with m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
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 : ℕ
⊢ 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)
have 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)
Tactic: generalize hB : (∑ i : Fin (n + 1), C (substInvFun P ↑i) * X ^ i.1) = B
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
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
have rw : ∀ m < n + 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (mk P.substInvFun - B) : R) (0 : R)
Tactic: rw [X_pow_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
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
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)
have this₁ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
n : ℕ
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
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (P.substInv ^ m) : R) ((coeff n : (a : R⟦X⟧) → R) (B ^ m) : R)
have 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)
Tactic: obtain ⟨Q, hQ⟩ := this.trans (sub_dvd_pow_sub_pow _ _ m)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
⊢ subst P P.substInv = X
have haveI : ∀ (this : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P.substInv : R)), subst P P.substInv = X
Tactic: haveI : Invertible (P.substInv.coeff 1) := by simpa using invertibleInvOf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
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
⊢ subst P P.substInv = X
have hQ : HasSubst Q
Tactic: have hQ : HasSubst Q := HasSubst.substInv P.substInv
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
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 P P.substInv = X
have eq_aux : subst Q P.substInv = X
Tactic: have eq_aux : P.substInv.subst Q = X := subst_substInv_right P.substInv P.constantCoeff_substInv
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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 P P.substInv = X
have suffices : Q = P
Tactic: suffices h : Q = P from by simp_rw [← h, eq_aux]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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)
have rw : Q = subst (R := R) Q X
Tactic: rw [subst_substInv_right _ hP, subst_X hQ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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
⊢ Q = subst Q (subst P.substInv P)
have rw₁ : Q = Q
Tactic: rw [subst_substInv_right _ hP, subst_X hQ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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 = P
have _ : Q = subst Q (subst P.substInv 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
inst_1 : Invertible (α := R) ((coeff 1 : (a : R⟦X⟧) → R) P : R)
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)
⊢ Q = P
have _₁ : subst Q (subst P.substInv P) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ (coeff 1 : (a : R⟦X⟧) → R) (P.substInvOfIsUnit hP') = (↑hP'.unit⁻¹ : R)
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ = (↑hP'.unit⁻¹ : R)
Tactic: rw [substInvOfIsUnit_eq_substInv, coeff_one_substInv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
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
⊢ subst (P.substInvOfIsUnit hP') P = X
have rw : subst P.substInv P = X
Tactic: rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_right hP]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
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
⊢ subst (P.substInvOfIsUnit hP') P = X
have rw₁ : Eq.{u_2 + 1} (α := MvPowerSeries Unit R) X X
Tactic: rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_right hP]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
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
⊢ subst P (P.substInvOfIsUnit hP') = X
have rw : subst P P.substInv = X
Tactic: rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_left hP]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
P : R⟦X⟧
hP : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) P : R) (0 : R)
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
⊢ subst P (P.substInvOfIsUnit hP') = X
have rw₁ : Eq.{u_2 + 1} (α := MvPowerSeries Unit R) X X
Tactic: rw [P.substInvOfIsUnit_eq_substInv hP', P.subst_substInv_left hP]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ (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)
have 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)
Tactic: rw [PowerSeries.subst, MvPowerSeries.coeff_subst
    (MvPowerSeries.hasSubst_of_constantCoeff_zero (fun _ ↦ by simp))]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (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)
have rw : HMul.hMul (β := R)
    (MvPolynomial.coeff e
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := MvPolynomial (Fin 2) R) (MvPolynomial.X 0) (MvPolynomial.X 1))
        ((single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ)) :
              (a : Unit) → ℕ)
            PUnit.unit :
          ℕ)))
    ((MvPowerSeries.coeff
            (single () (HAdd.hAdd (α := ℕ) (β := ℕ) ((e : (a : Fin 2) → ℕ) 0 : ℕ) ((e : (a : Fin 2) → ℕ) 1 : ℕ))) :
          (a : MvPowerSeries Unit R) → R)
        f :
      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: rw [finsum_eq_single _ (single () (e 0 + e 1)), mul_comm]