awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
k : ℕ
rw :
  eval (-r) (ascPochhammer R k * HAdd.hAdd (α := R[X]) X (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X + HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₂ :
  eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) X) +
      eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₃ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (ascPochhammer R k) (↑k : R[X])) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₄ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (HMul.hMul (α := R[X]) (↑k : R[X]) (ascPochhammer R k)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₅ :
  eval (-r) (ascPochhammer R k) * -r + (↑k : R) * eval (-r) (ascPochhammer R k) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₆ :
  eval (-r) (ascPochhammer R k) * -r + eval (-r) (ascPochhammer R k) * (↑k : R) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₇ :
  eval (-r) (ascPochhammer R k) * (-r + (↑k : R)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₈ :
  HPow.hPow (α := R) (-1) k * eval r (descPochhammer R k) * (-r + (↑k : R)) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₉ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
rw₁₀ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R k * HSub.hSub (α := R[X]) X (↑k : R[X]))
rw₁₁ :
  HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
    HPow.hPow (α := R) (-1) (k + 1) *
      eval r (HMul.hMul (α := R[X]) (descPochhammer R k) X - HMul.hMul (α := R[X]) (descPochhammer R k) (↑k : R[X]))
⊢ eval (-r) (ascPochhammer R (k + 1)) = HPow.hPow (α := R) (-1) (k + 1) * eval r (descPochhammer R (k + 1))
have rw₁₂ : HPow.hPow (α := R) (-1) k * (eval r (descPochhammer R k) * (-r + (↑k : R))) =
  HPow.hPow (α := R) (-1) (k + 1) *
    (eval r (HMul.hMul (α := R[X]) (descPochhammer R k) X) -
      eval r (HMul.hMul (α := R[X]) (descPochhammer R k) (↑k : R[X])))
Tactic: rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      Nat.cast_comm, ← mul_add, ascPochhammer_eval_neg_eq_descPochhammer r k, mul_assoc,
      descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, eval_natCast_mul,
      pow_add, pow_one, mul_assoc ((-1) ^ k) (-1), mul_sub, neg_one_mul, neg_mul_eq_mul_neg,
      Nat.cast_comm, sub_eq_add_neg, neg_one_mul, neg_neg, ← mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
a b : ℕ
⊢ eval (HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
have rw : eval (↑(a + b) : ℤ) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
Tactic: rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
a b : ℕ
rw : eval (↑(a + b) : ℤ) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
⊢ eval (HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
have rw₁ : Eq (α := ℤ) (↑((a + b).descFactorial b) : ℤ) (↑((a + 1).ascFactorial b) : ℤ)
Tactic: rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
a b : ℕ
rw : eval (↑(a + b) : ℤ) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
rw₁ : Eq (α := ℤ) (↑((a + b).descFactorial b) : ℤ) (↑((a + 1).ascFactorial b) : ℤ)
⊢ eval (HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
have rw₂ : Eq (α := ℤ) (↑((a + 1).ascFactorial b) : ℤ) (↑((a + 1).ascFactorial b) : ℤ)
Tactic: rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-(↑k : R)) (ascPochhammer R (n + 1)) = 0
have succ : eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
Tactic: rw [ascPochhammer_succ_eval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
have succ : ∀ (hkn : k < n), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
Tactic: rcases lt_trichotomy k n with hkn | rfl | hkn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
succ : ∀ (hkn : k < n), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
have succ₁ : ∀ (ih : ∀ (h : k < k), eval (-(↑k : R)) (ascPochhammer R k) = 0) (h : k < k + 1),
  eval (-(↑k : R)) (ascPochhammer R k) * HAdd.hAdd (α := R) (-(↑k : R)) (↑k : R) = 0
Tactic: rcases lt_trichotomy k n with hkn | rfl | hkn
Cleared hypotheses: n, ih, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
succ : ∀ (hkn : k < n), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
succ₁ :
  ∀ (ih : ∀ (h : k < k), eval (-(↑k : R)) (ascPochhammer R k) = 0) (h : k < k + 1),
    eval (-(↑k : R)) (ascPochhammer R k) * HAdd.hAdd (α := R) (-(↑k : R)) (↑k : R) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
have succ₂ : ∀ (hkn : n < k), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
Tactic: rcases lt_trichotomy k n with hkn | rfl | hkn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n k : ℕ
h : k < n
⊢ eval (-(↑k : R)) (ascPochhammer R n) = 0
have zero : ∀ (h : k < 0), eval (-(↑k : R)) (ascPochhammer R 0) = 0
Tactic: induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · lia
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n k : ℕ
h : k < n
zero : ∀ (h : k < 0), eval (-(↑k : R)) (ascPochhammer R 0) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R n) = 0
have succ : ∀ (n : ℕ) (ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0) (h : k < n + 1),
  eval (-(↑k : R)) (ascPochhammer R (n + 1)) = 0
Tactic: induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · lia
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, (↑k : R) = -r
have refine_1 : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
Tactic: refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
refine_1 : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, (↑k : R) = -r
have refine_2 : ∀ (hrn : ∃ k < n, (↑k : R) = -r), eval r (ascPochhammer R n) = 0
Tactic: refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
n : ℕ
ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
zero' : eval r (ascPochhammer R (n + 1)) = 0
⊢ ∃ k < n + 1, (↑k : R) = -r
have zero'₁ : eval r (ascPochhammer R n) = 0 ∨ r + (↑n : R) = 0
Tactic: rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'
Cleared hypotheses: zero'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
n : ℕ
ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
h : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n + 1, (↑k : R) = -r
have refine_1 : ∀ (rn : ℕ) (hrn : rn < n) (rrn : (↑rn : R) = -r), ∃ k < n + 1, (↑k : R) = -r
Tactic: obtain ⟨rn, hrn, rrn⟩ := ih h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
n : ℕ
ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
zero' : eval r (ascPochhammer R n) = 0 ∨ r + (↑n : R) = 0
⊢ ∃ k < n + 1, (↑k : R) = -r
have refine_1 : ∀ (h : eval r (ascPochhammer R n) = 0), ∃ k < n + 1, (↑k : R) = -r
Tactic: cases zero' with
      | inl h =>
        obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by lia, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
Cleared hypotheses: zero'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
n : ℕ
ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
zero' : eval r (ascPochhammer R n) = 0 ∨ r + (↑n : R) = 0
refine_1 : ∀ (h : eval r (ascPochhammer R n) = 0), ∃ k < n + 1, (↑k : R) = -r
⊢ ∃ k < n + 1, (↑k : R) = -r
have refine_1₁ : ∀ (h : r + (↑n : R) = 0), ∃ k < n + 1, (↑k : R) = -r
Tactic: cases zero' with
      | inl h =>
        obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by lia, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
Cleared hypotheses: zero'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
zero' : eval r (ascPochhammer R n) = 0
⊢ ∃ k < n, (↑k : R) = -r
have refine_1 : ∀ (zero' : eval r (ascPochhammer R 0) = 0), ∃ k < 0, (↑k : R) = -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 lia, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
Cleared hypotheses: n, zero'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
zero' : eval r (ascPochhammer R n) = 0
refine_1 : ∀ (zero' : eval r (ascPochhammer R 0) = 0), ∃ k < 0, (↑k : R) = -r
⊢ ∃ k < n, (↑k : R) = -r
have refine_1₁ : ∀ (n : ℕ) (ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r)
  (zero' : eval r (ascPochhammer R (n + 1)) = 0), ∃ k < n + 1, (↑k : R) = -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 lia, rrn⟩
      | inr h =>
        exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
Cleared hypotheses: n, zero'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, (↑k : R) = -r
⊢ eval r (ascPochhammer R n) = 0
have refine_2 : ∀ (rn : ℕ) (hrn : rn < n) (rnn : (↑rn : R) = -r), eval r (ascPochhammer R n) = 0
Tactic: obtain ⟨rn, hrn, rnn⟩ := hrn
Cleared hypotheses: hrn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : (↑rn : R) = -r
⊢ eval r (ascPochhammer R n) = 0
have h : r = -(↑rn : R)
Tactic: convert! ascPochhammer_eval_neg_coe_nat_of_lt hrn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
k n : ℕ
h : k < n
⊢ eval (↑k : R) (descPochhammer R n) = 0
have rw : eval (-(↑(n - k.succ) : R)) (ascPochhammer R n) = 0
Tactic: rw [descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub,
    ← Nat.cast_add_one, ← neg_sub, ← Nat.cast_sub h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : R
⊢ eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - (↑j : R))
have zero : eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - (↑j : R))
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : R
zero : eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - (↑j : R))
⊢ eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - (↑j : R))
have succ : ∀ (n : ℕ) (ih : eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - (↑j : R))),
  eval r (descPochhammer R (n + 1)) = ∏ j ∈ Finset.range (n + 1), (r - (↑j : R))
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 < s
⊢ 0 < eval s (descPochhammer S n)
have h₁ : 0 < s - (↑n : S) + 1
Tactic: rw [← sub_pos, ← sub_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : 0 < s - (↑n : S) + 1
⊢ 0 < eval s (descPochhammer S n)
have rw : 0 < eval (s - (↑n : S) + 1) (ascPochhammer S n)
Tactic: rw [descPochhammer_eval_eq_ascPochhammer]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 ≤ s
⊢ 0 ≤ eval s (descPochhammer S n)
have inl : ∀ (heq : HSub.hSub (α := S) (↑n : S) 1 = s), 0 ≤ eval s (descPochhammer S n)
Tactic: rcases eq_or_lt_of_le h with heq | h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 ≤ s
inl : ∀ (heq : HSub.hSub (α := S) (↑n : S) 1 = s), 0 ≤ eval s (descPochhammer S n)
⊢ 0 ≤ eval s (descPochhammer S n)
have inr : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 < s), 0 ≤ eval s (descPochhammer S n)
Tactic: rcases eq_or_lt_of_le h with heq | h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 ≤ s
heq : HSub.hSub (α := S) (↑n : S) 1 = s
⊢ 0 ≤ eval s (descPochhammer S n)
have inl : LE.le.{u_1} (α := S) 0 (if n = 0 then 1 else 0)
Tactic: rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
n : ℕ
ih : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 ≤ s), (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
h : HSub.hSub (α := S) (↑(n + 1) : S) 1 ≤ s
⊢ (s - (↑(n + 1) : S) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))
have h₁ : 0 ≤ s - (↑n : S)
Tactic: rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
n : ℕ
ih : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 ≤ s), (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - (↑n : S)
⊢ (s - (↑(n + 1) : S) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))
have hsub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ s
Tactic: have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
n : ℕ
ih : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 ≤ s), (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - (↑n : S)
hsub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ s
⊢ (s - (↑(n + 1) : S) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))
have succ : (s - (↑n : S)) ^ n * (s - (↑n : S)) ≤ eval s (descPochhammer S n) * (s - (↑n : S))
Tactic: rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
n : ℕ
ih : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 ≤ s), (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
h : 0 ≤ s - (↑n : S)
hsub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ s
⊢ (s - (↑n : S)) ^ n * (s - (↑n : S)) ≤ eval s (descPochhammer S n) * (s - (↑n : S))
have apply : (s - (↑n : S)) ^ n ≤ eval s (descPochhammer S n)
Tactic: apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 ≤ s
⊢ (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
have zero : ∀ (h : HSub.hSub (α := S) (↑0 : S) 1 ≤ s), HPow.hPow (β := ℕ) (s - (↑0 : S) + 1) 0 ≤ eval s (descPochhammer S 0)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
    have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
    rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
    apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
    exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : HSub.hSub (α := S) (↑n : S) 1 ≤ s
zero : ∀ (h : HSub.hSub (α := S) (↑0 : S) 1 ≤ s), HPow.hPow (β := ℕ) (s - (↑0 : S) + 1) 0 ≤ eval s (descPochhammer S 0)
⊢ (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)
have succ : ∀ (n : ℕ) (ih : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 ≤ s), (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n))
  (h : HSub.hSub (α := S) (↑(n + 1) : S) 1 ≤ s), (s - (↑(n + 1) : S) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h
    have hsub1 : n - 1 ≤ s := (sub_le_self (n : S) zero_le_one).trans (le_of_sub_nonneg h)
    rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]
    apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)
    exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
a : S
ha : a ∈ Set.Ici (HSub.hSub (α := S) (↑(n + 1) : S) 1)
b : S
hb : b ∈ Set.Ici (HSub.hSub (α := S) (↑(n + 1) : S) 1)
hab : a ≤ b
⊢ LE.le.{u_1} (α := S) ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) a)
    ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) b)
have succ : ∀ (ha : (↑n : S) ≤ a) ⦃b : S⦄ (hb : (↑n : S) ≤ b) (hab : a ≤ b),
  LE.le.{u_1} (α := S) ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) a)
    ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) b)
Tactic: rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
Cleared hypotheses: ha, b, hb, hab
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
a : S
ha : (↑n : S) ≤ a
b : S
hb : (↑n : S) ≤ b
hab : a ≤ b
⊢ LE.le.{u_1} (α := S) ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) a)
    ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) b)
have ha_sub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ a
Tactic: have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
a : S
ha : (↑n : S) ≤ a
b : S
hb : (↑n : S) ≤ b
hab : a ≤ b
ha_sub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ a
⊢ LE.le.{u_1} (α := S) ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) a)
    ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) b)
have hb_sub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ b
Tactic: have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
a : S
ha : (↑n : S) ≤ a
b : S
hb : (↑n : S) ≤ b
hab : a ≤ b
ha_sub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ a
hb_sub1 : HSub.hSub (α := S) (↑n : S) 1 ≤ b
⊢ LE.le.{u_1} (α := S) ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) a)
    ((fun (x : S) ↦ eval x (descPochhammer S (n + 1))) b)
have succ : eval a (descPochhammer S n) * (a - (↑n : S)) ≤ eval b (descPochhammer S n) * (b - (↑n : S))
Tactic: simp_rw [descPochhammer_succ_eval]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
⊢ MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))
have zero : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S 0)) (Set.Ici (HSub.hSub (α := S) (↑0 : S) 1))
Tactic: induction n with
  | zero => simp [monotoneOn_const]
  | succ n ih =>
    intro a ha b hb hab
    rw [Set.mem_Ici, Nat.cast_add_one, add_sub_cancel_right] at ha hb
    have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
    have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
    simp_rw [descPochhammer_succ_eval]
    exact mul_le_mul (ih ha_sub1 hb_sub1 hab) (sub_le_sub_right hab (n : S))
      (sub_nonneg_of_le ha) (descPochhammer_nonneg hb_sub1)
Cleared hypotheses: n