awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ},
    dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i (↑m : Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)
have conv_lhs : Multiset.count i
    (↑(Sym.fill a ((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))
          ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))) :
      Multiset ι) =
  Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)
Tactic: conv_lhs => rw [← m.fill_filterNe a]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ},
    dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ Membership.mem (α :=
    Sym ι
      (n -
        (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
              ((fun (m : Sym ι n) (x : m ∈ (insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
          ℕ)))
    (γ :=
    Finset
      (Sym ι
        (n -
          (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                ((fun (m : Sym ι n) (x : m ∈ (insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
            ℕ))))
    (s.sym
      (n -
        (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
              ((fun (m : Sym ι n) (x : m ∈ (insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
          ℕ)))
    (Sigma.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
        ((fun (m : Sym ι n) (x : m ∈ (insert a s).sym n) ↦ Sym.filterNe a m) m hm) :
      Sym ι
        (n -
          (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                ((fun (m : Sym ι n) (x : m ∈ (insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
            ℕ)))
have h : s = (insert a s).erase a
Tactic: convert! sym_filterNe_mem a hm
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ},
    dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = (insert a s).erase a
have h : s = s
Tactic: rw [erase_insert ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
have empty : ∀ (hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I) {n : ℕ},
  dpow n (Finset.sum ∅ x) = ∑ k ∈ Finset.sym ∅ n, ∏ i ∈ ∅, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
Tactic: induction s using Finset.induction generalizing n with
  | empty =>
    simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
    by_cases hn : n = 0
    · rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]
    · rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩
  | insert a s ha ih =>
    -- This should be golfable using `Finset.symInsertEquiv`
    have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
    simp_rw [sum_insert ha,
      dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
      sum_range, ih hx', mul_sum, sum_sigma', eq_comm]
    apply sum_bij'
      (fun m _ ↦ m.filterNe a)
      (fun m _ ↦ m.2.fill a m.1)
      (fun m hm ↦ mem_sigma.2 ⟨mem_univ _, _⟩)
      (fun m hm ↦ by
        simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
        simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
        intro b
        apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h))
      (fun m _ ↦ m.fill_filterNe a)
    · intro m hm
      simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
      exact Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)
    · intro m hm
      simp only [mem_sym_iff, mem_insert] at hm
      rw [prod_insert ha]
      apply congr_arg₂ _ rfl
      apply prod_congr rfl
      intro i hi
      apply congr_arg₂ _ _ rfl
      conv_lhs => rw [← m.fill_filterNe a]
      exact Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)
    · intro m hm
      convert! sym_filterNe_mem a hm
      rw [erase_insert ha]
Cleared hypotheses: s, hx, n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
empty :
  ∀ (hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I) {n : ℕ},
    dpow n (Finset.sum ∅ x) = ∑ k ∈ Finset.sym ∅ n, ∏ i ∈ ∅, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ},
      dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i))
  (hx : ∀ i ∈ insert a s, x i ∈ I) {n : ℕ},
  dpow n ((insert a s).sum x) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
Tactic: induction s using Finset.induction generalizing n with
  | empty =>
    simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
    by_cases hn : n = 0
    · rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]
    · rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩
  | insert a s ha ih =>
    -- This should be golfable using `Finset.symInsertEquiv`
    have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
    simp_rw [sum_insert ha,
      dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
      sum_range, ih hx', mul_sum, sum_sigma', eq_comm]
    apply sum_bij'
      (fun m _ ↦ m.filterNe a)
      (fun m _ ↦ m.2.fill a m.1)
      (fun m hm ↦ mem_sigma.2 ⟨mem_univ _, _⟩)
      (fun m hm ↦ by
        simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
        simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
        intro b
        apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h))
      (fun m _ ↦ m.fill_filterNe a)
    · intro m hm
      simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
      exact Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)
    · intro m hm
      simp only [mem_sym_iff, mem_insert] at hm
      rw [prod_insert ha]
      apply congr_arg₂ _ rfl
      apply prod_congr rfl
      intro i hi
      apply congr_arg₂ _ _ rfl
      conv_lhs => rw [← m.fill_filterNe a]
      exact Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)
    · intro m hm
      convert! sym_filterNe_mem a hm
      rw [erase_insert ha]
Cleared hypotheses: s, hx, n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ hJ.dpow n (x.sum fun (i : ι) (r : A) ↦ r • b i) =
    ∑ k ∈ x.support.sym n,
      x.prod fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑k : Multiset ι) • hJ.dpow (Multiset.count i (↑k : Multiset ι)) (b i)
have rw : Eq.{u_3 + 1} (α := S)
  (∑ k ∈ x.support.sym n,
    ∏ i ∈ x.support,
      hJ.dpow (Multiset.count i (↑k : Multiset ι))
        (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)))
  (∑ k ∈ x.support.sym n,
    x.prod fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑k : Multiset ι) • hJ.dpow (Multiset.count i (↑k : Multiset ι)) (b i))
Tactic: rw [Finsupp.sum, hJ.dpow_sum (fun i hi ↦ Submodule.smul_of_tower_mem J _ (hx i hi))]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
⊢ Eq.{u_3 + 1} (α := S)
    (∑ k ∈ x.support.sym n,
      ∏ i ∈ x.support,
        hJ.dpow (Multiset.count i (↑k : Multiset ι))
          (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)))
    (∑ k ∈ x.support.sym n,
      x.prod fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑k : Multiset ι) • hJ.dpow (Multiset.count i (↑k : Multiset ι)) (b i))
have apply : ∀ x_1 ∈ x.support.sym n,
  Eq.{u_3 + 1} (α := S)
    (∏ i ∈ x.support,
      hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
        (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)))
    (x.prod fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x_1 : Sym ι n
h : x_1 ∈ x.support.sym n
⊢ Eq.{u_3 + 1} (α := S)
    (∏ i ∈ x.support,
      hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
        (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)))
    (x.prod fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
have apply : ∀ x_2 ∈ x.support,
  hJ.dpow (Multiset.count x_2 (↑x_1 : Multiset ι))
      (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) x_2 : A) (b x_2)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      x_2 ((x : (a : ι) → A) x_2)
Tactic: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x_1 : Sym ι n
h : x_1 ∈ x.support.sym n
i : ι
hi : i ∈ x.support
⊢ hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
have rw : hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
    (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S) (b i)) =
  (fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
    i ((x : (a : ι) → A) i)
Tactic: rw [Algebra.smul_def, hJ.dpow_mul (hx i hi), ← map_pow, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x_1 : Sym ι n
h : x_1 ∈ x.support.sym n
i : ι
hi : i ∈ x.support
rw :
  hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
⊢ hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
have rw₁ : HPow.hPow (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S)
      (Multiset.count i (↑x_1 : Multiset ι)) *
    hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i) =
  (fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
    i ((x : (a : ι) → A) i)
Tactic: rw [Algebra.smul_def, hJ.dpow_mul (hx i hi), ← map_pow, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x_1 : Sym ι n
h : x_1 ∈ x.support.sym n
i : ι
hi : i ∈ x.support
rw :
  hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
rw₁ :
  HPow.hPow (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S)
        (Multiset.count i (↑x_1 : Multiset ι)) *
      hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
⊢ hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
have rw₂ : HMul.hMul (α := S)
    ((algebraMap A S : (a : A) → S)
        (HPow.hPow (α := A) ((x : (a : ι) → A) i : A) (Multiset.count i (↑x_1 : Multiset ι))) :
      S)
    (hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i)) =
  (fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
    i ((x : (a : ι) → A) i)
Tactic: rw [Algebra.smul_def, hJ.dpow_mul (hx i hi), ← map_pow, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
ι : Type u_2
inst_1 : DecidableEq ι
S : Type u_3
inst_2 : CommSemiring S
inst_3 : Algebra A S
J : Ideal S
hJ : DividedPowers J
b : ι → S
x : ι →₀ A
hx : ∀ i ∈ x.support, b i ∈ J
n : ℕ
x_1 : Sym ι n
h : x_1 ∈ x.support.sym n
i : ι
hi : i ∈ x.support
rw :
  hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HMul.hMul (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
rw₁ :
  HPow.hPow (α := S) ((algebraMap A S : (a : A) → S) ((x : (a : ι) → A) i : A) : S)
        (Multiset.count i (↑x_1 : Multiset ι)) *
      hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
rw₂ :
  HMul.hMul (α := S)
      ((algebraMap A S : (a : A) → S)
          (HPow.hPow (α := A) ((x : (a : ι) → A) i : A) (Multiset.count i (↑x_1 : Multiset ι))) :
        S)
      (hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
⊢ hJ.dpow (Multiset.count i (↑x_1 : Multiset ι))
      (HSMul.hSMul.{u_1, u_3, u_3} (α := A) ((x : (a : ι) → A) i : A) (b i)) =
    (fun (i : ι) (r : A) ↦
        r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
      i ((x : (a : ι) → A) i)
have rw₃ : HPow.hPow (α := A) ((x : (a : ι) → A) i : A) (Multiset.count i (↑x_1 : Multiset ι)) •
    hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i) =
  (fun (i : ι) (r : A) ↦
      r ^ Multiset.count i (↑x_1 : Multiset ι) • hJ.dpow (Multiset.count i (↑x_1 : Multiset ι)) (b i))
    i ((x : (a : ι) → A) i)
Tactic: rw [Algebra.smul_def, hJ.dpow_mul (hx i hi), ← map_pow, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (∏ i ∈ insert a s, r i) =
    HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have insert : hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: rw [Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have pos : ∀ (h : s.Nonempty),
  hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: by_cases h : s.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
pos :
  ∀ (h : s.Nonempty),
    hI.dpow n (r a * ∏ x ∈ s, r x) =
      HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have neg : ∀ (h : ¬s.Nonempty),
  hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: by_cases h : s.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have pos : r a ^ n * hI.dpow n (∏ x ∈ s, r x) =
  HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: rw [dpow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
pos :
  r a ^ n * hI.dpow n (∏ x ∈ s, r x) =
    HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
⊢ hI.dpow n (r a * ∏ x ∈ s, r x) = HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have pos₁ : ∏ x ∈ s, r x ∈ I
Tactic: rw [dpow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ r a ^ n * hI.dpow n (∏ x ∈ s, r x) =
    HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
have pos : r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) * ∏ i ∈ s, hI.dpow n (r i) =
  HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a) * ∏ i ∈ s, hI.dpow n (r i)
Tactic: simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) * ∏ i ∈ s, hI.dpow n (r i) =
    HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a) * ∏ i ∈ s, hI.dpow n (r i)
have apply : r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a)
Tactic: apply congr_arg₂ _ _ rfl