awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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))
        ((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
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)
have C : ∀ (a : R) (f : DividedPowerAlgebra R M)
  (hf :
    (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) =
      f),
  P
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
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)
Cleared hypotheses: f, F, hf
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)
have 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))
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)
Cleared hypotheses: f, F, hf
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)
have 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))
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)
Cleared hypotheses: f, F, hf
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((MvPolynomial.C : (a : R) → MvPolynomial (ℕ × M) R) a))
have rw : P ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a)
Tactic: rw [mkAlgHom_C]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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) (dp R 0 m) 1
have 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))
Tactic: rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ dp R n (r • m) = HSMul.hSMul (β := DividedPowerAlgebra R M) (r ^ n) (dp R n m)
have 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)
Tactic: rw [dp_def, dp_def, ← map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)
have inl : Eq (α := DividedPowerAlgebra R M) (dp R n 0) 1
Tactic: rw [if_pos hn, hn, dp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)
have inl₁ : Eq (α := DividedPowerAlgebra R M) (dp R 0 0) 1
Tactic: rw [if_pos hn, hn, dp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)
have inl₂ : Eq (α := DividedPowerAlgebra R M) 1 1
Tactic: rw [if_pos hn, hn, dp_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)
have inr : HSMul.hSMul (β := DividedPowerAlgebra R M) (HPow.hPow (α := R) 0 n) (dp R n 0) = 0
Tactic: rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ HSMul.hSMul (β := DividedPowerAlgebra R M) (HPow.hPow (α := R) 0 n) (dp R n 0) = 0
have inr : HSMul.hSMul (α := R) (β := DividedPowerAlgebra R M) 0 (dp R n 0) = 0
Tactic: rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ HSMul.hSMul (β := DividedPowerAlgebra R M) (HPow.hPow (α := R) 0 n) (dp R n 0) = 0
have inr₁ : Eq (α := DividedPowerAlgebra R M) 0 0
Tactic: rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) (if n = 0 then 1 else 0)
have x : 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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) 0
have rw : Eq (α := DividedPowerAlgebra R M) (if n = 0 then 1 else 0) 0
Tactic: rw [dp_null, if_neg hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n 0) 0
have rw₁ : Eq (α := DividedPowerAlgebra R M) 0 0
Tactic: rw [dp_null, if_neg hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ 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)
have 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)
Tactic: simp only [dp_def, ← _root_.map_mul, ← map_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ (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))
have 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))
Tactic: rw [_root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, x + y)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
          ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.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 (x_1.2, y)) :
            RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      DividedPowerAlgebra R M)
have rw : Eq (α := DividedPowerAlgebra R M)
  ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, x)) (X (k.2, y))))
  (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.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 (x_1.2, y)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
Tactic: rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add, map_sum,
    Finset.sum_congr rfl (fun k _ ↦ by rw [_root_.map_mul])]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
rw :
  Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, x)) (X (k.2, y))))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.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 (x_1.2, y)) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, x + y)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
          ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.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 (x_1.2, y)) :
            RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      DividedPowerAlgebra R M)
have rw₁ : Eq (α := DividedPowerAlgebra R M)
  (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    (mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (x_1.1, x)) (X (x_1.2, y))))
  (∑ x_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R M)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (x_1.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 (x_1.2, y)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
Tactic: rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add, map_sum,
    Finset.sum_congr rfl (fun k _ ↦ by rw [_root_.map_mul])]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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
⊢ 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)))
have 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)))
Tactic: simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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)))
⊢ 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)))
have 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)))
Tactic: simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
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)))
⊢ 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)))
have 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)))
Tactic: simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]