-- Mathlib/RingTheory/PowerSeries/Basic.lean
/-- First coefficient of the `n`-th power of a power series. -/
lemma coeff_one_pow (n : ℕ) (φ : R⟦X⟧) :
    coeff R 1 (φ ^ n) = n * coeff R 1 φ * (constantCoeff R φ) ^ (n - 1)

Proof state:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
rw [ih]

Result:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ +
      ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1) * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ n' > 0

Proof state:
case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
⊢ (coeff R 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ (n' + 1 - 1)

Tactic:
have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl

Result:
case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff R 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ (n' + 1 - 1)

Proof state:
case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
h'' : ¬(coeff R 1) φ = (↑0 + 1) * (coeff R 1) φ
⊢ False

Tactic:
norm_num at h''

Result:
no goals

Proof state:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (constantCoeff R) φ ^ (n' - 1 + 1) * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']

Result:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (constantCoeff R) φ ^ n' * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Proof state:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ +
      (constantCoeff R) φ ^ (n' - 1) * (constantCoeff R) φ * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff R φ)]

Result:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ +
      (constantCoeff R) φ ^ (n' - 1) * (constantCoeff R) φ ^ 1 * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff R 1) (φ ^ n) = ↑n * (coeff R 1) φ * (constantCoeff R) φ ^ (n - 1)

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hn)

Result:
case inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
⊢ (coeff R 1) (φ ^ 0) = ↑0 * (coeff R 1) φ * (constantCoeff R) φ ^ (0 - 1)

case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff R 1) (φ ^ n) = ↑n * (coeff R 1) φ * (constantCoeff R) φ ^ (n - 1)

Proof state:
case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
by_contra h''

Result:
case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
h'' :
  ¬(constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
      (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'
⊢ False

Proof state:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ +
      (constantCoeff R) φ ^ (n' - 1) * (constantCoeff R) φ ^ 1 * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
rw [← pow_add (a := constantCoeff R φ)]

Result:
case inr.succ.inr
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff R 1) (φ ^ n') = ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (constantCoeff R) φ ^ (n' - 1 + 1) * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'