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
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)
⊢ 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 neg : ∀ (h : ¬n ≤ d), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (p * HPow.hPow (α := R⟦X⟧) X n) : R) (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)
have 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)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have pos₁ : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have pos₂ : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
have 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
Tactic: refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
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
have neg : ¬x.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⟧
n d : ℕ
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬n ≤ d), Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R)
have pos : Eq (α := R) ((coeff (d - n) : (a : R⟦X⟧) → R) p : R) ((coeff (d - n + n - n) : (a : R⟦X⟧) → R) p : R)
Tactic: rw [← tsub_add_cancel_of_le h, coeff_X_pow_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 : ¬n ≤ d
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X n * p) : R) (0 : R)
have 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
Tactic: refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
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
have neg : ¬x.1 = n
Tactic: rw [coeff_X_pow, if_neg, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
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 = n
have this : x.1 + x.2 = d
Tactic: have := mem_antidiagonal.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
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.1 = n
have this₁ : x.2 + x.1 = d
Tactic: rw [add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ =
    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⟧)
have 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)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ φ =
    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⟧)
have 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)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ =
    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⟧)
have 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)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ φ =
    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⟧)
have 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)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
r : R
⊢ 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⟧)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
⊢ Eq.{u_2 + 1} (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) X : S⟦X⟧) (X : S⟦X⟧)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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⟧
⊢ ∃ (a : S⟦X⟧), (map f : (a : S⟦X⟧) → T⟦X⟧) a = g
have h : (map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) = g
Tactic: use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff k g)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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⟧
⊢ (map f : (a : S⟦X⟧) → T⟦X⟧) (mk fun (k : ℕ) ↦ Function.surjInv hf ((coeff k : (a : T⟦X⟧) → T) g)) = g
have 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)
Tactic: ext k
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
    ((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)
have 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)) sorry) :
    T)
  ((coeff k : (a : T⟦X⟧) → T) g : T)
Tactic: simp only [Function.surjInv, coeff_map, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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⟧)
⊢ u = v
have h : ∀ (k : ℕ), Eq (α := S) ((coeff k : (a : S⟦X⟧) → S) u : S) ((coeff k : (a : S⟦X⟧) → S) v : S)
Tactic: ext k
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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 : ℕ
⊢ Eq (α := S) ((coeff k : (a : S⟦X⟧) → S) u : S) ((coeff k : (a : S⟦X⟧) → S) v : S)
have 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)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ HPow.hPow (α := R⟦X⟧) X n ∣ φ ↔ ∀ m < n, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
have 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)
Tactic: convert! @MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ (∀ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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 m : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
have h₁ : Eq (α := R)
  ((MvPowerSeries.coeff (single default ((m : (a : Unit) → ℕ) default)) : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
Tactic: rw [Finsupp.unique_single m]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)
have h₁ : (single () m : (a : Unit) → ℕ) () < n
Tactic: apply h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ X ∣ φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
have 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)
Tactic: rw [← pow_one (X : R⟦X⟧), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ (∀ m < 1, Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔
    Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
n : ℕ
⊢ Eq (α := R) ((↑((coeff n : (a : (↥T)⟦X⟧) → ↥T) (p.toSubring T hp)) : R) : R) ((coeff n : (a : R⟦X⟧) → R) p : R)
have rw : (↑((coeff n : (a : (↥T)⟦X⟧) → ↥T)
        (mk fun (n : ℕ) ↦ Subtype.mk (p := fun (x : R) ↦ x ∈ T) ((coeff n : (a : R⟦X⟧) → R) p) sorry)) :
    R) =
  (coeff n : (a : R⟦X⟧) → R) p
Tactic: rw [toSubring, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
n : ℕ
rw :
  (↑((coeff n : (a : (↥T)⟦X⟧) → ↥T)
          (mk fun (n : ℕ) ↦ Subtype.mk (p := fun (x : R) ↦ x ∈ T) ((coeff n : (a : R⟦X⟧) → R) p) ⋯)) :
      R) =
    (coeff n : (a : R⟦X⟧) → R) p
⊢ Eq (α := R) ((↑((coeff n : (a : (↥T)⟦X⟧) → ↥T) (p.toSubring T hp)) : R) : R) ((coeff n : (a : R⟦X⟧) → R) p : R)
have rw₁ : Eq (α := R) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) ((coeff n : (a : R⟦X⟧) → R) p) sorry) : R) : R)
  ((coeff n : (a : R⟦X⟧) → R) p : R)
Tactic: rw [toSubring, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) 1
have h : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 1 : R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 1 : R)
have h : (if n = 0 then a ^ n else 0) = if n = 0 then 1 else 0
Tactic: simp only [mul_boole, PowerSeries.coeff_mk, PowerSeries.coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
⊢ (if n = 0 then a ^ n else 0) = if n = 0 then 1 else 0
have pos : ∀ (h : n = 0), a ^ n = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
pos : ∀ (h : n = 0), a ^ n = 1
⊢ (if n = 0 then a ^ n else 0) = if n = 0 then 1 else 0
have neg : ∀ (h : ¬n = 0), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
h : n = 0
⊢ a ^ n = 1
have pos : HPow.hPow (β := ℕ) a 0 = 1
Tactic: rw [h, pow_zero a]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
h : n = 0
pos : HPow.hPow (β := ℕ) a 0 = 1
⊢ a ^ n = 1
have pos₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [h, pow_zero a]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
⊢ (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)) =
    HMul.hMul (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R))
      (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R))
have h : ∀ (n : ℕ),
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R))
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R))) :
      R)
Tactic: ext