awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
pos :
  Eq (α := R) ((coeff (d - n + n) : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R)
    ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)
pos₁ : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)
pos₂ pos₃ : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)
⊢ 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:
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Premises used: tsub_add_cancel_of_le, add_tsub_cancel_right, PowerSeries.coeff_mul_X_pow
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) (0 : R)

Tactic:
(coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, PowerSeries.coeff_mul, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
neg :
  ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) p : R)
        ((coeff x.2 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R) =
      0
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) (0 : R)

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, PowerSeries.coeff_mul, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
neg : ¬x.2 = n
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) p : R)
      ((coeff x.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⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ ¬x.2 = n

Tactic:
((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ ¬x.2 = n

Tactic:
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- 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) (HPow.hPow (α := R⟦X⟧) X n * p) : R)
      ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)
neg : ∀ (h : ¬n ≤ d), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) (0 : R)
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R)
    (if n ≤ d then (coeff (d - n) : (a : R⟦X⟧) → R) p else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
pos : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]

Premises used: tsub_add_cancel_of_le, PowerSeries.coeff_X_pow_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) (0 : R)

Tactic:
(coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, PowerSeries.coeff_mul, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
neg :
  ∀ (x : ℕ × ℕ) (hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
        ((coeff x.2 : (a : R⟦X⟧) → R) p : R) =
      0
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) (0 : R)

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Premises used: Finset.sum_eq_zero, PowerSeries.coeff_mul, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
neg : ¬x.1 = n
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n) : R)
      ((coeff x.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⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
⊢ x.1 + x.2 = d

Tactic:
have := mem_antidiagonal.mp hx
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
this : x.1 + x.2 = d
⊢ x.2 + x.1 = d

Tactic:
rw [add_comm] at this

Premises used: add_comm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
this : x.2 + x.1 = d
⊢ ¬x.1 = n

Tactic:
((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ d
this : x.2 + x.1 = d
⊢ ¬x.1 = n

Tactic:
exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

Premises used: not_le, le_of_add_le_right, Eq.le, Iff.mp, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : IsUnit φ
⊢ IsUnit (M := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)

Tactic:
MvPowerSeries.isUnit_constantCoeff φ h

Premises used: MvPowerSeries.isUnit_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h :
  Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X)
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) φ : R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X)
            ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
        R)
⊢ φ =
    HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X)
      ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)

Tactic:
ext (_ | n)
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X)
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) φ : R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X)
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)

Tactic:
simp only [coeff_succ_mul_X, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

Premises used: PowerSeries.coeff_succ_mul_X, if_false, map_add, PowerSeries.coeff_mk, Nat.succ_ne_zero, PowerSeries.coeff_C, add_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h :
  Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ))
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) φ : R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ))
            ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
        R)
⊢ φ =
    HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ))
      ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)

Tactic:
ext (_ | n)
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
    ((coeff 0 : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ))
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) φ : R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (β := R⟦X⟧) (HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ))
          ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧)) :
      R)

Tactic:
simp only [coeff_succ_X_mul, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

Premises used: if_false, map_add, PowerSeries.coeff_mk, Nat.succ_ne_zero, PowerSeries.coeff_C, PowerSeries.coeff_succ_X_mul, add_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := (a : R⟦X⟧) → R⟦X⟧) (⇑(map (RingHom.id R)) : (a : R⟦X⟧) → R⟦X⟧) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
T : Type u_3
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: MvPowerSeries.map, PowerSeries.map, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) φ : S⟦X⟧) : S)
    ((f : (a : R) → S) ((coeff n : (a : R⟦X⟧) → R) φ : R) : 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
f : R →+* S
r : R
h :
  ∀ (n : ℕ),
    Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) ((C : (a : R) → R⟦X⟧) r) : S⟦X⟧) : S)
      ((coeff n : (a : S⟦X⟧) → S) ((C : (a : S) → S⟦X⟧) ((f : (a : R) → S) r : S) : S⟦X⟧) : S)
⊢ Eq (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) ((C : (a : R) → R⟦X⟧) r) : S⟦X⟧)
    ((C : (a : S) → S⟦X⟧) ((f : (a : R) → S) r : S) : S⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
r : R
n : ℕ
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) ((C : (a : R) → R⟦X⟧) r) : S⟦X⟧) : S)
    ((coeff n : (a : S⟦X⟧) → S) ((C : (a : S) → S⟦X⟧) ((f : (a : R) → S) r : S) : S⟦X⟧) : S)

Tactic:
simp [coeff_C, apply_ite f]

Premises used: apply_ite, PowerSeries.coeff_C, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) X : S⟦X⟧) : S)
      ((coeff n : (a : S⟦X⟧) → S) X : S)
⊢ Eq.{u_2 + 1} (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) X : S⟦X⟧) (X : S⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ Eq.{u_2 + 1} (α := S) ((coeff n : (a : S⟦X⟧) → S) ((map f : (a : R⟦X⟧) → S⟦X⟧) X : S⟦X⟧) : S)
    ((coeff n : (a : S⟦X⟧) → S) X : S)

Tactic:
simp [coeff_X, apply_ite f]

Premises used: apply_ite, PowerSeries.coeff_X, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
g : T⟦X⟧
h : (map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) = g
⊢ ∃ (a : S⟦X⟧), (map f : (a : S⟦X⟧) → T⟦X⟧) a = g

Tactic:
use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff k g)

Premises used: PowerSeries.coeff, Function.surjInv, PowerSeries.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
g : T⟦X⟧
h :
  ∀ (k : ℕ),
    Eq.{u_3 + 1} (α := T)
      ((coeff k : (a : T⟦X⟧) → T)
          ((map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) : T⟦X⟧) :
        T)
      ((coeff k : (a : T⟦X⟧) → T) g : T)
⊢ (map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) = g

Tactic:
ext k
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
g : T⟦X⟧
k : ℕ
h :
  Eq.{u_3 + 1} (α := T)
    ((f : (a : S) → T)
        (Classical.choose (p := fun (x : S) ↦
          Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((coeff k : (a : T⟦X⟧) → T) g : T)) ⋯) :
      T)
    ((coeff k : (a : T⟦X⟧) → T) g : T)
⊢ Eq.{u_3 + 1} (α := T)
    ((coeff k : (a : T⟦X⟧) → T)
        ((map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) : T⟦X⟧) :
      T)
    ((coeff k : (a : T⟦X⟧) → T) g : T)

Tactic:
simp only [Function.surjInv, coeff_map, coeff_mk]

Premises used: PowerSeries.coeff_mk, Function.surjInv, PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
g : T⟦X⟧
k : ℕ
⊢ Eq.{u_3 + 1} (α := T)
    ((f : (a : S) → T)
        (Classical.choose (p := fun (x : S) ↦
          Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((coeff k : (a : T⟦X⟧) → T) g : T)) ⋯) :
      T)
    ((coeff k : (a : T⟦X⟧) → T) g : T)

Tactic:
Classical.choose_spec (hf (coeff k g))

Premises used: PowerSeries.coeff, Classical.choose_spec, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
g : T⟦X⟧
k : ℕ
⊢ Eq.{u_3 + 1} (α := T)
    ((f : (a : S) → T)
        (Classical.choose (p := fun (x : S) ↦
          Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) x : T) ((coeff k : (a : T⟦X⟧) → T) g : T)) ⋯) :
      T)
    ((coeff k : (a : T⟦X⟧) → T) g : T)

Tactic:
exact Classical.choose_spec (hf (coeff k g))

Premises used: PowerSeries.coeff, Classical.choose_spec, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
u v : S⟦X⟧
huv : Eq.{u_3 + 1} (α := T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) u : T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧)
h : ∀ (k : ℕ), Eq (α := S) ((coeff k : (a : S⟦X⟧) → S) u : S) ((coeff k : (a : S⟦X⟧) → S) v : S)
⊢ u = v

Tactic:
ext k
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
u v : S⟦X⟧
huv : Eq.{u_3 + 1} (α := T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) u : T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧)
k : ℕ
h :
  Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) ((coeff k : (a : S⟦X⟧) → S) u : S) : T)
    ((f : (a : S) → T) ((coeff k : (a : S⟦X⟧) → S) v : S) : T)
⊢ Eq (α := S) ((coeff k : (a : S⟦X⟧) → S) u : S) ((coeff k : (a : S⟦X⟧) → S) v : S)

Tactic:
apply hf
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
S : Type u_2
T : Type u_3
inst : Semiring S
inst_1 : Semiring T
f : S →+* T
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
u v : S⟦X⟧
huv : Eq.{u_3 + 1} (α := T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) u : T⟦X⟧) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧)
k : ℕ
h :
  Eq.{u_3 + 1} (α := T) ((coeff k : (a : T⟦X⟧) → T) ((map f : (a : S⟦X⟧) → T⟦X⟧) u : T⟦X⟧) : T)
    ((f : (a : S) → T) ((coeff k : (a : S⟦X⟧) → S) v : S) : T)
h₁ :
  Eq.{u_3 + 1} (α := T) ((coeff k : (a : T⟦X⟧) → T) ((map f : (a : S⟦X⟧) → T⟦X⟧) u : T⟦X⟧) : T)
    ((coeff k : (a : T⟦X⟧) → T) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧) : T)
h₂ h₃ :
  Eq.{u_3 + 1} (α := T) ((coeff k : (a : T⟦X⟧) → T) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧) : T)
    ((coeff k : (a : T⟦X⟧) → T) ((map f : (a : S⟦X⟧) → T⟦X⟧) v : T⟦X⟧) : T)
⊢ Eq.{u_3 + 1} (α := T) ((f : (a : S) → T) ((coeff k : (a : S⟦X⟧) → S) u : S) : T)
    ((f : (a : S) → T) ((coeff k : (a : S⟦X⟧) → S) v : S) : T)

Tactic:
rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]

Premises used: PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : R⟦X⟧
f : R →+* S
⊢ Eq.{u_3 + 1} (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) φ : S⟦X⟧) (0 : S⟦X⟧) ↔ φ = 0

Tactic:
MvPowerSeries.map_eq_zero _ _

Premises used: MvPowerSeries.map_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ HPow.hPow (α := MvPowerSeries Unit R) (MvPowerSeries.X ()) n ∣ φ ↔
    ∀ (m : Unit →₀ ℕ),
      (m : (a : Unit) → ℕ) () < n → Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)

Tactic:
@MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ

Premises used: MvPowerSeries.X_pow_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h :
  (∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    ∀ (m : Unit →₀ ℕ),
      (m : (a : Unit) → ℕ) () < n → Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
⊢ HPow.hPow (α := R⟦X⟧) X n ∣ φ ↔ ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
convert! @MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ

Premises used: MvPowerSeries.X_pow_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h :
  (∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) →
    ∀ (m : Unit →₀ ℕ),
      (m : (a : Unit) → ℕ) () < n → Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
h₁ :
  (∀ (m : Unit →₀ ℕ),
      (m : (a : Unit) → ℕ) () < n →
        Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)) →
    ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    ∀ (m : Unit →₀ ℕ),
      (m : (a : Unit) → ℕ) () < n → Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
m : Unit →₀ ℕ
hm : (m : (a : Unit) → ℕ) () < n
h₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (single default ((m : (a : Unit) → ℕ) default)) : (a : MvPowerSeries Unit R) → R) φ : R)
    (0 : R)
⊢ Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)

Tactic:
rw [Finsupp.unique_single m]

Premises used: Finsupp.unique_single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
m : Unit →₀ ℕ
hm : (m : (a : Unit) → ℕ) () < n
⊢ Eq (α := R) ((coeff ((m : (a : Unit) → ℕ) ()) : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
h _ hm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
m : Unit →₀ ℕ
hm : (m : (a : Unit) → ℕ) () < n
⊢ Eq (α := R)
    ((MvPowerSeries.coeff (single default ((m : (a : Unit) → ℕ) default)) : (a : MvPowerSeries Unit R) → R) φ : R)
    (0 : R)

Tactic:
convert! h _ hm
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
h :
  ∀ (m : Unit →₀ ℕ),
    (m : (a : Unit) → ℕ) () < n → Eq (α := R) ((MvPowerSeries.coeff m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
m : ℕ
hm : m < n
h₁ : (single () m : (a : Unit) → ℕ) () < n
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)

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

Tactic:
simpa only [Finsupp.single_eq_same] using hm

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
rw :
  (∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ X ∣ φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
rw [← pow_one (X : R⟦X⟧), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]

Premises used: PowerSeries.X, PowerSeries.coeff_zero_eq_constantCoeff_apply, pow_one, PowerSeries.X_pow_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
mp :
  (∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) →
    Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
mpr :
  Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R) →
    ∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)

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

Tactic:
h 0 zero_lt_one

Premises used: zero_lt_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : ∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
exact h 0 zero_lt_one

Premises used: zero_lt_one, OfNat.ofNat