awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : A
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) a ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) 1)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) a) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
have ha : Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
          (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
        ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
          (comul : (a : B) → B ⊗[R] B) 1)) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
          TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R] ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: rw [← (ℛ R a).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : B
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                  (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                    A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                  (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
                A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
have hb : Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
          (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
        ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) a)) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
          TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((comul : (a : B) → B ⊗[R] B) a ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) 1) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : B
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) a)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) a ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) 1) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
have hb : Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
          (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
        ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R]
          ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
          TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
        (comul : (a : A) → A ⊗[R] A) 1) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: rw [← (ℛ R a).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
⊢ Eq (α := A →ₐc[R] A ⊗[R] A) (BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A))
    (comulBialgHom R A)
have H : ∀ (x : A),
  Eq (α := A ⊗[R] A)
    ((BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A) : (a : A) → A ⊗[R] A) x :
      A ⊗[R] A)
    ((comulBialgHom R A : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (A ⊗[R] A) R) (counit ∘ₗ LinearMap.mul' R A) counit
have a : ∀ (x x_1 : A),
  Eq.{u_1 + 1} (α := R)
    (((((TensorProduct.AlgebraTensorModule.curry (counit ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] R) :
                (a : A) → A →ₗ[R] R)
              x :
            A →ₗ[R] R) :
          (a : A) → R)
        x_1 :
      R)
    (((((TensorProduct.AlgebraTensorModule.curry counit : A →ₗ[R] A →ₗ[R] R) : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) :
          (a : A) → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := A ⊗[R] A →ₗ[R] A ⊗[R] A) (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul)
    (comul ∘ₗ LinearMap.mul' R A)
have a : ∀ (a b : A),
  Eq (α := A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul) :
                  A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry (comul ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
⊢ Eq (α := A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul) :
                  A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry (comul ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)
have a₁ : ∑ x ∈ Repr.index (ℛ R a),
    (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) : (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
      (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
            A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
          (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
        (Repr.left (ℛ R a) x ⊗ₜ[R] Repr.right (ℛ R a) x ⊗ₜ[R]
          ∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)) =
  HMul.hMul (α := A ⊗[R] A) (∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)
    (∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)
Tactic: simp [← (ℛ R a).eq, ← (ℛ R b).eq, TensorProduct.sum_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0
have rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0
have rw₁ : smeval (ascPochhammer ℕ 0) r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₁ : smeval (ascPochhammer ℕ 0) r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0
have rw₂ : smeval (R := ℕ) 1 r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₁ : smeval (ascPochhammer ℕ 0) r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₂ : smeval (R := ℕ) 1 r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0
have rw₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₁ : smeval (ascPochhammer ℕ 0) r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₂ : smeval (R := ℕ) 1 r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0
have rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
⊢ multichoose r 0 = 1
have rw : HPow.hPow (β := ℕ) r 0 = 1
Tactic: rw [multichoose_zero_right', npow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
rw : HPow.hPow (β := ℕ) r 0 = 1
⊢ multichoose r 0 = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [multichoose_zero_right', npow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw₂ : smeval (R := ℕ) X r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₂ : smeval (R := ℕ) X r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw₃ : HPow.hPow (β := ℕ) r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₂ : smeval (R := ℕ) X r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₃ : HPow.hPow (β := ℕ) r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw₄ : HPow.hPow (β := ℕ) r 1 = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 1)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₂ : smeval (R := ℕ) X r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₃ : HPow.hPow (β := ℕ) r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₄ : HPow.hPow (β := ℕ) r 1 = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 1)
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1
have rw₅ : HPow.hPow (β := ℕ) r 1 = HPow.hPow (β := ℕ) r 1
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
⊢ multichoose r 1 = r
have rw : HPow.hPow (β := ℕ) r 1 = r
Tactic: rw [multichoose_one_right', npow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
rw : HPow.hPow (β := ℕ) r 1 = r
⊢ multichoose r 1 = r
have rw₁ : r = r
Tactic: rw [multichoose_one_right', npow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw₂ : Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ (k + 1)) 0) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₂ : Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ (k + 1)) 0) 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw₃ : Eq.{u_2 + 1} (α := R) ((X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₂ : Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ (k + 1)) 0) 0
rw₃ : Eq.{u_2 + 1} (α := R) ((X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw₄ : HMul.hMul (α := R) 0 ((Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) = 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₂ : Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ (k + 1)) 0) 0
rw₃ : Eq.{u_2 + 1} (α := R) ((X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) 0
rw₄ : HMul.hMul (α := R) 0 ((Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) = 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0
have rw₅ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]