awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((MvPolynomial.C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial.{u_2, u_1} (ℕ × M) R
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F = f
C :
  ∀ (a : R) (f : DividedPowerAlgebra R M)
    (hf :
      (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
          ((MvPolynomial.C : (a : R) → MvPolynomial (ℕ × M) R) a) =
        f),
    P
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((MvPolynomial.C : (a : R) → MvPolynomial (ℕ × M) R) a))
add :
  ∀ (g1 g2 : MvPolynomial.{u_2, u_1} (ℕ × M) R)
    (hg1 :
      ∀ (f : DividedPowerAlgebra R M)
        (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 = f),
        P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1))
    (hg2 :
      ∀ (f : DividedPowerAlgebra R M)
        (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 = f),
        P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2))
    (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2) = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2))
mul_X :
  ∀ (g : MvPolynomial.{u_2, u_1} (ℕ × M) R) (nm : ℕ × M)
    (h :
      ∀ (f : DividedPowerAlgebra R M)
        (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
        P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g))
    (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)

Tactic:
induction F using MvPolynomial.induction_on generalizing f with
  | C a =>
      convert! h_C a using 1
      rw [mkAlgHom, AlgHom.coe_mk]
  | add g1 g2 hg1 hg2 =>
      rw [map_add]
      exact h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)
  | mul_X g nm h =>
      have h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2 := by
        simp only [dp_def, Prod.mk.eta, mkAlgHom, AlgHom.coe_mk]
      rw [_root_.map_mul, h']
      exact h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)

Premises used: AlgHom.coe_mk, map_add, MvPolynomial.induction_on, RingQuot.mkAlgHom, map_mul, MvPolynomial.C
-- 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
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
C : ∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)
add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * DividedPowerAlgebra.dp R n m)
a : R
rw : P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)
⊢ P
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((MvPolynomial.C : (a : R) → MvPolynomial (ℕ × M) R) a))

Tactic:
rw [mkAlgHom_C]

Premises used: DividedPowerAlgebra.mkAlgHom_C
-- 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
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
C : ∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)
add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * DividedPowerAlgebra.dp R n m)
a : R
⊢ P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)

Tactic:
C a
-- 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
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
C : ∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)
add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * DividedPowerAlgebra.dp R n m)
a : R
⊢ P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)

Tactic:
exact C a
-- 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
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n m)
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)))

Tactic:
simp [dp, mkRingHom, mkAlgHom]

Premises used: RingQuot.mkAlgHom, RingQuot.mkRingHom, DividedPowerAlgebra.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
m : M
rw :
  Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (0, m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) 1 :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
⊢ Eq (α := DividedPowerAlgebra R M) (dp R 0 m) 1

Tactic:
rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkAlgHom, map_one, 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
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (0, m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) 1 :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))

Tactic:
RingQuot.mkAlgHom_rel R Rel.zero

Premises used: RingQuot.mkAlgHom_rel, DividedPowerAlgebra.Rel.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
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (0, m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) 1 :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))

Tactic:
exact RingQuot.mkAlgHom_rel R Rel.zero

Premises used: RingQuot.mkAlgHom_rel, DividedPowerAlgebra.Rel.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
r : R
n : ℕ
m : M
rw :
  Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, r • m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, m))) :
      DividedPowerAlgebra R M)
⊢ dp R n (r • m) = HSMul.hSMul (β := DividedPowerAlgebra R M) (r ^ n) (dp R n m)

Tactic:
rw [dp_def, dp_def, ← map_smul]

Premises used: DividedPowerAlgebra.dp_def, map_smul
-- 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
r : R
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, r • m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, m))) :
      DividedPowerAlgebra R M)

Tactic:
mkAlgHom_rel R Rel.smul

Premises used: DividedPowerAlgebra.Rel.smul, RingQuot.mkAlgHom_rel
-- 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
r : R
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, r • m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, m))) :
      DividedPowerAlgebra R M)

Tactic:
exact mkAlgHom_rel R Rel.smul

Premises used: DividedPowerAlgebra.Rel.smul, RingQuot.mkAlgHom_rel
-- 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
n : ℕ
hn : n = 0
inl : Eq (α := DividedPowerAlgebra R M) (dp R n 0) 1
inl₁ : Eq (α := DividedPowerAlgebra R M) (dp R 0 0) 1
inl₂ inl₃ : Eq (α := DividedPowerAlgebra R M) 1 1
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)

Tactic:
rw [if_pos hn, hn, dp_zero]

Premises used: if_pos, 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
n : ℕ
hn : n > 0
inr : HSMul.hSMul (β := DividedPowerAlgebra R M) (HPow.hPow (α := R) 0 n) (dp R n 0) = 0
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)

Tactic:
rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]

Premises used: ne_of_gt, zero_smul, DividedPowerAlgebra.dp_smul, OfNat.ofNat, if_neg
-- 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
n : ℕ
hn : n > 0
inr : HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) 0 (dp R n 0) = 0
inr₁ inr₂ : Eq (α := DividedPowerAlgebra R M) 0 0
⊢ HSMul.hSMul (β := DividedPowerAlgebra R M) (HPow.hPow (α := R) 0 n) (dp R n 0) = 0

Tactic:
rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]

Premises used: Nat.pos_iff_ne_zero, zero_smul, Iff.mp, zero_pow
-- 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
n : ℕ
⊢ n = 0 ∨ n > 0

Tactic:
cases Nat.eq_zero_or_pos n with
  | inl hn =>
    rw [if_pos hn, hn, dp_zero]
  | inr hn =>
    rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]
    rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]

Premises used: DividedPowerAlgebra.dp_zero, zero_smul, DividedPowerAlgebra.dp_smul, OfNat.ofNat, Nat.eq_zero_or_pos
-- 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
n : ℕ
hn : n ≠ 0
rw : Eq (α := DividedPowerAlgebra R M) (if n = 0 then 1 else 0) 0
rw₁ rw₂ : Eq (α := DividedPowerAlgebra R M) 0 0
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) 0

Tactic:
rw [dp_null, if_neg hn]

Premises used: if_neg, DividedPowerAlgebra.dp_null
-- 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
n p : ℕ
m : M
simp :
  Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (n, m)) (X (p, m))) :
      DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((n + p).choose n) (X (n + p, m))) :
      DividedPowerAlgebra R M)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (dp R n m) (dp R p m) =
    HSMul.hSMul (β := DividedPowerAlgebra R M) ((n + p).choose n) (dp R (n + p) m)

Tactic:
simp only [dp_def, ← _root_.map_mul, ← map_nsmul]

Premises used: map_mul, DividedPowerAlgebra.dp_def, map_nsmul
-- 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
n p : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (n, m)) (X (p, m))) :
      DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((n + p).choose n) (X (n + p, m))) :
      DividedPowerAlgebra R M)

Tactic:
mkAlgHom_rel R Rel.mul

Premises used: DividedPowerAlgebra.Rel.mul, RingQuot.mkAlgHom_rel
-- 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
n p : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (n, m)) (X (p, m))) :
      DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra R M)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((n + p).choose n) (X (n + p, m))) :
      DividedPowerAlgebra R M)

Tactic:
exact mkAlgHom_rel R Rel.mul

Premises used: DividedPowerAlgebra.Rel.mul, RingQuot.mkAlgHom_rel
-- 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
n : ℕ
x y : M
k : ℕ × ℕ
h : k ∈ @antidiagonal _ Nat.instAddMonoid _ n
rw rw₁ :
  HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.1, x)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.2, y)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) =
    HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.1, x)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.2, y)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
⊢ (mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, x)) (X (k.2, y))) =
    HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.1, x)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (k.2, y)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))

Tactic:
rw [_root_.map_mul]

Premises used: map_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
ι : Type u_3
inst_3 : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ Eq (α := DividedPowerAlgebra R M) (dp R q (s.sum x))
    (∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i (↑k : Multiset ι)) (x i))

Tactic:
DividedPowers.dpow_sum' (I := ⊤) _ (fun _ ↦ dp_zero)
    (fun _ _ ↦ dp_add) dp_null_of_ne_zero (fun _ _ ↦ trivial)

Premises used: trivial, DividedPowers.dpow_sum', DividedPowerAlgebra.dp_zero, DividedPowerAlgebra.dp_add, DividedPowerAlgebra.dp_null_of_ne_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
ι : Type u_3
inst_3 : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
simp_rw :
  Eq (α := DividedPowerAlgebra R M) (∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i (↑k : Multiset ι)) (a i • x i))
    (∑ k ∈ s.sym q,
      HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) (∏ i ∈ s, a i ^ Multiset.count i (↑k : Multiset ι))
        (∏ i ∈ s, dp R (Multiset.count i (↑k : Multiset ι)) (x i)))
simp_rw₁ :
  Eq (α := DividedPowerAlgebra R M)
    (∑ x_1 ∈ s.sym q,
      ∏ x_2 ∈ s,
        HSMul.hSMul (β := DividedPowerAlgebra R M) (a x_2 ^ Multiset.count x_2 (↑x_1 : Multiset ι))
          (dp R (Multiset.count x_2 (↑x_1 : Multiset ι)) (x x_2)))
    (∑ k ∈ s.sym q,
      HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) (∏ i ∈ s, a i ^ Multiset.count i (↑k : Multiset ι))
        (∏ i ∈ s, dp R (Multiset.count i (↑k : Multiset ι)) (x i)))
simp_rw₂ :
  Eq (α := DividedPowerAlgebra R M)
    (∑ x_1 ∈ s.sym q,
      ∏ x_2 ∈ s,
        HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
          ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M)
              (a x_2 ^ Multiset.count x_2 (↑x_1 : Multiset ι)) :
            DividedPowerAlgebra R M)
          (dp R (Multiset.count x_2 (↑x_1 : Multiset ι)) (x x_2)))
    (∑ x_1 ∈ s.sym q,
      HMul.hMul (α := DividedPowerAlgebra R M)
        ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M)
          (∏ i ∈ s, a i ^ Multiset.count i (↑x_1 : Multiset ι)))
        (∏ i ∈ s, dp R (Multiset.count i (↑x_1 : Multiset ι)) (x i)))
simp_rw₃ :
  Eq (α := DividedPowerAlgebra R M)
    (∑ x_1 ∈ s.sym q,
      ∏ x_2 ∈ s,
        HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
          ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M)
              (a x_2 ^ Multiset.count x_2 (↑x_1 : Multiset ι)) :
            DividedPowerAlgebra R M)
          (dp R (Multiset.count x_2 (↑x_1 : Multiset ι)) (x x_2)))
    (∑ x_1 ∈ s.sym q,
      HMul.hMul (α := DividedPowerAlgebra R M)
        (∏ x ∈ s,
          (algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M)
            (a x ^ Multiset.count x (↑x_1 : Multiset ι)))
        (∏ i ∈ s, dp R (Multiset.count i (↑x_1 : Multiset ι)) (x i)))
⊢ Eq (α := DividedPowerAlgebra R M) (dp R q (∑ i ∈ s, a i • x i))
    (∑ k ∈ s.sym q,
      HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) (∏ i ∈ s, a i ^ Multiset.count i (↑k : Multiset ι))
        (∏ i ∈ s, dp R (Multiset.count i (↑k : Multiset ι)) (x i)))

Tactic:
simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, map_prod, DividedPowerAlgebra.dp_sum, Algebra.smul_def, DividedPowerAlgebra.dp_smul
-- 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
ι : Type u_3
n : ι → ℕ
m : M
⊢ ∏ i ∈ ∅, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)

Tactic:
simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]

Premises used: Finset.prod_empty, DividedPowerAlgebra.dp_zero, Finset.sum_empty, Nat.multinomial_empty, Nat.cast_one, one_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
ι : Type u_3
n : ι → ℕ
m : M
a : ι
s : Finset ι
hi : a ∉ s
hrec :
  ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
insert :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
        (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M) *
      dp R (∑ x ∈ Insert.insert a s, n x) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((Insert.insert a s).sum n) m)
⊢ ∏ i ∈ Insert.insert a s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((Insert.insert a s).sum n) m)

Tactic:
rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (dp R (n _) m),
      mul_assoc, dp_mul, ← sum_insert hi, nsmul_eq_mul, ← mul_assoc]

Premises used: Finset.prod_insert, mul_assoc, DividedPowerAlgebra.dp_mul, DividedPowerAlgebra.dp, mul_comm, nsmul_eq_mul, Finset.sum_insert
-- 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
ι : Type u_3
n : ι → ℕ
m : M
a : ι
s : Finset ι
hi : a ∉ s
hrec :
  ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
insert :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M) =
    (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
        (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M) *
      dp R (∑ x ∈ Insert.insert a s, n x) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((Insert.insert a s).sum n) m)

Tactic:
congr 1
-- 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
ι : Type u_3
n : ι → ℕ
m : M
a : ι
s : Finset ι
hi : a ∉ s
hrec :
  ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
insert :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M) =
    (↑((n a + ∑ i ∈ s, n i).choose (n a) * multinomial s n) : DividedPowerAlgebra R M)
insert₁ :
  HMul.hMul (α := DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M)
      (↑(multinomial s n) : DividedPowerAlgebra R M) =
    (↑((n a + ∑ i ∈ s, n i).choose (n a) * multinomial s n) : DividedPowerAlgebra R M)
insert₂ :
  HMul.hMul (α := DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M)
      (↑(multinomial s n) : DividedPowerAlgebra R M) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑((n a + ∑ i ∈ s, n i).choose (n a)) : DividedPowerAlgebra R M)
      (↑(multinomial s n) : DividedPowerAlgebra R M)
insert₃ insert₄ :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑((n a + ∑ x ∈ s, n x).choose (n a)) : DividedPowerAlgebra R M)
      (↑(multinomial s n) : DividedPowerAlgebra R M) =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑((n a + ∑ i ∈ s, n i).choose (n a)) : DividedPowerAlgebra R M)
      (↑(multinomial s n) : DividedPowerAlgebra R M)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ Insert.insert a s, n x) (n a)) : DividedPowerAlgebra R M) =
    (↑(multinomial (Insert.insert a s) n) : DividedPowerAlgebra R M)

Tactic:
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Premises used: Nat.cast_mul, Nat.multinomial_insert, mul_comm, Finset.sum_insert