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 : ℕ
B : R⟦X⟧
hB :
  ∑ i : Fin (n + 2),
      HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) (P.substInvFun (↑i : ℕ)) : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (↑i : ℕ)) =
    B
hB' : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) B : R) (0 : R)
k : R
hk :
  HMul.hMul (α := R) (β := R)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne ((coeff 1 : (a : R⟦X⟧) → R) P) _ : R)
      ((coeff (n + 1 + 1) : (a : R⟦X⟧) → R) (subst B P) : R) =
    k
i : ℕ
⊢ (coeff (n + 2) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 2)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
have e_a : (coeff (n + 2) : (a : R⟦X⟧) → R)
    (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) 0 *
        B ^ (i + 2 - 0) *
      (↑((i + 2).choose 0) : R⟦X⟧)) =
  HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
Tactic: rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 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
i : ℕ
e_a :
  (coeff (n + 2) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) 0 *
          B ^ (i + 2 - 0) *
        (↑((i + 2).choose 0) : R⟦X⟧)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
⊢ (coeff (n + 2) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 2)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
have e_a₁ : ∀ b ∈ Finset.range (i + 2 + 1),
  b ≠ 0 →
    Eq (α := R)
      ((coeff (n + 2) : (a : R⟦X⟧) → R)
          ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ b *
              B ^ (i + 2 - b) *
            (↑((i + 2).choose b) : R⟦X⟧)) :
        R)
      (0 : R)
Tactic: rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 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
i : ℕ
e_a :
  (coeff (n + 2) : (a : R⟦X⟧) → R)
      (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) 0 *
          B ^ (i + 2 - 0) *
        (↑((i + 2).choose 0) : R⟦X⟧)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
e_a₁ :
  ∀ b ∈ Finset.range (i + 2 + 1),
    b ≠ 0 →
      Eq (α := R)
        ((coeff (n + 2) : (a : R⟦X⟧) → R)
            ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ b *
                B ^ (i + 2 - b) *
              (↑((i + 2).choose b) : R⟦X⟧)) :
          R)
        (0 : R)
⊢ (coeff (n + 2) : (a : R⟦X⟧) → R)
      ((B + -HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (i + 2)) =
    HSub.hSub (α := R) ((coeff (n + 2) : (a : R⟦X⟧) → R) (B ^ (i + 2)) : R) (if i + 2 = 1 then k else 0)
have e_a₂ : 0 ∉ Finset.range (i + 2 + 1) →
  Eq (α := R)
    ((coeff (n + 2) : (a : R⟦X⟧) → R)
        (HPow.hPow (β := ℕ) (-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2)))
              0 *
            B ^ (i + 2 - 0) *
          (↑((i + 2).choose 0) : R⟦X⟧)) :
      R)
    (0 : R)
Tactic: rw [add_comm B, add_pow, map_sum, Finset.sum_eq_single (a := 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
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)
        ((-HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) k : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X (n + 2))) ^ (j + 1 + 1) *
            B ^ (i + 2 - (j + 1 + 1)) *
          (↑((i + 2).choose (j + 1 + 1)) : R⟦X⟧)) :
      R)
    (0 : R)
have e_a : Eq (α := R)
  ((coeff (n + 2) : (a : R⟦X⟧) → R)
      (HPow.hPow (α := R⟦X⟧) X ((n + 2) * (j + 1 + 1)) *
            HPow.hPow (α := R⟦X⟧) (-(C : (a : R) → R⟦X⟧) k : R⟦X⟧) (j + 1 + 1) *
          B ^ (i + 2 - (j + 1 + 1)) *
        (↑((i + 2).choose (j + 1 + 1)) : R⟦X⟧)) :
    R)
  (0 : R)
Tactic: rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
-- 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) ((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
have 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
Tactic: simp_rw [mul_sub]
-- 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 ^ d) : R) -
        HMul.hMul (α := R) ((coeff d : (a : R⟦X⟧) → R) P : R) (if d = 1 then k else 0)))
    0
have 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
Tactic: rw [finsum_sub_distrib]
-- 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
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
⊢ 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
have 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)
Tactic: rw [finsum_sub_distrib]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [finsum_sub_distrib]
-- 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
⊢ 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
have 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
Tactic: simp only [mul_ite, mul_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)
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
⊢ 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
have 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
Tactic: nth_rw 2 [finsum_eq_single (a := 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
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
⊢ 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
have ha : ∀ (x : ℕ), x ≠ 1 → (if x = 1 then HMul.hMul (α := R) ((coeff x : (a : R⟦X⟧) → R) P : R) k else 0) = 0
Tactic: nth_rw 2 [finsum_eq_single (a := 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 : ℕ),
        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
have 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)
Tactic: simp only [↓reduceIte, ← hk, mul_invOf_cancel_left', sub_eq_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)
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 (α := 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)
have 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))
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)
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))
⊢ 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)
have hb : HasSubst B
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)
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)
have 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)
Tactic: refine .subset (Set.finite_Iio (n + 3)) 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 : ℕ
⊢ 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)
have 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)
Tactic: obtain ⟨B, rfl⟩ : X ∣ B := by rwa [X_dvd_iff]
Cleared hypotheses: B, hB, hB', hk
-- 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.substInv P = X
have h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (subst P.substInv P) : R) ((coeff n : (a : R⟦X⟧) → R) X : R)
Tactic: ext n
-- 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 : ℕ
⊢ 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)
      (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