awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                ((Function.Embedding.prodMap { toFun := single (), inj' := ⋯ } { toFun := single (), inj' := ⋯ } :
                      (a : ℕ × ℕ) → (Unit →₀ ℕ) × (Unit →₀ ℕ))
                    x).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                ((Function.Embedding.prodMap { toFun := single (), inj' := ⋯ } { toFun := single (), inj' := ⋯ } :
                      (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:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
a : R
⊢ (coeff n : (a : R⟦X⟧) → R) (HMul.hMul (β := R⟦X⟧) φ ((C : (a : R) → R⟦X⟧) a : R⟦X⟧)) =
    HMul.hMul (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) a

Tactic:
MvPowerSeries.coeff_mul_C _ φ a

Premises used: MvPowerSeries.coeff_mul_C
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
a : R
⊢ (coeff n : (a : R⟦X⟧) → R) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) φ) =
    HMul.hMul (β := R) a ((coeff n : (a : R⟦X⟧) → R) φ : R)

Tactic:
MvPowerSeries.coeff_C_mul _ φ a

Premises used: MvPowerSeries.coeff_C_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
n : ℕ
φ : S⟦X⟧
a : R
⊢ (coeff n : (a : S⟦X⟧) → S) (a • φ) = HSMul.hSMul (β := S) a ((coeff n : (a : S⟦X⟧) → S) φ : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
φ : S⟦X⟧
a : R
⊢ (constantCoeff : (a : S⟦X⟧) → S) (a • φ) = HSMul.hSMul (β := S) a ((constantCoeff : (a : S⟦X⟧) → S) φ : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : R
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)
⊢ a • f = HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) f

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : R
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:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
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)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (φ * X) : R) ((coeff n : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp only [coeff, Finsupp.single_add]

Premises used: PowerSeries.coeff, Finsupp.single_add
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () n) (single () 1)) : (a : MvPowerSeries Unit R) → R)
      (HMul.hMul (β := MvPowerSeries Unit R) φ
        ((MvPowerSeries.monomial (single () 1) : (a : R) → MvPowerSeries Unit R) 1 : MvPowerSeries Unit R)) =
    HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R) (1 : R)

Tactic:
φ.coeff_add_mul_monomial (single () n) (single () 1) _

Premises used: Unit.unit, MvPowerSeries.coeff_add_mul_monomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
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)
⊢ 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:
convert! φ.coeff_add_mul_monomial (single () n) (single () 1) _

Premises used: Unit.unit, MvPowerSeries.coeff_add_mul_monomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h h₁ :
  Eq (α := R) ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
    ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
⊢ (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:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
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)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (X * φ) : R) ((coeff n : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp only [coeff, Finsupp.single_add, add_comm n 1]

Premises used: PowerSeries.coeff, add_comm, Finsupp.single_add, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (HAdd.hAdd (α := Unit →₀ ℕ) (single () 1) (single () n)) : (a : MvPowerSeries Unit R) → R)
      (HMul.hMul (α := MvPowerSeries Unit R)
        ((MvPowerSeries.monomial (single () 1) : (a : R) → MvPowerSeries Unit R) 1 : MvPowerSeries Unit R) φ) =
    HMul.hMul (α := R) (β := R) (1 : R) ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)

Tactic:
φ.coeff_add_monomial_mul (single () 1) (single () n) _

Premises used: Unit.unit, OfNat.ofNat, MvPowerSeries.coeff_add_monomial_mul, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
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)
⊢ 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:
convert! φ.coeff_add_monomial_mul (single () 1) (single () n) _

Premises used: Unit.unit, OfNat.ofNat, MvPowerSeries.coeff_add_monomial_mul, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h h₁ :
  Eq (α := R) ((MvPowerSeries.coeff (single () n) : (a : R⟦X⟧) → R) φ : R)
    ((MvPowerSeries.coeff (single () n) : (a : MvPowerSeries Unit R) → R) φ : R)
⊢ (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:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ * X = ψ * X
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 ⊢

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
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:
simpa using h (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Function.Injective (β := R⟦X⟧) fun (x : R⟦X⟧) ↦ x * X

Tactic:
fun _ _ ↦ mul_X_cancel

Premises used: PowerSeries.mul_X_cancel, Function.Injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ φ * X = ψ * X ↔ φ = ψ

Tactic:
mul_X_injective.eq_iff

Premises used: Function.Injective.eq_iff, PowerSeries.mul_X_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : X * φ = X * ψ
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 ⊢

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
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:
simpa using h (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Function.Injective (β := R⟦X⟧) fun (x : R⟦X⟧) ↦ X * x

Tactic:
fun _ _ ↦ X_mul_cancel

Premises used: PowerSeries.X_mul_cancel, Function.Injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ X * φ = X * ψ ↔ φ = ψ

Tactic:
X_mul_injective.eq_iff

Premises used: Function.Injective.eq_iff, PowerSeries.X_mul_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ (constantCoeff : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = a

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := R →+* R) (RingHom.comp constantCoeff C) (RingHom.id R)

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : R⟦X⟧) → R) 0 : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : R⟦X⟧) → R) 1 : R) (1 : R)

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : R⟦X⟧) → R) X : R) (0 : R)

Tactic:
MvPowerSeries.coeff_zero_X _

Premises used: Function.update, Multiset.zero, PowerSeries.X, Pi.single, dite, MvPowerSeries.X, Multiset.ofList, MvPowerSeries.coeff_zero_X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
f : ℕ → R
⊢ (constantCoeff : (a : R⟦X⟧) → R) (mk f) = f 0

Tactic:
rfl

Premises used: PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (φ * X) : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (X * φ) : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := R⟦X⟧) (β := R) (⇑constantCoeff : (a : R⟦X⟧) → R)

Tactic:
fun r => ⟨C r, constantCoeff_C r⟩

Premises used: PowerSeries.constantCoeff_C, PowerSeries.C, Exists.intro, DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
x : R
k n : ℕ
⊢ (coeff n : (a : R⟦X⟧) → R) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) x : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X k)) =
    if n = k then x else 0

Tactic:
simp [X_pow_eq, coeff_monomial]

Premises used: PowerSeries.coeff_monomial, PowerSeries.X_pow_eq
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
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
⊢ 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)

Tactic:
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]

Premises used: Prod.mk, if_pos, Finset.sum_eq_single, PowerSeries.coeff_mul, PowerSeries.coeff_X_pow, mul_one, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : ¬(i, j).2 = 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

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Premises used: MulZeroClass.mul_zero, PowerSeries.coeff_X_pow, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : (i, j) = (d, (i, j).2)
⊢ False

Tactic:
apply h2
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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).1 = d

Tactic:
rw [mem_antidiagonal, add_right_cancel_iff] at h1

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, add_right_cancel_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h1₁ : (i, j).1 = d
⊢ (i, j) ≠ (d, (i, j).2)

Tactic:
rw [mem_antidiagonal, add_right_cancel_iff] at h1

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, add_right_cancel_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : ∀ (h2 : (i, j) ≠ ((i, j).1, (i, j).2)), (i, j) = ((i, j).1, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Tactic:
subst h1
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (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:
fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Premises used: Iff.mpr, False.elim, Finset.HasAntidiagonal.mem_antidiagonal, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (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:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
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
⊢ 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)

Tactic:
rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]

Premises used: Prod.mk, if_pos, Finset.sum_eq_single, PowerSeries.coeff_mul, PowerSeries.coeff_X_pow, one_mul, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : ¬(i, j).1 = n
⊢ 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

Tactic:
rw [coeff_X_pow, if_neg, zero_mul]

Premises used: MulZeroClass.zero_mul, PowerSeries.coeff_X_pow, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : (i, j) = ((i, j).1, d)
⊢ False

Tactic:
apply h2
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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).2 = d

Tactic:
rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1

Premises used: add_comm, Finset.HasAntidiagonal.mem_antidiagonal, add_right_cancel_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h1₁ : (i, j).2 = d
⊢ (i, j) ≠ ((i, j).1, d)

Tactic:
rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1

Premises used: add_comm, Finset.HasAntidiagonal.mem_antidiagonal, add_right_cancel_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
h₀ : ∀ (h2 : (i, j) ≠ ((i, j).1, (i, j).2)), (i, j) = ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, d)

Tactic:
subst h1
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
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
⊢ (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 [add_comm]

Premises used: add_comm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (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:
fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Premises used: Iff.mpr, False.elim, Finset.HasAntidiagonal.mem_antidiagonal, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (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:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : φ * HPow.hPow (α := R⟦X⟧) X k = ψ * HPow.hPow (α := R⟦X⟧) X k
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 ⊢

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
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:
simpa using h (n + k)

Premises used: HAdd.hAdd
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
⊢ Function.Injective (β := R⟦X⟧) fun (x : R⟦X⟧) ↦ x * HPow.hPow (α := R⟦X⟧) X k

Tactic:
fun _ _ ↦ mul_X_pow_cancel

Premises used: PowerSeries.mul_X_pow_cancel, Function.Injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
⊢ φ * HPow.hPow (α := R⟦X⟧) X k = ψ * HPow.hPow (α := R⟦X⟧) X k ↔ φ = ψ

Tactic:
mul_X_pow_injective.eq_iff

Premises used: Function.Injective.eq_iff, PowerSeries.mul_X_pow_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
h : HPow.hPow (α := R⟦X⟧) X k * φ = HPow.hPow (α := R⟦X⟧) X k * ψ
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 ⊢

Premises used: PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
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:
simpa using h (n + k)

Premises used: HAdd.hAdd
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
⊢ Function.Injective (β := R⟦X⟧) fun (x : R⟦X⟧) ↦ HPow.hPow (α := R⟦X⟧) X k * x

Tactic:
fun _ _ ↦ X_pow_mul_cancel

Premises used: Function.Injective, PowerSeries.X_pow_mul_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
φ ψ : R⟦X⟧
⊢ HPow.hPow (α := R⟦X⟧) X k * φ = HPow.hPow (α := R⟦X⟧) X k * ψ ↔ φ = ψ

Tactic:
X_pow_mul_injective.eq_iff

Premises used: Function.Injective.eq_iff, PowerSeries.X_pow_mul_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
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)
neg : ∀ (h : ¬n ≤ d), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) (0 : R)
⊢ 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)

Tactic:
split_ifs with h