awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
⊢ HSub.hSub (α := R) (β := R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          (subst
            (∑ x : Fin (n + 2),
                HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑x : ℕ)) : R⟦X⟧)
                  (HPow.hPow (α := R⟦X⟧) X (↑x : ℕ)) +
              HMul.hMul (α := R⟦X⟧)
                ((C : (a : R) → R⟦X⟧)
                    (HMul.hMul (α := R) (β := R)
                      (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
                      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
                          (subst
                            (∑ i : Fin (n + 1 + 1),
                              HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
                                (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)))
                            P) :
                        R)) :
                  R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (n + 2)))
            P) :
        R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
    0
have succ : ∀ (B : R⟦X⟧)
  (hB :
    ∑ i : Fin (n + 2),
        HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧)
          (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
      B),
  HSub.hSub (α := R) (β := R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          (subst
            (B +
              HMul.hMul (α := R⟦X⟧)
                ((C : (a : R) → R⟦X⟧)
                    (HMul.hMul (α := R) (β := R)
                      (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
                      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R)) :
                  R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (n + 2)))
            P) :
        R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
    0
Tactic: generalize hB : ∑ i : Fin (n + 2), C (substInvFun P i) * X ^ i.1 = B
-- 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 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 2),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
⊢ HSub.hSub (α := R) (β := R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          (subst
            (B +
              HMul.hMul (α := R⟦X⟧)
                ((C : (a : R) → R⟦X⟧)
                    (HMul.hMul (α := R) (β := R)
                      (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
                      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R)) :
                  R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (n + 2)))
            P) :
        R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
    0
have hB' : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)
Tactic: have hB' : B.constantCoeff = 0 := by simp [← hB, zero_pow_eq, substInvFun]
-- 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 : ℕ
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)
⊢ HSub.hSub (α := R) (β := R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
          (subst
            (B +
              HMul.hMul (α := R⟦X⟧)
                ((C : (a : R) → R⟦X⟧)
                    (HMul.hMul (α := R) (β := R)
                      (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
                      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R)) :
                  R⟦X⟧)
                (HPow.hPow (α := R⟦X⟧) X (n + 2)))
            P) :
        R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) X : R) =
    0
have succ : Eq (α := R)
  ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R)
      (subst
        (B +
          -(HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧)
                ((C : (a : R) → R⟦X⟧)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R) :
                  R⟦X⟧)
                ((C : (a : R) → R⟦X⟧) ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R) : R⟦X⟧) *
              HPow.hPow (α := R⟦X⟧) X (n + 2)))
        P) :
    R)
  (0 : R)
Tactic: simp only [neg_mul, map_neg, map_mul, coeff_X, Nat.add_eq_right, Nat.add_eq_zero_iff,
      one_ne_zero, and_false, ↓reduceIte, sub_zero]
-- 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 : ℕ
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)
⊢ 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)
have 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
Tactic: rw [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 : ℕ
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
⊢ 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)
have 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)))
Tactic: rw [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 : ℕ
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)
⊢ 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
have 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
Tactic: simp only [smul_eq_mul, ← map_mul]
-- 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 : ℕ
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)
⊢ 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
have 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
Tactic: generalize hk : ⅟(P.coeff 1) * coeff (n + 1 + 1) (subst B P) = k
-- 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 : ℕ
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))
    0
have 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)))
Tactic: trans ∑ᶠ d, P.coeff d * (coeff (n + 1 + 1) (B ^ d) - if d = 1 then k else 0)
-- 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 : ℕ
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)))
⊢ 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
have 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
Tactic: trans ∑ᶠ d, P.coeff d * (coeff (n + 1 + 1) (B ^ d) - if d = 1 then k else 0)
-- 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 : ℕ
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)))
have 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))
Tactic: refine finsum_congr fun i ↦ ?_
-- 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 : ℕ
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 : ℕ
⊢ 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))
have 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)
Tactic: congr 1
-- 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 : ℕ
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 + 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)
have 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)
Tactic: obtain (_ | _ | i) := i
Cleared hypotheses: i
-- 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 : ℕ
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)
⊢ (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)
have 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)
Tactic: obtain (_ | _ | i) := i
Cleared hypotheses: i
-- 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 : ℕ
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)
⊢ (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)
have 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)
Tactic: obtain (_ | _ | i) := i
Cleared hypotheses: i