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)}
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 : HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 1
Tactic: enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
-- 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 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'
Tactic: conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
-- 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)
        (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'
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) (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: rw [← pow_add (a := constantCoeff φ)]
-- 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) (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'
have enter : HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1)
Tactic: enter [1, 2, 1, 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'
| HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1 + 1)
have rw : HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: rw [Nat.sub_add_cancel 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) (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'
have enter : HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
Tactic: enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel 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) (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'
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) (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: conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
φ : R⟦X⟧
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)
have 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)
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ (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)
have 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)
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
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
⊢ ¬IsField.{u_2} A⟦X⟧
have pos : ∀ (hA : Subsingleton A), ¬IsField.{u_2} A⟦X⟧
Tactic: by_cases hA : Subsingleton A
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
pos : ∀ (hA : Subsingleton A), ¬IsField.{u_2} A⟦X⟧
⊢ ¬IsField.{u_2} A⟦X⟧
have neg : ∀ (hA : ¬Subsingleton A), ¬IsField.{u_2} A⟦X⟧
Tactic: by_cases hA : Subsingleton A
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
⊢ ¬IsField.{u_2} A⟦X⟧
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ¬IsField.{u_2} A⟦X⟧
have rw : ∃ (I : Ideal A⟦X⟧), ⊥ < I ∧ I < ⊤
Tactic: rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ∃ (I : Ideal A⟦X⟧), ⊥ < I ∧ I < ⊤
have h : LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X}) ∧ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
Tactic: use Ideal.span {X}
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X}) ∧ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
have h : LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X})
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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}) ∧ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
have h₁ : LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X})
have h : ¬Eq.{u_2 + 1} (α := A⟦X⟧) X 0
Tactic: rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤
have h : ¬Eq.{u_2 + 1} (α := A) 1 0
Tactic: rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
        X_dvd_iff, constantCoeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
a : A
⊢ (rescale a : (a : A⟦X⟧) → A⟦X⟧) X = HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X) : A)
have h : (a ^ n * if n = 1 then 1 else 0) = a * if n = 1 then 1 else 0
Tactic: simp only [coeff_rescale, coeff_C_mul, coeff_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
⊢ (a ^ n * if n = 1 then 1 else 0) = a * if n = 1 then 1 else 0
have pos : ∀ (h : n = 1), a ^ n * 1 = a * 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
pos : ∀ (h : n = 1), a ^ n * 1 = a * 1
⊢ (a ^ n * if n = 1 then 1 else 0) = a * if n = 1 then 1 else 0
have neg : ∀ (h : ¬n = 1), a ^ n * 0 = a * 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)
have rw : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) (-1) : A⟦X⟧) X = -X
Tactic: rw [rescale_X, map_neg, map_one, neg_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
rw : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) (-1) : A⟦X⟧) X = -X
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)
have rw₁ : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) (-(C : (a : A) → A⟦X⟧) 1 : A⟦X⟧) X = -X
Tactic: rw [rescale_X, map_neg, map_one, neg_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
rw : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) (-1) : A⟦X⟧) X = -X
rw₁ : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) (-(C : (a : A) → A⟦X⟧) 1 : A⟦X⟧) X = -X
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)
have rw₂ : HMul.hMul (α := A⟦X⟧) (-1) X = -X
Tactic: rw [rescale_X, map_neg, map_one, neg_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
A : Type u_2
inst : CommRing A
rw : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) (-1) : A⟦X⟧) X = -X
rw₁ : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) (-(C : (a : A) → A⟦X⟧) 1 : A⟦X⟧) X = -X
rw₂ : HMul.hMul (α := A⟦X⟧) (-1) X = -X
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)
have rw₃ : Eq.{u_2 + 1} (α := A⟦X⟧) (-X) (-X)
Tactic: rw [rescale_X, map_neg, map_one, neg_one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial n : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.monomial n : (a : R) → PowerSeries R) a)
have h : ∀ (n_1 : ℕ),
  Eq.{u_1 + 1} (α := R)
    ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R) (↑((monomial n : (a : R) → R[X]) a) : PowerSeries R) : R)
    ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R)
        ((PowerSeries.monomial n : (a : R) → PowerSeries R) a : PowerSeries R) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑1 : PowerSeries R) 1
have this : Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
  ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) 1)
Tactic: have := coe_monomial 0 (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
this :
  Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) 1)
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑1 : PowerSeries R) 1
have rwa : ∀
  (this :
    Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
      ((PowerSeries.C : (a : R) → PowerSeries R) 1)),
  Eq.{u_1 + 1} (α := PowerSeries R) (↑1 : PowerSeries R) 1
Tactic: rwa [PowerSeries.monomial_zero_eq_C_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R[X]
⊢ (↑(φ + ψ) : PowerSeries R) = (↑φ : PowerSeries R) + (↑ψ : PowerSeries R)
have h : ∀ (n : ℕ),
  Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑(φ + ψ) : PowerSeries R) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) ((↑φ : PowerSeries R) + (↑ψ : PowerSeries R)) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((C : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.C : (a : R) → PowerSeries R) a)
have this : Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
  ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) a)
Tactic: have := coe_monomial 0 a
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
this :
  Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) a)
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((C : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.C : (a : R) → PowerSeries R) a)
have rwa : ∀
  (this :
    Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
      ((PowerSeries.C : (a : R) → PowerSeries R) a)),
  Eq.{u_1 + 1} (α := PowerSeries R) (↑((C : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.C : (a : R) → PowerSeries R) a)
Tactic: rwa [PowerSeries.monomial_zero_eq_C_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
U : Type u_2
V : Type u_3
inst : CommSemiring U
inst_1 : CommSemiring V
φ : U →+* V
f : U[X]
⊢ (↑(map φ f) : PowerSeries V) = (PowerSeries.map φ : (a : PowerSeries U) → PowerSeries V) (↑f : PowerSeries U)
have h : ∀ (n : ℕ),
  Eq (α := V) ((PowerSeries.coeff n : (a : PowerSeries V) → V) (↑(map φ f) : PowerSeries V) : V)
    ((PowerSeries.coeff n : (a : PowerSeries V) → V)
        ((PowerSeries.map φ : (a : PowerSeries U) → PowerSeries V) (↑f : PowerSeries U) : PowerSeries V) :
      V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R[X]
h : (↑x : PowerSeries R) = (↑y : PowerSeries R)
⊢ x = y
have a : ∀ (n : ℕ), x.coeff n = y.coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R[X]
h : (↑x : PowerSeries R) = (↑y : PowerSeries R)
n : ℕ
⊢ x.coeff n = y.coeff n
have a : Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑x : PowerSeries R) : R)
  ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑y : PowerSeries R) : R)
Tactic: simp_rw [← coeff_coe, h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ (↑φ : PowerSeries R) = 0 ↔ φ = 0
have rw : (↑φ : PowerSeries R) = (↑0 : PowerSeries R) ↔ φ = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
rw : (↑φ : PowerSeries R) = (↑0 : PowerSeries R) ↔ φ = 0
⊢ (↑φ : PowerSeries R) = 0 ↔ φ = 0
have rw₁ : φ = 0 ↔ φ = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ (↑φ : PowerSeries R) = 1 ↔ φ = 1
have rw : (↑φ : PowerSeries R) = (↑1 : PowerSeries R) ↔ φ = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
rw : (↑φ : PowerSeries R) = (↑1 : PowerSeries R) ↔ φ = 1
⊢ (↑φ : PowerSeries R) = 1 ↔ φ = 1
have rw₁ : φ = 1 ↔ φ = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ eval₂ PowerSeries.C PowerSeries.X φ = (↑φ : PowerSeries R)
have nth_rw : eval₂ PowerSeries.C PowerSeries.X φ = (↑(eval₂ C X φ) : PowerSeries R)
Tactic: nth_rw 2 [← eval₂_C_X (p := φ)]