awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
refine_1 : ∀ (rn : ℕ) (hrn : rn < n) (rrn : (↑rn : R) = -r), ∃ k < n + 1, (↑k : R) = -r
⊢ ∃ k < n + 1, (↑k : R) = -r

Tactic:
obtain ⟨rn, hrn, rrn⟩ := ih h
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
rn : ℕ
hrn : rn < n
rrn : (↑rn : R) = -r
⊢ rn < n + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
rn : ℕ
hrn : rn < n
rrn : (↑rn : R) = -r
⊢ ∃ k < n + 1, (↑k : R) = -r

Tactic:
exact ⟨rn, by lia, rrn⟩
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 : r + (↑n : R) = 0
⊢ ∃ k < n + 1, (↑k : R) = -r

Tactic:
⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩

Premises used: lt_add_one, And.intro, Exists.intro, eq_neg_of_add_eq_zero_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 : r + (↑n : R) = 0
⊢ ∃ k < n + 1, (↑k : R) = -r

Tactic:
exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
refine_1₁ : ∀ (h : r + (↑n : R) = 0), ∃ k < n + 1, (↑k : R) = -r
⊢ ∃ 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⟩
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
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
⊢ ∃ k < n, (↑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⟩

Premises used: ascPochhammer_succ_eval, mul_eq_zero, ascPochhammer_zero, Polynomial.eval_one, one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
hrn : ∃ k < n, (↑k : R) = -r
refine_2 : ∀ (rn : ℕ) (hrn : rn < n) (rnn : (↑rn : R) = -r), eval r (ascPochhammer R n) = 0
⊢ eval r (ascPochhammer R n) = 0

Tactic:
obtain ⟨rn, hrn, rnn⟩ := hrn
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : (↑rn : R) = -r
⊢ eval (-(↑rn : R)) (ascPochhammer R n) = 0

Tactic:
ascPochhammer_eval_neg_coe_nat_of_lt hrn

Premises used: ascPochhammer_eval_neg_coe_nat_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : (↑rn : R) = -r
h : r = -(↑rn : R)
⊢ eval r (ascPochhammer R n) = 0

Tactic:
convert! ascPochhammer_eval_neg_coe_nat_of_lt hrn

Premises used: ascPochhammer_eval_neg_coe_nat_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : (↑rn : R) = -r
⊢ r = -(↑rn : R)

Tactic:
simp [rnn]
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
h : k < n
rw : eval (-(↑(n - k.succ) : R)) (ascPochhammer R n) = 0
⊢ eval (↑k : R) (descPochhammer R n) = 0

Tactic:
rw [descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub,
    ← Nat.cast_add_one, ← neg_sub, ← Nat.cast_sub h]

Premises used: neg_sub, Nat.cast_sub, descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub, Nat.cast_add_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
h : k < n
⊢ eval (-(↑(n - k.succ) : R)) (ascPochhammer R n) = 0

Tactic:
ascPochhammer_eval_neg_coe_nat_of_lt (Nat.sub_lt_of_pos_le k.succ_pos h)

Premises used: Nat.sub_lt_of_pos_le, ascPochhammer_eval_neg_coe_nat_of_lt, Nat.succ_pos
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
h : k < n
⊢ eval (-(↑(n - k.succ) : R)) (ascPochhammer R n) = 0

Tactic:
exact ascPochhammer_eval_neg_coe_nat_of_lt (Nat.sub_lt_of_pos_le k.succ_pos h)

Premises used: Nat.sub_lt_of_pos_le, ascPochhammer_eval_neg_coe_nat_of_lt, Nat.succ_pos
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - (↑j : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u_1
inst : CommRing R
r : R
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:
simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]

Premises used: descPochhammer_succ_right, Finset.prod_range_succ
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : R
zero : eval r (descPochhammer R 0) = ∏ j ∈ Finset.range 0, (r - (↑j : R))
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))
⊢ eval r (descPochhammer R n) = ∏ j ∈ Finset.range n, (r - (↑j : R))

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [descPochhammer_succ_right, ih, ← Finset.prod_range_succ]

Premises used: descPochhammer_succ_right, Finset.prod_range_succ
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 < s - (↑n : S) + 1

Tactic:
rw [← sub_pos, ← sub_add] at h

Premises used: sub_add, sub_pos
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
rw : 0 < eval (s - (↑n : S) + 1) (ascPochhammer S n)
⊢ 0 < eval s (descPochhammer S n)

Tactic:
rw [descPochhammer_eval_eq_ascPochhammer]

Premises used: descPochhammer_eval_eq_ascPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 - (↑n : S) + 1) (ascPochhammer S n)

Tactic:
ascPochhammer_pos n (s - n + 1) h

Premises used: HSub.hSub, Nat.cast, ascPochhammer_pos, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 - (↑n : S) + 1) (ascPochhammer S n)

Tactic:
exact ascPochhammer_pos n (s - n + 1) h

Premises used: HSub.hSub, Nat.cast, ascPochhammer_pos, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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)
inr : ∀ (h : HSub.hSub (α := S) (↑n : S) 1 < s), 0 ≤ eval s (descPochhammer S n)
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
rcases eq_or_lt_of_le h with heq | h

Premises used: eq_or_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
inl : LE.le.{u_1} (α := S) 0 (if n = 0 then 1 else 0)
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
rw [← heq, descPochhammer_eval_eq_ascPochhammer,
      sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]

Premises used: ascPochhammer_eval_zero, sub_sub_cancel_left, neg_add_cancel, descPochhammer_eval_eq_ascPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ LE.le.{u_1} (α := S) 0 (if n = 0 then 1 else 0)

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h_1 : HSub.hSub (α := S) (↑n : S) 1 ≤ s
h : HSub.hSub (α := S) (↑n : S) 1 < s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
(descPochhammer_pos h).le

Premises used: LT.lt.le, descPochhammer_pos
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h_1 : HSub.hSub (α := S) (↑n : S) 1 ≤ s
h : HSub.hSub (α := S) (↑n : S) 1 < s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
exact (descPochhammer_pos h).le

Premises used: LT.lt.le, descPochhammer_pos
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : HSub.hSub (α := S) (↑0 : S) 1 ≤ s
⊢ HPow.hPow (β := ℕ) (s - (↑0 : S) + 1) 0 ≤ eval s (descPochhammer S 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ 0 ≤ s - (↑n : S)

Tactic:
rw [Nat.cast_add_one, add_sub_cancel_right, ← sub_nonneg] at h

Premises used: add_sub_cancel_right, Nat.cast_add_one, sub_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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)
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
succ : (s - (↑n : S)) ^ n * (s - (↑n : S)) ≤ eval s (descPochhammer S n) * (s - (↑n : S))
⊢ (s - (↑(n + 1) : S) + 1) ^ (n + 1) ≤ eval s (descPochhammer S (n + 1))

Tactic:
rw [pow_succ, descPochhammer_succ_eval, Nat.cast_add_one, sub_add, add_sub_cancel_right]

Premises used: sub_add, pow_succ, descPochhammer_succ_eval, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
apply : (s - (↑n : S)) ^ n ≤ eval s (descPochhammer S n)
⊢ (s - (↑n : S)) ^ n * (s - (↑n : S)) ≤ eval s (descPochhammer S n) * (s - (↑n : S))

Tactic:
apply mul_le_mul _ le_rfl h (descPochhammer_nonneg hsub1)

Premises used: le_rfl, descPochhammer_nonneg, mul_le_mul
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 ≤ eval s (descPochhammer S n)

Tactic:
(ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n

Premises used: pow_le_pow_left₀, zero_le_one, le_add_of_nonneg_right, LE.le.trans'
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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 ≤ eval s (descPochhammer S n)

Tactic:
exact (ih hsub1).trans' <| pow_le_pow_left₀ h (le_add_of_nonneg_right zero_le_one) n

Premises used: pow_le_pow_left₀, zero_le_one, le_add_of_nonneg_right, LE.le.trans'
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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)
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))
⊢ (s - (↑n : S) + 1) ^ n ≤ eval s (descPochhammer S n)

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

Premises used: sub_add, pow_succ, pow_le_pow_left₀, zero_le_one, le_add_of_nonneg_right, descPochhammer_succ_eval, add_sub_cancel_right, Nat.cast_add_one, sub_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
⊢ MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S 0)) (Set.Ici (HSub.hSub (α := S) (↑0 : S) 1))

Tactic:
simp [monotoneOn_const]

Premises used: monotoneOn_const
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
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)
⊢ 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

Premises used: Set.mem_Ici, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ HSub.hSub (α := S) (↑n : S) 1 ≤ a

Tactic:
have ha_sub1 : n - 1 ≤ a := (sub_le_self (n : S) zero_le_one).trans ha
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ HSub.hSub (α := S) (↑n : S) 1 ≤ b

Tactic:
have hb_sub1 : n - 1 ≤ b := (sub_le_self (n : S) zero_le_one).trans hb
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
succ : eval a (descPochhammer S n) * (a - (↑n : S)) ≤ eval b (descPochhammer S n) * (b - (↑n : S))
⊢ 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:
simp_rw [descPochhammer_succ_eval]

Premises used: descPochhammer_succ_eval
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ eval a (descPochhammer S n) * (a - (↑n : S)) ≤ eval b (descPochhammer S n) * (b - (↑n : S))

Tactic:
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)

Premises used: sub_le_sub_right, sub_nonneg_of_le, descPochhammer_nonneg, Nat.cast, mul_le_mul
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
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
⊢ eval a (descPochhammer S n) * (a - (↑n : S)) ≤ eval b (descPochhammer S n) * (b - (↑n : S))

Tactic:
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)

Premises used: sub_le_sub_right, sub_nonneg_of_le, descPochhammer_nonneg, Nat.cast, mul_le_mul
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
zero : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S 0)) (Set.Ici (HSub.hSub (α := S) (↑0 : S) 1))
succ :
  ∀ (n : ℕ)
    (ih : MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : S) 1))),
    MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S (n + 1)))
      (Set.Ici (HSub.hSub (α := S) (↑(n + 1) : S) 1))
⊢ MonotoneOn (β := S) (fun (x : S) ↦ eval x (descPochhammer S n)) (Set.Ici (HSub.hSub (α := S) (↑n : 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)

Premises used: monotoneOn_const, Set.mem_Ici, descPochhammer_succ_eval, add_sub_cancel_right, Nat.cast_add_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₃ : (↑(a.descFactorial b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b)
rw₄ rw₅ : Eq.{u_1 + 1} (α := K) (↑(a.descFactorial b) : K) (↑(a.descFactorial b) : K)
⊢ (↑(a.choose b) : K) = eval (↑(a - (b - 1)) : K) (ascPochhammer K b) / (↑b ! : K)

Tactic:
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]

Premises used: Iff.mpr, Nat.factorial_ne_zero, Nat.cast_mul, eq_div_iff_mul_eq, mul_comm, Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_ne_zero, Nat.cast_descFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : CharZero K
a b : ℕ
rw : HMul.hMul (α := K) (↑(a.choose b) : K) (↑b ! : K) = eval (↑a : K) (descPochhammer K b)
rw₁ : (↑(a.choose b * b !) : K) = eval (↑a : K) (descPochhammer K b)
rw₂ : (↑(b ! * a.choose b) : K) = eval (↑a : K) (descPochhammer K b)
rw₃ : (↑(a.descFactorial b) : K) = eval (↑a : K) (descPochhammer K b)
rw₄ rw₅ : Eq.{u_1 + 1} (α := K) (↑(a.descFactorial b) : K) (↑(a.descFactorial b) : K)
⊢ (↑(a.choose b) : K) = eval (↑a : K) (descPochhammer K b) / (↑b ! : K)

Tactic:
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
    mul_comm, ← descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]

Premises used: Iff.mpr, descPochhammer_eval_eq_descFactorial, Nat.factorial_ne_zero, Nat.cast_mul, eq_div_iff_mul_eq, mul_comm, Nat.descFactorial_eq_factorial_mul_choose, Nat.cast_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x_1 x : R
⊢ (aeval x_1 : (a : R[X]) → R) ((fun (a : R) ↦ ((C : (a : R) → R[X]) a : R[X])) x) = x

Tactic:
eval_C

Premises used: Polynomial.eval, Polynomial.eval_C, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x_1 x : R
⊢ (aeval x_1 : (a : R[X]) → R) ((fun (a : R) ↦ ((C : (a : R) → R[X]) a : R[X])) x) = x

Tactic:
exact eval_C

Premises used: Polynomial.eval_C
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x : R
p : R[X]
⊢ (quotientSpanXSubCAlgEquiv x : (a : R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) x}) → R)
      ((Ideal.Quotient.mk (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])}) :
            (a : R[X]) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) x})
          p :
        HasQuotient.Quotient R[X] (B := Ideal R[X])
          (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])})) =
    eval x p

Tactic:
rfl

Premises used: Polynomial.eval, Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Polynomial.Quotient
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Eq (α :=
    HasQuotient.Quotient R[X] (B := Ideal R[X])
      (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])}))
    ((AlgEquiv.symm (quotientSpanXSubCAlgEquiv x) : (a : R) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) x}) y :
      HasQuotient.Quotient R[X] (B := Ideal R[X])
        (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])}))
    ((algebraMap R
            (HasQuotient.Quotient R[X] (B := Ideal R[X])
              (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])})) :
          (a : R) → R[X] ⧸ Ideal.span {X - (C : (a : R) → R[X]) x})
        y :
      HasQuotient.Quotient R[X] (B := Ideal R[X])
        (Ideal.span {HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])}))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl