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
ι : 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)))
⊢ 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)
      (∏ 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)))
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
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)
⊢ ∏ i ∈ insert a s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((insert a s).sum n) m)
have insert : HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ insert a s, n x) (n a)) : DividedPowerAlgebra R M) *
    dp R (∑ x ∈ insert a s, n x) m =
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
    (dp R ((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]
-- 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
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)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
        (↑(Nat.choose (∑ x ∈ insert a s, n x) (n a)) : DividedPowerAlgebra R M) *
      dp R (∑ x ∈ insert a s, n x) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((insert a s).sum n) m)
have insert : HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
    (↑(Nat.choose (∑ x ∈ insert a s, n x) (n a)) : DividedPowerAlgebra R M) =
  (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
Tactic: congr 1
-- 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
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)
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
      (↑(Nat.choose (∑ x ∈ insert a s, n x) (n a)) : DividedPowerAlgebra R M) =
    (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
have insert : HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M)
    (↑(Nat.choose (∑ x ∈ 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)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- 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
s : Finset ι
n : ι → ℕ
m : M
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
have empty : ∏ i ∈ ∅, dp R (n i) m =
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    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]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- 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
s : Finset ι
n : ι → ℕ
m : M
empty :
  ∏ i ∈ ∅, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
have insert : ∀ (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)),
  ∏ i ∈ insert a s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((insert a s).sum n) m)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    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]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- 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
s : Finset ι
n : ι → ℕ
m : M
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
have empty : ∏ i ∈ ∅, dp R (n i) m =
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    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]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- 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
s : Finset ι
n : ι → ℕ
m : M
empty :
  ∏ i ∈ ∅, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial ∅ n) : DividedPowerAlgebra R M) (dp R (Finset.sum ∅ n) m)
⊢ ∏ i ∈ s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial s n) : DividedPowerAlgebra R M) (dp R (s.sum n) m)
have insert : ∀ (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)),
  ∏ i ∈ insert a s, dp R (n i) m =
    HMul.hMul (α := DividedPowerAlgebra R M) (↑(multinomial (insert a s) n) : DividedPowerAlgebra R M)
      (dp R ((insert a s).sum n) m)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
  | insert _ _ hi hrec =>
    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]
    congr 1
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- 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
x : M
n : ℕ
h :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) (n + 1)
have succ : HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(n ! * (n + 1).choose n) : DividedPowerAlgebra R M) (dp R (n + 1) x)
Tactic: rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_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 : M
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n
have zero : HMul.hMul (α := DividedPowerAlgebra R M) (↑0! : DividedPowerAlgebra R M) (dp R 0 x) =
  HPow.hPow (α := DividedPowerAlgebra R M) (β := ℕ) (dp R 1 x) 0
Tactic: induction n with
  | zero => simp [dp_zero]
  | succ n h =>
    rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
    simp [mul_comm _ (n + 1), Nat.factorial_succ]
Cleared hypotheses: n
-- 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 : M
zero :
  HMul.hMul (α := DividedPowerAlgebra R M) (↑0! : DividedPowerAlgebra R M) (dp R 0 x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (β := ℕ) (dp R 1 x) 0
⊢ HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n
have succ : ∀ (n : ℕ)
  (h :
    HMul.hMul (α := DividedPowerAlgebra R M) (↑n ! : DividedPowerAlgebra R M) (dp R n x) =
      HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) n),
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(n + 1)! : DividedPowerAlgebra R M) (dp R (n + 1) x) =
    HPow.hPow (α := DividedPowerAlgebra R M) (dp R 1 x) (n + 1)
Tactic: induction n with
  | zero => simp [dp_zero]
  | succ n h =>
    rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
    simp [mul_comm _ (n + 1), Nat.factorial_succ]
Cleared hypotheses: n
-- 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
x : ℕ
x_1 : M
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
have rw : Eq.{u_3 + 1} (α := A) ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
  ((g : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
Tactic: rw [h]
-- 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔
    ∀ (n : ℕ) (m : M),
      Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
        ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
have refine : ∀
  (h :
    ∀ (n : ℕ) (m : M),
      Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
        ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)),
  f = g
Tactic: refine ⟨fun h _ _ ↦ by rw [h], fun h ↦ ?_⟩
-- 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
⊢ f = g
have rw : Eq (α := (a : DividedPowerAlgebra R M) → A) (⇑f : (a : DividedPowerAlgebra R M) → A)
  (⇑g : (a : DividedPowerAlgebra R M) → A)
Tactic: rw [DFunLike.ext'_iff]
-- 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
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h :
  ∀ (n : ℕ) (m : M),
    Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
      ((g : (a : DividedPowerAlgebra R M) → A) (dp R n m) : A)
⊢ Eq (α := (a : DividedPowerAlgebra R M) → A) (⇑f : (a : DividedPowerAlgebra R M) → A)
    (⇑g : (a : DividedPowerAlgebra R M) → A)
have a : Eq (α := MvPolynomial.{u_2, u_1} (ℕ × M) R → A)
  ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
      (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
        MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
    (⇑f : (a : DividedPowerAlgebra R M) → A))
  ((fun (g : RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) → A) ↦
      (g ∘ (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) :
        MvPolynomial.{u_2, u_1} (ℕ × M) R → A))
    (⇑g : (a : DividedPowerAlgebra R M) → A))
Tactic: apply Function.Surjective.injective_comp_right mkAlgHom_surjective
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ Eq (α := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) ⊤
have rw : LE.le (α := Submodule R (DividedPowerAlgebra R M)) ⊤
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
r : R
⊢ Membership.mem (α := DividedPowerAlgebra R M) (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) r : DividedPowerAlgebra R M)
have C : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (HSMul.hSMul (β := DividedPowerAlgebra R M) r 1)
Tactic: simp only [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (hypothesis)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
x : DividedPowerAlgebra R M
k : ℕ
m : M
hx :
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) x
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k m)
have hm : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m
Tactic: have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
m : M
x : DividedPowerAlgebra R M
k : ℕ
hx :
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) x
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k 0)
have dp : Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
  (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
  (x * if k = 0 then 1 else 0)
Tactic: rw [dp_null]