awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
inr :
  HMul.hMul (α := R) (β := R) ((coeff (0, 1).1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
        ((coeff (0, 1).2 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff (1, 0).1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
        ((coeff (1, 0).2 : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ (n' + 1)) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
have inr₁ : (0, 1) ∉ {(1, 0)}
Tactic: rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
⊢ HMul.hMul (α := R) (β := R) ((coeff (0, 1).1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
        ((coeff (0, 1).2 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff (1, 0).1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
        ((coeff (1, 0).2 : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
have inr : HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n') ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
  HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have h₀ : n' = 0 ∨ 1 ≤ n'
Tactic: have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h₀ : n' = 0 ∨ 1 ≤ n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr : ∀ (h' : n' = 0),
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: rcases h₀ with h' | h'
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h₀ : n' = 0 ∨ 1 ≤ n'
inr :
  ∀ (h' : n' = 0),
    HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr₁ : ∀ (h' : 1 ≤ n'),
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: rcases h₀ with h' | h'
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : n' = 0
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr : ∀
  (h'' :
    ¬HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
            ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
          HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
            ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
        HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
          HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'),
  False
Tactic: by_contra h''
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : n' = 0
h'' :
  ¬HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ False
have h''₁ : ¬HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0)
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) : R)
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0
Tactic: rw [h'] at h''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : n' = 0
h'' :
  ¬HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0)
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) : R)
          ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0
⊢ False
have h''₁ : ¬(coeff 1 : (a : R⟦X⟧) → R) φ = HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)
Tactic: simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr : HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n') ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
      ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
  HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
inr :
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
          HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr₁ : n' > 0
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
          HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have lhs : HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n') ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
  HMul.hMul (β := R)
    (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
    ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
Tactic: lhs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
      ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (β := R)
      (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
      ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have arg : HMul.hMul (β := R)
  (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
  ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
Tactic: arg 2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| HMul.hMul (β := R)
    (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
    ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have rw : HMul.hMul (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
    (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)) *
  HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
Tactic: rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
          HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have arg : HMul.hMul (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
    (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)) *
  HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
Tactic: lhs; arg 2; rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
          HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr : HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n') ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
        (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1) =
  HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
          (HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have inr : HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n') ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (β := R)
      (HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
          ((constantCoeff : (a : R⟦X⟧) → R) φ : R) *
        (↑n' : R))
      ((coeff 1 : (a : R⟦X⟧) → R) φ : R) =
  HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: move_mul [← constantCoeff φ ^ (n' - 1)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1))
            ((constantCoeff : (a : R⟦X⟧) → R) φ : R) *
          (↑n' : R))
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
have enter : (constantCoeff : (a : R⟦X⟧) → R) φ
Tactic: enter [1, 2, 1, 1, 2]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
h' : 1 ≤ n'
| (constantCoeff : (a : R⟦X⟧) → R) φ
have rw : HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1
Tactic: rw [← pow_one (a := constantCoeff φ)]