-- 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
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 ∨ 1 ≤ n'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
rcases h₀ with h' | 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
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (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'
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
    (↑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) φ +
      ↑n' * (coeff R 1) φ * (constantCoeff R) φ ^ (n' - 1) * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]

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' * (coeff R 1) φ) * (constantCoeff R) φ ^ (n' - 1) =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

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

Tactic:
simp

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'
⊢ (↑n' + 1) * ((constantCoeff R) φ ^ n' * (coeff R 1) φ) = (↑n' + 1) * ((coeff R 1) φ * (constantCoeff R) φ ^ n')

Tactic:
conv => enter [1, 2]; rw [mul_comm]

Result:
no goals

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'' :
  ¬(constantCoeff R) φ ^ 0 * (coeff R 1) φ + (coeff R 1) (φ ^ 0) * (constantCoeff R) φ =
      (↑0 + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ 0
⊢ False

Tactic:
simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
  CharP.cast_eq_zero, zero_add, mul_one, not_true_eq_false] at 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'' : ¬(coeff R 1) φ = (↑0 + 1) * (coeff R 1) φ
⊢ 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) φ + ↑n' * (constantCoeff R) φ ^ n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
rw [mul_assoc, ← one_add_mul, add_comm, mul_assoc]

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'
⊢ (↑n' + 1) * ((constantCoeff R) φ ^ n' * (coeff R 1) φ) = (↑n' + 1) * ((coeff R 1) φ * (constantCoeff R) φ ^ n')

Proof state:
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 * φ
⊢ antidiagonal 1 = {(0, 1), (1, 0)}

Tactic:
exact rfl

Result:
no goals

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
⊢ (coeff R 1) (φ ^ (n' + 1)) = ↑(n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ (n' + 1 - 1)

Tactic:
have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := 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 * φ
⊢ (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'' :
  ¬(constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
      (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'
⊢ False

Tactic:
rw [h'] at 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) φ ^ 0 * (coeff R 1) φ + (coeff R 1) (φ ^ 0) * (constantCoeff R) φ =
      (↑0 + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ 0
⊢ 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' * (coeff R 1) φ) * (constantCoeff R) φ ^ (n' - 1) =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
move_mul [← (constantCoeff R) φ ^ (n' - 1)]

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) φ * ↑n' * (coeff R 1) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'