awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₇ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
    HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₇ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₈ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  comp (ascPochhammer ℤ n) ((HAdd.hAdd (α := ℤ[X]) X 1).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
    HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₇ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₈ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) ((HAdd.hAdd (α := ℤ[X]) X 1).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₉ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  comp (ascPochhammer ℤ n)
      (comp X (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
    HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₇ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₈ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) ((HAdd.hAdd (α := ℤ[X]) X 1).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₉ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n)
        (comp X (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₁₀ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
    HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₇ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₈ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) ((HAdd.hAdd (α := ℤ[X]) X 1).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₉ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n)
        (comp X (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₁₀ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
have succ₁₁ : comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
⊢ descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
have zero : descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
Tactic: induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
n : ℕ
zero : descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
⊢ descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
have succ : ∀ (n : ℕ) (ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)),
  descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
Tactic: induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
⊢ eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
have zero : eval r 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
Tactic: rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
zero : eval r 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
⊢ eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
have zero₁ : 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
Tactic: rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
zero : eval r 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
zero₁ : 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
⊢ eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
have zero₂ : 1 = eval (r - (↑0 : R) + 1) 1
Tactic: rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
zero : eval r 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
zero₁ : 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
zero₂ : 1 = eval (r - (↑0 : R) + 1) 1
⊢ eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
have zero₃ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₅ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₆ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
have succ₇ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
  eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]