awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : IsLeftCancelMulZero.{u_1} R[X]ᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₁ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₂ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₃ : IsRightCancelMulZero R ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
⊢ IsRightCancelMulZero.{u_1} R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
have rw₄ : IsRightCancelMulZero R ∧ IsCancelAdd R ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Tactic: rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ IsCancelMulZero.{u_1} R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R
have simp_rw : (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
Tactic: simp_rw [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
have rw : (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R ∧ IsCancelAdd R ↔
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
Tactic: rw [and_and_and_comm, and_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
rw :
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
⊢ (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
have rw₁ : (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R ↔
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
Tactic: rw [and_and_and_comm, and_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ IsDomain.{u_1} R[X] ↔ IsDomain R ∧ IsCancelAdd R
have simp_rw : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial.{u_1} R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
Tactic: simp_rw [isDomain_iff_cancelMulZero_and_nontrivial, nontrivial_iff,
    Polynomial.isCancelMulZero_iff, and_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
simp_rw : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial.{u_1} R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
⊢ IsDomain.{u_1} R[X] ↔ IsDomain R ∧ IsCancelAdd R
have simp_rw₁ : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
Tactic: simp_rw [isDomain_iff_cancelMulZero_and_nontrivial, nontrivial_iff,
    Polynomial.isCancelMulZero_iff, and_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
simp_rw : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial.{u_1} R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
simp_rw₁ : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
⊢ IsDomain.{u_1} R[X] ↔ IsDomain R ∧ IsCancelAdd R
have simp_rw₂ : (IsCancelMulZero R ∧ IsCancelAdd R) ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
Tactic: simp_rw [isDomain_iff_cancelMulZero_and_nontrivial, nontrivial_iff,
    Polynomial.isCancelMulZero_iff, and_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ ascPochhammer S (n + 1) = X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)
have rw : X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1) = X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)
Tactic: rw [ascPochhammer]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (hypothesis)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
⊢ Monic (ascPochhammer S (n + 1))
have this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
Tactic: have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
⊢ Monic (ascPochhammer S (n + 1))
have succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₃ : leadingCoeff X *
    (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
  1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
⊢ Monic (ascPochhammer S (n + 1))
have succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₆ : 1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₆ : 1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₇ : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₆ : 1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
succ₇ : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₈ : HPow.hPow (α := S) 1 (natDegree (ascPochhammer S n)) = 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₆ : 1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
succ₇ : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
succ₈ : HPow.hPow (α := S) 1 (natDegree (ascPochhammer S n)) = 1
⊢ Monic (ascPochhammer S (n + 1))
have succ₉ : Eq.{u + 1} (α := S) 1 1
Tactic: rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
⊢ Monic (ascPochhammer S n)
have zero : Monic (ascPochhammer S 0)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
zero : Monic (ascPochhammer S 0)
⊢ Monic (ascPochhammer S n)
have succ : ∀ (n : ℕ) (hn : Monic (ascPochhammer S n)), Monic (ascPochhammer S (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
⊢ map f (ascPochhammer S n) = ascPochhammer T n
have zero : map f (ascPochhammer S 0) = ascPochhammer T 0
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, ascPochhammer_succ_left, map_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
zero : map f (ascPochhammer S 0) = ascPochhammer T 0
⊢ map f (ascPochhammer S n) = ascPochhammer T n
have succ : ∀ (n : ℕ) (ih : map f (ascPochhammer S n) = ascPochhammer T n),
  map f (ascPochhammer S (n + 1)) = ascPochhammer T (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, ascPochhammer_succ_left, map_comp]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)
have rw : eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)
Tactic: rw [← ascPochhammer_map f]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
have rw : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
  eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
Tactic: rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
rw :
  eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
have rw₁ : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
Tactic: rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
rw :
  eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
rw₁ : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
have rw₂ : eval x (comp (map (algebraMap R S) (ascPochhammer R n)) (map (algebraMap R S) p)) =
  eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
Tactic: rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
rw :
  eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
rw₁ : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₂ :
  eval x (comp (map (algebraMap R S) (ascPochhammer R n)) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
have rw₃ : eval x (map (algebraMap R S) (comp (ascPochhammer R n) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
Tactic: rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
rw :
  eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
rw₁ : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₂ :
  eval x (comp (map (algebraMap R S) (ascPochhammer R n)) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₃ : eval x (map (algebraMap R S) (comp (ascPochhammer R n) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)
have rw₄ : eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
Tactic: rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n k : ℕ
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)
have rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
Tactic: rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n k : ℕ
rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)
have rw₁ : (↑(eval k (ascPochhammer ℕ n)) : S) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
Tactic: rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n k : ℕ
rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
rw₁ : (↑(eval k (ascPochhammer ℕ n)) : S) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)
have rw₂ : (algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
Tactic: rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Pochhammer (goal)
Goal:
S : Type u
inst : Semiring S
n k : ℕ
rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
rw₁ : (↑(eval k (ascPochhammer ℕ n)) : S) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
rw₂ : (algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)
have rw₃ : Eq (α := S) ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
  ((algebraMap ℕ S : (a : ℕ) → S) (eval (↑k : ℕ) (ascPochhammer ℕ n)) : S)
Tactic: rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]