-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_eq_zero_iff [IsDomain R]
    (n : ℕ) (r : R) : (ascPochhammer R n).eval r = 0 ↔ ∃ k < n, k = -r

Proof state:
case refine_1.zero
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
zero' : eval r (ascPochhammer R 0) = 0
⊢ ∃ k < 0, ↑k = -r

Tactic:
simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'

Result:
no goals

Proof state:
case refine_1.succ.inl.intro.intro
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
rn : ℕ
hrn : rn < n
rrn : ↑rn = -r
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
exact ⟨rn, by omega, rrn⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, ↑k = -r

Tactic:
refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩

Result:
case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
zero' : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n, ↑k = -r

case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, ↑k = -r
⊢ eval r (ascPochhammer R n) = 0

Proof state:
case refine_1.succ.inl
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
obtain ⟨rn, hrn, rrn⟩ := ih h

Result:
case refine_1.succ.inl.intro.intro
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
rn : ℕ
hrn : rn < n
rrn : ↑rn = -r
⊢ ∃ k < n + 1, ↑k = -r

Proof state:
case h.e'_2.h.e'_3
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ r = -↑rn

Tactic:
simp [rnn]

Result:
no goals

Proof state:
case refine_2.intro.intro
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ eval r (ascPochhammer R n) = 0

Tactic:
convert ascPochhammer_eval_neg_coe_nat_of_lt hrn

Result:
case h.e'_2.h.e'_3
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ r = -↑rn

Proof state:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, ↑k = -r
⊢ eval r (ascPochhammer R n) = 0

Tactic:
obtain ⟨rn, hrn, rnn⟩ := hrn

Result:
case refine_2.intro.intro
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ eval r (ascPochhammer R n) = 0

Proof state:
case refine_1.succ.inr
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : r + ↑n = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩

Result:
no goals

Proof state:
case refine_1.succ
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
zero' : eval r (ascPochhammer R n) = 0 ∨ r + ↑n = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
cases zero' with
| inl h =>
  obtain ⟨rn, hrn, rrn⟩ := ih h
  exact ⟨rn, by omega, rrn⟩
| inr h =>
  exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
zero' : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n, ↑k = -r

Tactic:
induction n with
| zero => simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'
| succ n ih =>
  rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'
  cases zero' with
  | inl h =>
    obtain ⟨rn, hrn, rrn⟩ := ih h
    exact ⟨rn, by omega, rrn⟩
  | inr h =>
    exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩

Result:
no goals

Proof state:
case refine_1.succ
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
zero' : eval r (ascPochhammer R (n + 1)) = 0
⊢ ∃ k < n + 1, ↑k = -r

Tactic:
rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'

Result:
case refine_1.succ
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
zero' : eval r (ascPochhammer R n) = 0 ∨ r + ↑n = 0
⊢ ∃ k < n + 1, ↑k = -r

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
n : ℕ
ih : eval r (ascPochhammer R n) = 0 → ∃ k < n, ↑k = -r
h : eval r (ascPochhammer R n) = 0
rn : ℕ
hrn : rn < n
rrn : ↑rn = -r
⊢ rn < n + 1

Tactic:
omega

Result:
no goals