awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
k : ℕ
rw :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial univ fun (_i : Fin k) ↦ n) : DividedPowerAlgebra R M)
      (dp R (∑ _i : Fin k, n) m) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial (range k) fun (x : ℕ) ↦ n) : DividedPowerAlgebra R M)
      (dp R (k * n) m)
⊢ HPow.hPow (α := DividedPowerAlgebra R M) (dp R n m) k =
    HMul.hMul (α := DividedPowerAlgebra R M)
      (↑(HSMul.hSMul (β := Multiset ℕ) k {n}).multinomial : DividedPowerAlgebra R M) (dp R (k * n) m)

Tactic:
rw [Multiset.multinomial_nsmul_singleton, ← Fin.prod_const, prod_dp]

Premises used: Fin.prod_const, Multiset.multinomial_nsmul_singleton, DividedPowerAlgebra.prod_dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
k : ℕ
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial univ fun (_i : Fin k) ↦ n) : DividedPowerAlgebra R M)
      (dp R (∑ _i : Fin k, n) m) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial (range k) fun (x : ℕ) ↦ n) : DividedPowerAlgebra R M)
      (dp R (k * n) m)

Tactic:
simp [Nat.multinomial]

Premises used: Nat.multinomial
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
rfl_zero :
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
zero :
  ∀ {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)
smul :
  ∀ {r : R} {n : ℕ} {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, r • a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, a))) :
        A)
mul :
  ∀ {m n : ℕ} {a : M},
    Eq.{u_3 + 1} (α := A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (m, a)) (X (n, a))) :
        A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((m + n).choose m) (X (m + n, a))) :
        A)
add :
  ∀ {n : ℕ} {a b : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, a + b)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
            HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, a)) (X (k.2, b))) :
        A)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)

Tactic:
rcases h
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
a : M
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
r : R
n : ℕ
a : M
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, r • a)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, a))) :
      A)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ Eq.{u_3 + 1} (α := A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (m, a)) (X (n, a))) :
      A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((m + n).choose m) (X (m + n, a))) :
      A)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, a + b)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, a)) (X (k.2, b))) :
      A)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
⊢ ∀ ⦃x y : MvPolynomial.{u_2, u_1} (ℕ × M) R⦄,
    Rel R M x y →
      Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) x : A)
        ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) y : A)

Tactic:
lift'_imp R M hf_zero hf_smul hf_mul hf_add

Premises used: _private.0.DividedPowerAlgebra.lift'_imp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
⊢ ∀ ⦃x y : MvPolynomial.{u_2, u_1} (ℕ × M) R⦄,
    Rel R M x y →
      Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) x : A)
        ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) y : A)

Tactic:
exact lift'_imp R M hf_zero hf_smul hf_mul hf_add

Premises used: _private.0.DividedPowerAlgebra.lift'_imp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
⊢ Eq.{u_3 + 1} (α := A)
    ((lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval f : (a : MvPolynomial (ℕ × M) R) → A) p : A)

Tactic:
simp [lift', aeval_eq_eval₂Hom]

Premises used: DividedPowerAlgebra.lift', MvPolynomial.aeval_eq_eval₂Hom
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
rw :
  (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) =
    f (n, m)
rw₁ : (aeval f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, m)) = f (n, m)
rw₂ rw₃ : f (n, m) = f (n, m)
⊢ (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A) (dp R n m) = f (n, m)

Tactic:
rw [dp_def, lift'_apply hf_zero hf_smul hf_mul hf_add, aeval_X]

Premises used: MvPolynomial.aeval_X, DividedPowerAlgebra.lift'_apply, DividedPowerAlgebra.dp_def
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
r : R
m : M
dsimp : hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
⊢ (fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, r • m) =
    HSMul.hSMul (β := A) (r ^ n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, m))

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
r : R
m : M
rw :
  hI.dpow n (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) r : R) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₁ : hI.dpow n (HSMul.hSMul (β := A) r ((g : (a : M) → A) m : A)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₂ :
  hI.dpow n (HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₃ :
  hI.dpow n (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₄ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n * hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₅ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n • hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₆ :
  HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) (r ^ n) : A) (hI.dpow n ((g : (a : M) → A) m)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₇ rw₈ : r ^ n • hI.dpow n ((g : (a : M) → A) m) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)

Tactic:
rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]

Premises used: RingHom.id_apply, algebraMap_smul, map_pow, DividedPowers.dpow_mul, LinearMap.map_smulₛₗ, smul_eq_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n p : ℕ
m : M
rw :
  (↑(((n, m).1 + (p, m).1).choose (n, m).1) : A) * hI.dpow ((n, m).1 + (p, m).1) ((g : (a : M) → A) m) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
rw₁ rw₂ :
  ((n, m).1 + (p, m).1).choose (n, m).1 • hI.dpow ((n, m).1 + (p, m).1) ((g : (a : M) → A) m) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
⊢ HMul.hMul (α := A) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, m))
      ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (p, m)) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))

Tactic:
rw [hI.mul_dpow (hg m), ← nsmul_eq_mul]

Premises used: DividedPowers.mul_dpow, nsmul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
u v : M
⊢ Eq.{u_3 + 1} (α := A) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, u + v))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      match (motive := ℕ × ℕ → A) x with
      | (k, l) =>
        HMul.hMul (α := A) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (k, u))
          ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (l, v)))

Tactic:
simp [hI.dpow_add (hg u) (hg v)]

Premises used: DividedPowers.dpow_add
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
rw :
  Eq.{u_3 + 1} (α := A)
    ((lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) ⋯ ⋯ ⋯ ⋯ : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)

Tactic:
rw [lift, lift'_apply]

Premises used: DividedPowerAlgebra.lift'_apply, DividedPowerAlgebra.lift
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
m : M
rw :
  (lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) ⋯ ⋯ ⋯ ⋯ : (a : DividedPowerAlgebra R M) → A)
      (dp R n m) =
    hI.dpow n ((g : (a : M) → A) m)
rw₁ rw₂ : hI.dpow (n, m).1 ((g : (a : M) → A) (n, m).2) = hI.dpow n ((g : (a : M) → A) m)
⊢ (lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)

Tactic:
rw [lift, lift'_apply_dp]

Premises used: DividedPowerAlgebra.lift'_apply_dp, DividedPowerAlgebra.lift
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), (f : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)
x : ℕ
x_1 : M
rw : (f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) = hI.dpow x ((g : (a : M) → A) x_1)
rw₁ rw₂ : hI.dpow x ((g : (a : M) → A) x_1) = hI.dpow x ((g : (a : M) → A) x_1)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)

Tactic:
rw [lift_apply_dp, hf]

Premises used: DividedPowerAlgebra.lift_apply_dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
m : M
⊢ Eq.{u_3 + 1} (α := A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A)
        ((embed R M : (a : M) → DividedPowerAlgebra R M) m : DividedPowerAlgebra R M) :
      A)
    ((g : (a : M) → A) m : A)

Tactic:
simp [embed_def, hI.dpow_one (hg m)]

Premises used: DividedPowers.dpow_one, DividedPowerAlgebra.embed_def
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := A) (((lift hI g hg).toLinearMap ∘ₗ embed R M : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
⊢ (lift hI g hg).toLinearMap ∘ₗ embed R M = g

Tactic:
ext
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
x : M
⊢ Eq.{u_3 + 1} (α := A) (((lift hI g hg).toLinearMap ∘ₗ embed R M : (a : M) → A) x : A) ((g : (a : M) → A) x : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
a : M
⊢ Eq (α := DividedPowerAlgebra S N) (dp S 0 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
    (1 : DividedPowerAlgebra S N)

Tactic:
DividedPowerAlgebra.dp_zero

Premises used: DividedPowerAlgebra.dp_zero
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
m n : ℕ
a : M
⊢ HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
      (dp S m ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) ((m + n).choose m)
      (dp S (m + n) ((f : (a : M) → N) a) : DividedPowerAlgebra S N)

Tactic:
DividedPowerAlgebra.dp_mul

Premises used: DividedPowerAlgebra.dp_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
n : ℕ
a b : M
rw :
  Eq (α := DividedPowerAlgebra S N)
    (dp S n (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)))
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
        (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
        (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
rw₁ rw₂ :
  Eq (α := DividedPowerAlgebra S N)
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
        (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
        (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
        (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
        (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
⊢ Eq (α := DividedPowerAlgebra S N) (dp S n ((f : (a : M) → N) (a + b)) : DividedPowerAlgebra S N)
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
          (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
          (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N) :
      DividedPowerAlgebra S N)

Tactic:
rw [map_add, DividedPowerAlgebra.dp_add]

Premises used: map_add, DividedPowerAlgebra.dp_add