awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
have succ : ∀ (h : a ≤ b),
  Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
succ :
  ∀ (h : a ≤ b),
    Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
have succ₁ : ∀ (h : b ≤ a),
  Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : a ≤ b
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
have rw : a - b + b ≤ b
Tactic: rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : a ≤ b
⊢ a - b + b ≤ b
have rw : 0 + b ≤ b
Tactic: rw [tsub_eq_zero_iff_le.mpr h, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : a ≤ b
rw : 0 + b ≤ b
⊢ a - b + b ≤ b
have rw₁ : b ≤ b
Tactic: rw [tsub_eq_zero_iff_le.mpr h, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : b ≤ a
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
have succ : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑(a.descFactorial (b + 0).succ) : S)
Tactic: rw [tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
have zero : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial 0) : S) (↑((a - HSub.hSub (α := ℕ) 0 1 + 0 - 1).descFactorial 0) : S)
Tactic: induction b with
  | zero => simp
  | succ b =>
    simp_rw [add_succ, Nat.add_one_sub_one]
    obtain h | h := le_total a b
    · rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
      rw [tsub_eq_zero_iff_le.mpr h, zero_add]
    · rw [tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
zero : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial 0) : S) (↑((a - HSub.hSub (α := ℕ) 0 1 + 0 - 1).descFactorial 0) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
have succ : ∀ (b : ℕ),
  Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S) →
    Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 1)) : S)
      (↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1)) : S)
Tactic: induction b with
  | zero => simp
  | succ b =>
    simp_rw [add_succ, Nat.add_one_sub_one]
    obtain h | h := le_total a b
    · rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
      rw [tsub_eq_zero_iff_le.mpr h, zero_add]
    · rw [tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a : ℕ
⊢ (↑a ! : S) = eval 1 (ascPochhammer S a)
have rw : (↑(ascFactorial 1 a) : S) = eval 1 (ascPochhammer S a)
Tactic: rw [← one_ascFactorial, cast_ascFactorial, cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a : ℕ
rw : (↑(ascFactorial 1 a) : S) = eval 1 (ascPochhammer S a)
⊢ (↑a ! : S) = eval 1 (ascPochhammer S a)
have rw₁ : eval (↑1 : S) (ascPochhammer S a) = eval 1 (ascPochhammer S a)
Tactic: rw [← one_ascFactorial, cast_ascFactorial, cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u_1
inst : Semiring S
a : ℕ
rw : (↑(ascFactorial 1 a) : S) = eval 1 (ascPochhammer S a)
rw₁ : eval (↑1 : S) (ascPochhammer S a) = eval 1 (ascPochhammer S a)
⊢ (↑a ! : S) = eval 1 (ascPochhammer S a)
have rw₂ : eval 1 (ascPochhammer S a) = eval 1 (ascPochhammer S a)
Tactic: rw [← one_ascFactorial, cast_ascFactorial, cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ descPochhammer R (n + 1) = X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)
have rw : X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1) = X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)
Tactic: rw [descPochhammer]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
⊢ Monic (descPochhammer R (n + 1))
have h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
Tactic: have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
⊢ Monic (descPochhammer R (n + 1))
have this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
Tactic: have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
⊢ Monic (descPochhammer R (n + 1))
have succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
⊢ Monic (descPochhammer R (n + 1))
have succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₃ : leadingCoeff X *
    (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
  1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
⊢ Monic (descPochhammer R (n + 1))
have succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₆ : 1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₆ : 1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₇ : (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₆ : 1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
succ₇ : (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₈ : HPow.hPow (α := R) 1 (natDegree (descPochhammer R n)) = 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₆ : 1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
succ₇ : (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
succ₈ : HPow.hPow (α := R) 1 (natDegree (descPochhammer R n)) = 1
⊢ Monic (descPochhammer R (n + 1))
have succ₉ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
⊢ Monic (descPochhammer R n)
have zero : Monic (descPochhammer R 0)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
zero : Monic (descPochhammer R 0)
⊢ Monic (descPochhammer R n)
have succ : ∀ (n : ℕ) (hn : Monic (descPochhammer R n)), Monic (descPochhammer R (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
T : Type v
inst_1 : Ring T
f : R →+* T
n : ℕ
⊢ map f (descPochhammer R n) = descPochhammer T n
have zero : map f (descPochhammer R 0) = descPochhammer T 0
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, descPochhammer_succ_left, map_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
T : Type v
inst_1 : Ring T
f : R →+* T
n : ℕ
zero : map f (descPochhammer R 0) = descPochhammer T 0
⊢ map f (descPochhammer R n) = descPochhammer T n
have succ : ∀ (n : ℕ) (ih : map f (descPochhammer R n) = descPochhammer T n),
  map f (descPochhammer R (n + 1)) = descPochhammer T (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, descPochhammer_succ_left, map_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
k : ℤ
⊢ (↑(eval k (descPochhammer ℤ n)) : R) = eval (↑k : R) (descPochhammer R n)
have rw : (algebraMap ℤ R : (a : ℤ) → R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k : R) (descPochhammer ℤ n)
Tactic: rw [← descPochhammer_map (algebraMap ℤ R), eval_map, ← eq_intCast (algebraMap ℤ R)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0
have zero : eval 0 (descPochhammer R 0) = if Eq (α := ℕ) 0 0 then 1 else 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
zero : eval 0 (descPochhammer R 0) = if Eq (α := ℕ) 0 0 then 1 else 0
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0
have succ : ∀ (n : ℕ), eval 0 (descPochhammer R (n + 1)) = if n + 1 = 0 then 1 else 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
R : Type u
inst : Ring R
n : ℕ
h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer R (n + 1) = descPochhammer R n * HSub.hSub (α := R[X]) X (↑n : R[X])
have h₁ : Eq (α := R[X]) (map (algebraMap ℤ R) (descPochhammer ℤ (n + 1)))
  (map (algebraMap ℤ R) (descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])))
Tactic: apply_fun Polynomial.map (algebraMap ℤ R) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ descPochhammer R (n + 1) = descPochhammer R n * HSub.hSub (α := R[X]) X (↑n : R[X])
have suffices : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤ[X])) by
    apply_fun Polynomial.map (algebraMap ℤ R) at h
    simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
| descPochhammer ℤ (n + 1 + 1)
have rw : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X]))
Tactic: rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1 + 1) = descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
have succ : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
  descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
Tactic: conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
have succ : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
  descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) (↑1 : ℤ[X]))
Tactic: rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) (↑1 : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
have succ₁ : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
  descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1)
Tactic: rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) (↑1 : ℤ[X]))
succ₁ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1)
⊢ descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
have succ₂ : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X]))
Tactic: rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]