awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n k : ℕ
rw :
  ∑ b ∈ range (n + 1),
      (HMul.hMul (α := ℤ[X])
            ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) b * (↑(n.choose b) : ℤ) * (↑((n + b).choose n) : ℤ)) : ℤ[X])
            (HPow.hPow (α := ℤ[X]) X b)).coeff
        k =
    HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
⊢ (shiftedLegendre n).coeff k = HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)

Tactic:
rw [shiftedLegendre, finsetSum_coeff]

Premises used: Polynomial.finsetSum_coeff, Polynomial.shiftedLegendre
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n k : ℕ
simp_rw :
  (∑ x ∈ range (n + 1),
      if k = x then HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ) * (↑((n + x).choose n) : ℤ) else 0) =
    HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
⊢ ∑ b ∈ range (n + 1),
      (HMul.hMul (α := ℤ[X])
            ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) b * (↑(n.choose b) : ℤ) * (↑((n + b).choose n) : ℤ)) : ℤ[X])
            (HPow.hPow (α := ℤ[X]) X b)).coeff
        k =
    HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)

Tactic:
simp_rw [coeff_C_mul_X_pow]

Premises used: Polynomial.coeff_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n k : ℕ
⊢ (∑ x ∈ range (n + 1),
      if k = x then HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ) * (↑((n + x).choose n) : ℤ) else 0) =
    HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)

Tactic:
simp +contextual [choose_eq_zero_of_lt]

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ (shiftedLegendre n).degree = (↑n : WithBot ℕ)

Tactic:
le_antisymm ?_ (le_degree_of_ne_zero ?_)

Premises used: le_antisymm, Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
refine_1 : (shiftedLegendre n).degree ≤ (↑n : WithBot ℕ)
refine_2 : (shiftedLegendre n).coeff n ≠ 0
⊢ (shiftedLegendre n).degree = (↑n : WithBot ℕ)

Tactic:
refine le_antisymm ?_ (le_degree_of_ne_zero ?_)

Premises used: le_antisymm, Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
refine_1 : ∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑m : WithBot ℕ) → (shiftedLegendre n).coeff m = 0
⊢ (shiftedLegendre n).degree ≤ (↑n : WithBot ℕ)

Tactic:
rw [degree_le_iff_coeff_zero]

Premises used: Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n k : ℕ
h : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑k : WithBot ℕ)
⊢ n < k

Tactic:
norm_cast at h
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n k : ℕ
h : n < k
⊢ (shiftedLegendre n).coeff k = 0

Tactic:
simp [coeff_shiftedLegendre, choose_eq_zero_of_lt h]

Premises used: Polynomial.coeff_shiftedLegendre, Nat.choose_eq_zero_of_lt
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ n ≤ n + n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ (shiftedLegendre n).coeff n ≠ 0

Tactic:
simp [coeff_shiftedLegendre, (choose_pos (show n ≤ n + n by simp)).ne']

Premises used: Polynomial.coeff_shiftedLegendre, LT.lt.ne', Nat.choose_pos
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ (shiftedLegendre n).natDegree = n

Tactic:
natDegree_eq_of_degree_eq_some (degree_shiftedLegendre n)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_shiftedLegendre
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X) = shiftedLegendre n

Tactic:
nat_mul_inj' ?_ (factorial_ne_zero n)

Premises used: Nat.factorial_ne_zero, nat_mul_inj'
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
refine :
  (↑n ! : ℤ[X]) * (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
⊢ HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X) = shiftedLegendre n

Tactic:
refine nat_mul_inj' ?_ (factorial_ne_zero n)

Premises used: Nat.factorial_ne_zero, nat_mul_inj'
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
rw :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      ((HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n)
⊢ (↑n ! : ℤ[X]) * (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
    (↑n ! : ℤ[X]) * shiftedLegendre n

Tactic:
rw [← mul_assoc, mul_comm (n ! : ℤ[X]), mul_assoc, ← natCast_mul_comp,
    factorial_mul_shiftedLegendre_eq, ← iterate_derivative_comp_one_sub_X]

Premises used: mul_assoc, Polynomial.iterate_derivative_comp_one_sub_X, Nat.cast, Polynomial.factorial_mul_shiftedLegendre_eq, Nat.factorial, mul_comm, Polynomial.natCast_mul_comp
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      ((HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
R : Type u_1
inst : Ring R
x : R
⊢ Eq (α := R)
    ((aeval x : (a : ℤ[X]) → R) (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) :
      R)
    ((aeval x : (a : ℤ[X]) → R) (shiftedLegendre n) : R)

Tactic:
have := congr(aeval x $(neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq n))
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
R : Type u_1
inst : Ring R
x : R
this :
  Eq (α := R)
    ((aeval x : (a : ℤ[X]) → R) (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) :
      R)
    ((aeval x : (a : ℤ[X]) → R) (shiftedLegendre n) : R)
⊢ (aeval x : (a : ℤ[X]) → R) (shiftedLegendre n) =
    HMul.hMul (β := R) (HPow.hPow (α := R) (-1) n) ((aeval (1 - x) : (a : ℤ[X]) → R) (shiftedLegendre n) : R)

Tactic:
simpa [aeval_comp] using this.symm

Premises used: Polynomial.aeval_comp, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : (s : (a : Unit) → ℕ) () = n
rw : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () n)) (MvPowerSeries.coeff s)
rw₁ :
  Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () ((s : (a : Unit) → ℕ) ()))) (MvPowerSeries.coeff s)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff s) (MvPowerSeries.coeff s)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (coeff n) (MvPowerSeries.coeff s)

Tactic:
rw [coeff, ← h, ← Finsupp.unique_single s]

Premises used: Finsupp.unique_single, PowerSeries.coeff
-- 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) φ : 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) → ℕ) () : ℕ)
rw₂ : ℕ
⊢ Eq (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) φ : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) ψ : R)

Tactic:
rw [← coeff_def]

Premises used: PowerSeries.coeff_def
-- 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) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
n : Unit →₀ ℕ
⊢ Eq (α := R) ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) φ : R)
    ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) ψ : R)

Tactic:
apply h
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
simp : ∀ (x y : R⟦X⟧) (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) x : R) ((coeff n : (a : R⟦X⟧) → R) y : R)
⊢ Subsingleton.{u_1 + 1} R⟦X⟧

Tactic:
simp only [subsingleton_iff, PowerSeries.ext_iff]

Premises used: subsingleton_iff, PowerSeries.ext_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
⊢ ∀ (x y : R⟦X⟧) (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) x : R) ((coeff n : (a : R⟦X⟧) → R) y : R)

Tactic:
subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : ℕ → R
⊢ (coeff n : (a : R⟦X⟧) → R) (mk f) = f n

Tactic:
congr_arg f Finsupp.single_eq_same

Premises used: Finsupp.single_eq_same, congr_arg, PowerSeries.mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
a : R
⊢ (if Eq (α := Unit →₀ ℕ) (single () m) (single () n) then a else 0) = if m = n then a else 0

Tactic:
simp only [Finsupp.unique_single_eq_iff]

Premises used: Finsupp.unique_single_eq_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
rw₁ rw₂ : (if m = n then a else 0) = 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)

Tactic:
rw [coeff_monomial, coeff_mk]

Premises used: PowerSeries.coeff_mk, PowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ (coeff n : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) a : R⟦X⟧) = a

Tactic:
MvPowerSeries.coeff_monomial_same _ _

Premises used: MvPowerSeries.coeff_monomial_same
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ coeff n ∘ₗ monomial n = LinearMap.id

Tactic:
LinearMap.ext <| coeff_monomial_same n

Premises used: LinearMap.ext, PowerSeries.coeff_monomial_same
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
a b : R
⊢ HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) ((monomial m : (a : R) → R⟦X⟧) a : R⟦X⟧) ((monomial n : (a : R) → R⟦X⟧) b : R⟦X⟧) =
    (monomial (m + n) : (a : R) → R⟦X⟧) (a * b)

Tactic:
simpa [monomial] using
    MvPowerSeries.monomial_mul_monomial (Finsupp.single () m) (Finsupp.single () n) a b

Premises used: Unit.unit, PowerSeries.monomial, MvPowerSeries.monomial_mul_monomial, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit R) → R) f : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
⊢ Eq (α := R →+* R⟦X⟧) (algebraMap R R⟦X⟧) C

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, PowerSeries.C, rfl, MvPowerSeries.C
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Commute φ X

Tactic:
MvPowerSeries.commute_X _ _

Premises used: MvPowerSeries.commute_X, PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ X * φ = φ * X

Tactic:
MvPowerSeries.X_mul

Premises used: PowerSeries.X, MvPowerSeries.X_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ Commute φ (HPow.hPow (α := R⟦X⟧) X n)

Tactic:
MvPowerSeries.commute_X_pow _ _ _

Premises used: MvPowerSeries.commute_X_pow, PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ HPow.hPow (α := R⟦X⟧) X n * φ = φ * HPow.hPow (α := R⟦X⟧) X n

Tactic:
MvPowerSeries.X_pow_mul

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

Tactic:
rw [coeff, Finsupp.single_zero]

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

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

Tactic:
rw [coeff_zero_eq_constantCoeff]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := (a : R) → R⟦X⟧) (⇑MvPowerSeries.C : (a : R) → MvPowerSeries Unit R) (⇑C : (a : R) → R⟦X⟧)
⊢ Eq.{u_1 + 1} (α := (a : R) → R⟦X⟧) (⇑(monomial 0) : (a : R) → R⟦X⟧) (⇑C : (a : R) → R⟦X⟧)

Tactic:
rw [monomial, Finsupp.single_zero, MvPowerSeries.monomial_zero_eq_C]

Premises used: MvPowerSeries.monomial_zero_eq_C, PowerSeries.monomial, Finsupp.single_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := (a : R) → R⟦X⟧) (⇑MvPowerSeries.C : (a : R) → MvPowerSeries Unit R) (⇑C : (a : R) → R⟦X⟧)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq (α := R⟦X⟧) ((monomial 0 : (a : R) → R⟦X⟧) a : R⟦X⟧) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
rw₁ rw₂ : (if n = 0 then a else 0) = 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

Tactic:
rw [← monomial_zero_eq_C_apply, coeff_monomial]

Premises used: PowerSeries.coeff_monomial, PowerSeries.monomial_zero_eq_C_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
rw : (if Eq (α := ℕ) 0 0 then a else 0) = a
rw₁ rw₂ : a = a
⊢ (coeff 0 : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) = a

Tactic:
rw [coeff_C, if_pos rfl]

Premises used: if_pos, PowerSeries.coeff_C, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
h : n ≠ 0
rw : (if n = 0 then a else 0) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)

Tactic:
rw [coeff_C, if_neg h]

Premises used: PowerSeries.coeff_C, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) a : R⟦X⟧) : R) (0 : R)

Tactic:
coeff_C_of_ne_zero n.succ_ne_zero

Premises used: PowerSeries.coeff_C_of_ne_zero, Nat.succ_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := R⟦X⟧) (⇑C : (a : R) → R⟦X⟧)

Tactic:
MvPowerSeries.C_injective

Premises used: MvPowerSeries.C_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Subsingleton.{u_1 + 1} R⟦X⟧ ↔ Subsingleton R

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
refine : ∀ (h : Subsingleton.{u_1 + 1} R⟦X⟧), Subsingleton R
⊢ Subsingleton.{u_1 + 1} R⟦X⟧ ↔ Subsingleton R

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
h : Subsingleton.{u_1 + 1} R⟦X⟧
rw : ∀ (h : ∀ (x y : R⟦X⟧), x = y) (x y : R), x = y
⊢ Subsingleton R

Tactic:
rw [subsingleton_iff] at h ⊢

Premises used: subsingleton_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y

Tactic:
fun a b ↦ C_injective (h (C a) (C b))

Premises used: PowerSeries.C_injective, PowerSeries.C, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y

Tactic:
exact fun a b ↦ C_injective (h (C a) (C b))

Premises used: PowerSeries.C_injective, PowerSeries.C, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) X ((monomial 1 : (a : R) → R⟦X⟧) 1)

Tactic:
rfl

Premises used: PowerSeries.X, MvPowerSeries.X, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (if n = 1 then 1 else 0) (if n = 1 then 1 else 0)
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) X : R) (if n = 1 then 1 else 0 : R)

Tactic:
rw [X_eq, coeff_monomial]

Premises used: PowerSeries.X_eq, PowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) X : R) (0 : R)

Tactic:
rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]

Premises used: PowerSeries.coeff, PowerSeries.X, MvPowerSeries.coeff_zero_X, Finsupp.single_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
rw : Eq.{u_1 + 1} (α := R) (if Eq (α := ℕ) 1 1 then 1 else 0) 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) ((coeff 1 : (a : R⟦X⟧) → R) X : R) (1 : R)

Tactic:
rw [coeff_X, if_pos rfl]

Premises used: if_pos, PowerSeries.coeff_X, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
H : Eq.{u_1 + 1} (α := R⟦X⟧) X 0
⊢ False

Tactic:
simpa only [coeff_one_X, one_ne_zero, map_zero] using congr_arg (coeff 1) H

Premises used: map_zero, PowerSeries.coeff, congr_arg, one_ne_zero, OfNat.ofNat, DFunLike.coe, PowerSeries.coeff_one_X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ HPow.hPow (α := R⟦X⟧) X n = (monomial n : (a : R) → R⟦X⟧) 1

Tactic:
MvPowerSeries.X_pow_eq _ n

Premises used: MvPowerSeries.X_pow_eq, PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (if m = n then 1 else 0) (if m = n then 1 else 0)
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (if m = n then 1 else 0 : R)

Tactic:
rw [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
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (if n = n then 1 else 0) 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) (1 : R)

Tactic:
rw [coeff_X_pow, if_pos rfl]

Premises used: if_pos, PowerSeries.coeff_X_pow, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 1 : R) (if n = 0 then 1 else 0 : R)

Tactic:
coeff_C n 1

Premises used: Function.update, Pi.single, dite, PowerSeries.coeff_C, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) 1 : R) (1 : R)

Tactic:
coeff_zero_C 1

Premises used: Function.update, Pi.single, dite, PowerSeries.coeff_zero_C, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)

Tactic:
(MvPowerSeries.coeff_mul _ φ ψ).trans ?_

Premises used: Eq.trans, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
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))
⊢ 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)

Tactic:
refine (MvPowerSeries.coeff_mul _ φ ψ).trans ?_

Premises used: Eq.trans, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
rw :
  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))
⊢ 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:
rw [Finsupp.antidiagonal_single, Finset.sum_map]

Premises used: Finset.sum_map, Finsupp.antidiagonal_single