awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
n : Unit →₀ ℕ
rw :
  Eq (α := R) ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) φ : R)
    ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) ψ : R)
rw₁ : Eq (α := ℕ) ((n : (a : Unit) → ℕ) () : ℕ) ((n : (a : Unit) → ℕ) () : ℕ)
⊢ Eq (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) φ : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) ψ : R)
have rw₂ : ℕ
Tactic: rw [← coeff_def]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
⊢ Subsingleton.{u_1 + 1} R⟦X⟧
have simp : ∀ (x y : R⟦X⟧) (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) x : R) ((coeff n : (a : R⟦X⟧) → R) y : R)
Tactic: simp only [subsingleton_iff, PowerSeries.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = n then a else 0) : R)
have rw : (if m = n then a else 0) = (coeff m : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = n then a else 0)
Tactic: rw [coeff_monomial, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
rw : (if m = n then a else 0) = (coeff m : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = n then a else 0)
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) (mk fun (m : ℕ) ↦ if m = n then a else 0) : R)
have rw₁ : (if m = n then a else 0) = if m = n then a else 0
Tactic: rw [coeff_monomial, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := (a : R⟦X⟧) → R) (⇑(coeff 0) : (a : R⟦X⟧) → R) (⇑constantCoeff : (a : R⟦X⟧) → R)
have rw : Eq.{u_1 + 1} (α := (a : R⟦X⟧) → R) (⇑(MvPowerSeries.coeff 0) : (a : R⟦X⟧) → R) (⇑constantCoeff : (a : R⟦X⟧) → R)
Tactic: rw [coeff, Finsupp.single_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have rw : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := (a : R) → R⟦X⟧) (⇑(monomial 0) : (a : R) → R⟦X⟧) (⇑C : (a : R) → R⟦X⟧)
have rw : Eq.{u_1 + 1} (α := (a : R) → R⟦X⟧) (⇑MvPowerSeries.C : (a : R) → MvPowerSeries Unit R) (⇑C : (a : R) → R⟦X⟧)
Tactic: rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ (coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = if n = 0 then a else 0
have rw : (coeff n : (a : R⟦X⟧) → R) ((monomial 0 : (a : R) → R⟦X⟧) a : R⟦X⟧) = if n = 0 then a else 0
Tactic: rw [← monomial_zero_eq_C_apply, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
rw : (coeff n : (a : R⟦X⟧) → R) ((monomial 0 : (a : R) → R⟦X⟧) a : R⟦X⟧) = if n = 0 then a else 0
⊢ (coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = if n = 0 then a else 0
have rw₁ : (if n = 0 then a else 0) = if n = 0 then a else 0
Tactic: rw [← monomial_zero_eq_C_apply, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ (coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = a
have rw : (if Eq (α := ℕ) 0 0 then a else 0) = a
Tactic: rw [coeff_C, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
rw : (if Eq (α := ℕ) 0 0 then a else 0) = a
⊢ (coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = a
have rw₁ : a = a
Tactic: rw [coeff_C, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
h : n ≠ 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have rw : (if n = 0 then a else 0) = 0
Tactic: rw [coeff_C, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
h : n ≠ 0
rw : (if n = 0 then a else 0) = 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_C, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Subsingleton.{u_1 + 1} R⟦X⟧ ↔ Subsingleton R
have refine : ∀ (h : Subsingleton.{u_1 + 1} R⟦X⟧), Subsingleton R
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
h : Subsingleton.{u_1 + 1} R⟦X⟧
⊢ Subsingleton R
have rw : ∀ (h : ∀ (x y : R⟦X⟧), x = y) (x y : R), x = y
Tactic: rw [subsingleton_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) X : R) (if n = 1 then 1 else 0 : R)
have rw : Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) ((monomial 1 : (a : R) → R⟦X⟧) 1 : R⟦X⟧) : R)
  (if n = 1 then 1 else 0 : R)
Tactic: rw [X_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) ((monomial 1 : (a : R) → R⟦X⟧) 1 : R⟦X⟧) : R)
    (if n = 1 then 1 else 0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) X : R) (if n = 1 then 1 else 0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (if n = 1 then 1 else 0) (if n = 1 then 1 else 0)
Tactic: rw [X_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
have rw : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff (single () 0) : (a : R⟦X⟧) → R) X : R) (0 : R)
Tactic: rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff (single () 0) : (a : R⟦X⟧) → R) X : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
Tactic: rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff (single () 0) : (a : R⟦X⟧) → R) X : R) (0 : R)
rw₁ : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
have rw₂ : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff 0 : (a : R⟦X⟧) → R) (MvPowerSeries.X ()) : R) (0 : R)
Tactic: rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff (single () 0) : (a : R⟦X⟧) → R) X : R) (0 : R)
rw₁ : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
rw₂ : Eq.{u_1 + 1} (α := R) ((MvPowerSeries.coeff 0 : (a : R⟦X⟧) → R) (MvPowerSeries.X ()) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((coeff 1 : (a : R⟦X⟧) → R) X : R) (1 : R)
have rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
Tactic: rw [coeff_X, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
⊢ Eq.{u_1 + 1} (α := R) ((coeff 1 : (a : R⟦X⟧) → R) X : R) (1 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [coeff_X, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (if m = n then 1 else 0 : R)
have rw : Eq.{u_1 + 1} (α := R) ((coeff m : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) 1 : R⟦X⟧) : R)
  (if m = n then 1 else 0 : R)
Tactic: rw [X_pow_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) ((coeff m : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) 1 : R⟦X⟧) : R)
    (if m = n then 1 else 0 : R)
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (if m = n then 1 else 0 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (if m = n then 1 else 0) (if m = n then 1 else 0)
Tactic: rw [X_pow_eq, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (1 : R)
have rw : Eq.{u_1 + 1} (α := R) (if n = n then 1 else 0) 1
Tactic: rw [coeff_X_pow, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (if n = n then 1 else 0) 1
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (1 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [coeff_X_pow, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R)
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R) :
      R)
have refine : Eq.{u_1 + 1} (α := R)
  (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
    HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff p.1 : (a : MvPowerSeries Unit R) → R) φ : R)
      ((MvPowerSeries.coeff p.2 : (a : MvPowerSeries Unit R) → R) ψ : R))
  (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
Tactic: refine (MvPowerSeries.coeff_mul _ φ ψ).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ Eq.{u_1 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff p.1 : (a : MvPowerSeries Unit R) → R) φ : R)
        ((MvPowerSeries.coeff p.2 : (a : MvPowerSeries Unit R) → R) ψ : R))
    (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
have rw : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff
              ((Function.Embedding.prodMap { toFun := single (), inj' := sorry } { toFun := single (), inj' := sorry } :
                    (a : ℕ × ℕ) → (Unit →₀ ℕ) × (Unit →₀ ℕ))
                  x).1 :
            (a : MvPowerSeries Unit R) → R)
          φ :
        R)
      ((MvPowerSeries.coeff
              ((Function.Embedding.prodMap { toFun := single (), inj' := sorry } { toFun := single (), inj' := sorry } :
                    (a : ℕ × ℕ) → (Unit →₀ ℕ) × (Unit →₀ ℕ))
                  x).2 :
            (a : MvPowerSeries Unit R) → R)
          ψ :
        R))
  (∑ p ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : R⟦X⟧) → R) φ : R) ((coeff p.2 : (a : R⟦X⟧) → R) ψ : R))
Tactic: rw [Finsupp.antidiagonal_single, Finset.sum_map]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : R
⊢ a • f = HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) f
have h : ∀ (n : ℕ),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (a • f) : R)
    ((coeff n : (a : R⟦X⟧) → R) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) f) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (φ * X) : R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
have simp : Eq (α := R)
  ((MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () n) (single () 1)) : (a : R⟦X⟧) → R) (φ * X) : R)
  ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
Tactic: simp only [coeff, Finsupp.single_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R)
    ((MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () n) (single () 1)) : (a : R⟦X⟧) → R) (φ * X) : R)
    ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
have h : (MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ =
  HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R) (1 : R)
Tactic: convert! φ.coeff_add_mul_monomial (single () n) (single () 1) _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ =
    HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R) (1 : R)
have h : Eq (α := R) ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
  ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (X * φ) : R) ((coeff n : (a : R⟦X⟧) → R) φ : R)
have simp : Eq (α := R)
  ((MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () 1) (single () n)) : (a : R⟦X⟧) → R) (X * φ) : R)
  ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
Tactic: simp only [coeff, Finsupp.single_add, add_comm n 1]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R)
    ((MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () 1) (single () n)) : (a : R⟦X⟧) → R) (X * φ) : R)
    ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
have h : (MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ =
  HMul.hMul (α := R) (β := R) (1 : R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
Tactic: convert! φ.coeff_add_monomial_mul (single () 1) (single () n) _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ =
    HMul.hMul (α := R) (β := R) (1 : R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
have h : Eq (α := R) ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
  ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ * X = ψ * X
⊢ φ = ψ
have rw : ∀ (h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * X) : R) ((coeff n : (a : R⟦X⟧) → R) (ψ * X) : R))
  (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
Tactic: rw [PowerSeries.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : X * φ = X * ψ
⊢ φ = ψ
have rw : ∀ (h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (X * φ) : R) ((coeff n : (a : R⟦X⟧) → R) (X * ψ) : R))
  (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
Tactic: rw [PowerSeries.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ Eq (α := R) ((coeff (d + n) : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) ((coeff d : (a : R⟦X⟧) → R) p : R)
have h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
  b ≠ (d, n) →
    HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : R⟦X⟧) → R) p : R)
        ((coeff b.2 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) =
      0
Tactic: rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h₀ :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
    b ≠ (d, n) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : R⟦X⟧) → R) p : R)
          ((coeff b.2 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) =
        0
⊢ Eq (α := R) ((coeff (d + n) : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) ((coeff d : (a : R⟦X⟧) → R) p : R)
have h₁ : (d, n) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) →
  HMul.hMul (α := R) (β := R) ((coeff (d, n).1 : (a : R⟦X⟧) → R) p : R)
      ((coeff (d, n).2 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) =
    0
Tactic: rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n)
h2 : (i, j) ≠ (d, n)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) p : R)
      ((coeff (i, j).2 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) =
    0
have h₀ : ¬(i, j).2 = n
Tactic: rw [coeff_X_pow, if_neg, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False
have h₀ : (i, j) = (d, (i, j).2)
Tactic: apply h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)
have h1₁ : (i, j).1 = d
Tactic: rw [mem_antidiagonal, add_right_cancel_iff] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).1 = d
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)
have h₀ : ∀ (h2 : (i, j) ≠ ((i, j).1, (i, j).2)), (i, j) = ((i, j).1, (i, j).2)
Tactic: subst h1
Cleared hypotheses: d, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ Eq (α := R) ((coeff (d + n) : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) ((coeff d : (a : R⟦X⟧) → R) p : R)
have h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
  b ≠ (n, d) →
    HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
        ((coeff b.2 : (a : R⟦X⟧) → R) p : R) =
      0
Tactic: rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h₀ :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n),
    b ≠ (n, d) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
          ((coeff b.2 : (a : R⟦X⟧) → R) p : R) =
        0
⊢ Eq (α := R) ((coeff (d + n) : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) ((coeff d : (a : R⟦X⟧) → R) p : R)
have h₁ : (n, d) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) →
  HMul.hMul (α := R) (β := R) ((coeff (n, d).1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
      ((coeff (n, d).2 : (a : R⟦X⟧) → R) p : R) =
    0
Tactic: rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + n)
h2 : (i, j) ≠ (n, d)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
      ((coeff (i, j).2 : (a : R⟦X⟧) → R) p : R) =
    0
have h₀ : ¬(i, j).1 = n
Tactic: rw [coeff_X_pow, if_neg, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ False
have h₀ : (i, j) = ((i, j).1, d)
Tactic: apply h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)
have h1₁ : (i, j).2 = d
Tactic: rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).2 = d
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)
have h₀ : ∀ (h2 : (i, j) ≠ ((i, j).1, (i, j).2)), (i, j) = ((i, j).1, (i, j).2)
Tactic: subst h1
Cleared hypotheses: d, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ @antidiagonal _ Nat.instAddMonoid _ (d + n) →
    HMul.hMul (α := R) (β := R) ((coeff (n, d).1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
        ((coeff (n, d).2 : (a : R⟦X⟧) → R) p : R) =
      0
have h₁ : (n, d) ∉ @antidiagonal _ Nat.instAddMonoid _ (n + d) →
  HMul.hMul (α := R) (β := R) ((coeff (n, d).1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
      ((coeff (n, d).2 : (a : R⟦X⟧) → R) p : R) =
    0
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : φ * HPow.hPow (α := R⟦X⟧) X k = ψ * HPow.hPow (α := R⟦X⟧) X k
⊢ φ = ψ
have rw : ∀
  (h :
    ∀ (n : ℕ),
      Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * HPow.hPow (α := R⟦X⟧) X k) : R)
        ((coeff n : (a : R⟦X⟧) → R) (ψ * HPow.hPow (α := R⟦X⟧) X k) : R))
  (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
Tactic: rw [PowerSeries.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : HPow.hPow (α := R⟦X⟧) X k * φ = HPow.hPow (α := R⟦X⟧) X k * ψ
⊢ φ = ψ
have rw : ∀
  (h :
    ∀ (n : ℕ),
      Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X k * φ) : R)
        ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X k * ψ) : R))
  (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
Tactic: rw [PowerSeries.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R)
    (if n ≤ d then (coeff (d - n) : (a : R⟦X⟧) → R) p else 0 : R)
have pos : ∀ (h : n ≤ d),
  Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)
Tactic: split_ifs with h