-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
theorem existsUnique_hilbertPoly (p : F[X]) (d : ℕ) :
    ∃! h : F[X], ∃ N : ℕ, ∀ n > N,
      PowerSeries.coeff F n (p * invOneSubPow F d) = h.eval (n : F)

Proof state:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ h = p.hilbertPoly d

Tactic:
apply eq_of_infinite_eval_eq h (hilbertPoly p d)

Result:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ {x | eval x h = eval x (p.hilbertPoly d)}.Infinite

Proof state:
case h.right.intro.intro.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : N < n ∧ p.natDegree < n
⊢ eval (↑n) h = eval (↑n) (p.hilbertPoly d)

Tactic:
rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > p.natDegree, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) (p.hilbertPoly d)

Tactic:
exact fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d) ∧
    ∀ (y : F[X]),
      (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Tactic:
constructor

Result:
case h.left
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d)

case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ (y : F[X]),
    (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Proof state:
case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ (y : F[X]),
    (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Tactic:
rintro h ⟨N, hhN⟩

Result:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ h = p.hilbertPoly d

Proof state:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ {x | eval x h = eval x (p.hilbertPoly d)}

Tactic:
rintro x ⟨n, hn, rfl⟩

Result:
case h.right.intro.intro.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : n ∈ Set.Ioi (N ⊔ p.natDegree)
⊢ ↑n ∈ {x | eval x h = eval x (p.hilbertPoly d)}

Proof state:
case h.right.intro.intro.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : n ∈ Set.Ioi (N ⊔ p.natDegree)
⊢ ↑n ∈ {x | eval x h = eval x (p.hilbertPoly d)}

Tactic:
simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hn ⊢

Result:
case h.right.intro.intro.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
n : ℕ
hn : N < n ∧ p.natDegree < n
⊢ eval (↑n) h = eval (↑n) (p.hilbertPoly d)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∃! h, ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h

Tactic:
use hilbertPoly p d

Result:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d) ∧
    ∀ (y : F[X]),
      (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Proof state:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ {x | eval x h = eval x (p.hilbertPoly d)}.Infinite

Tactic:
apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono

Result:
case h.right.intro
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
h : F[X]
N : ℕ
hhN : ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h
⊢ Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆ {x | eval x h = eval x (p.hilbertPoly d)}

Proof state:
case h.left
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (fun h => ∃ N, ∀ n > N, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) (p.hilbertPoly d)

Tactic:
use p.natDegree

Result:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > p.natDegree, (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) (p.hilbertPoly d)