awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
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)
| 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:
arg 2
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
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)
| 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:
rw [mul_comm, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
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)
| 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:
lhs; arg 2; rw [mul_comm, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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) ((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'
⊢ 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:
conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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) (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'
⊢ 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:
move_mul [← constantCoeff φ ^ (n' - 1)]

Premises used: HSub.hSub, PowerSeries.constantCoeff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
enter : (constantCoeff : (a : R⟦X⟧) → R) φ
| 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:
enter [1, 2, 1, 1, 2]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
rw : HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1
| (constantCoeff : (a : R⟦X⟧) → R) φ

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

Premises used: PowerSeries.constantCoeff, pow_one, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
enter : HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1
| 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:
enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]

Premises used: PowerSeries.constantCoeff, pow_one, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
        (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1) *
            HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1 *
          (↑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'
⊢ 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:
conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]

Premises used: PowerSeries.constantCoeff, pow_one, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1) * (↑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'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1) *
            HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1 *
          (↑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:
rw [← pow_add (a := constantCoeff φ)]

Premises used: pow_add, PowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
enter : HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1)
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1) * (↑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:
enter [1, 2, 1, 1]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
rw : HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
| HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1)

Tactic:
rw [Nat.sub_add_cancel h']

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
enter : 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) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1) * (↑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:
enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n' * (↑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'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1) * (↑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:
conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n' * (↑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:
ring
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
⊢ n' > 0

Tactic:
h'

Premises used: Nat.lt
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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'
⊢ n' > 0

Tactic:
exact h'
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
decide
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
inr :
  ∀ (hn : GT.gt (α := ℕ) 0 0),
    (coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) =
      HMul.hMul (α := R) (β := R) ((↑0 : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (HSub.hSub (α := ℕ) 0 1)
inr₁ :
  ∀ (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),
    (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)
⊢ (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)

Tactic:
induction n with
  | zero => lia
  | succ n' ih =>
      have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
      have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
      rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
      · simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]
        have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
        rcases h₀ with h' | h'
        · by_contra h''
          rw [h'] at h''
          simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
          norm_num at h''
        · rw [ih]
          · conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
            move_mul [← constantCoeff φ ^ (n' - 1)]
            conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
            rw [← pow_add (a := constantCoeff φ)]
            conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
            ring
          exact h'
      · decide

Premises used: MulZeroClass.zero_mul, mul_assoc, pow_add, map_pow, PowerSeries.constantCoeff, pow_zero, Finset.sum_singleton, Nat.cast_add, PowerSeries.coeff_mul, PowerSeries.coeff_one, pow_one, PowerSeries.coeff_zero_eq_constantCoeff, mul_comm, reduceIte, add_tsub_cancel_right, mul_one, Finset.sum_insert, add_zero, one_ne_zero, Nat.cast_one, DFunLike.coe, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
pos : ∀ (hA : Subsingleton A), ¬IsField.{u_2} A⟦X⟧
neg : ∀ (hA : ¬Subsingleton A), ¬IsField.{u_2} A⟦X⟧
⊢ ¬IsField.{u_2} A⟦X⟧

Tactic:
by_cases hA : Subsingleton A

Premises used: Subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : Subsingleton A
⊢ ¬IsField.{u_2} A⟦X⟧

Tactic:
not_isField_of_subsingleton _

Premises used: not_isField_of_subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : Subsingleton A
⊢ ¬IsField.{u_2} A⟦X⟧

Tactic:
exact not_isField_of_subsingleton _

Premises used: not_isField_of_subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
rw : ∃ (I : Ideal A⟦X⟧), ⊥ < I ∧ I < ⊤
⊢ ¬IsField.{u_2} A⟦X⟧

Tactic:
rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]

Premises used: Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h_1 : Nontrivial A
h : LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X}) ∧ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
⊢ ∃ (I : Ideal A⟦X⟧), ⊥ < I ∧ I < ⊤

Tactic:
use Ideal.span {X}

Premises used: PowerSeries.X, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h_1 : Nontrivial A
h : LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X})
h₁ : LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
⊢ LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X}) ∧ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤

Tactic:
constructor