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

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

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' * (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 * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ n' = 0 ∨ 1 ≤ n'

Tactic:
omega

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
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff R (0, 1).1) (φ ^ n') * (coeff R (0, 1).2) φ + (coeff R (1, 0).1) (φ ^ n') * (coeff R (1, 0).2) φ =
    ↑(n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ (n' + 1 - 1)

Tactic:
simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
  add_tsub_cancel_right]

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

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
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)

Tactic:
rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]

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

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)}
⊢ (0, 1) ∉ {(1, 0)}

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

Tactic:
omega

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
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (constantCoeff R) φ ^ n' * (coeff R 1) φ + (coeff R 1) (φ ^ n') * (constantCoeff R) φ =
    (↑n' + 1) * (coeff R 1) φ * (constantCoeff R) φ ^ n'

Tactic:
have h₀ : n' = 0 ∨ 1 ≤ n' := by omega

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)}
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'

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' > 0

Tactic:
exact h'

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
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
decide

Result:
no goals