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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
have pos : ∀ (hn : n = 0), dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
Tactic: by_cases hn : n = 0
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
pos : ∀ (hn : n = 0), dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
have neg : ∀ (hn : ¬n = 0), dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
Tactic: by_cases hn : n = 0
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
have pos : dpow 0 0 = (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)
Tactic: rw [hn]
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow 0 0 = (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)
have pos : Eq.{u_1 + 1} (α := A) 1 (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)
Tactic: rw [dpow_zero I.zero_mem]
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
have neg : Eq.{u_1 + 1} (α := A) (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A) (↑0 : A)
Tactic: rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ Eq.{u_1 + 1} (α := A) (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A) (↑0 : A)
have neg : card.{u_3} (α := Sym ι n) (Finset.sym ∅ n) = 0
Tactic: apply congr_arg
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ card.{u_3} (α := Sym ι n) (Finset.sym ∅ n) = 0
have neg : n ≠ 0 ∧ Eq.{u_3 + 1} (α := Finset ι) ∅ ∅
Tactic: rw [card_eq_zero, sym_eq_empty]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
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 : ℕ
⊢ 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)
have hx' : ∀ i ∈ s, x i ∈ I
Tactic: have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
-- 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
⊢ 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)
have insert : Eq.{u_1 + 1} (α := A) (∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i))
  (∑
    x_1 ∈
      Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦ s.sym (n - (↑a : ℕ)),
    dpow (↑(x_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow (Multiset.count i (↑(x_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)) (x i))
Tactic: 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]
-- 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 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm :
  Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
    (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦ s.sym (n - (↑a : ℕ))) m
⊢ (fun (m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ)))
          (x :
            Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
              (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
                s.sym (n - (↑a : ℕ)))
              m) ↦
        Sym.fill a (m.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
          (m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))))
      m hm ∈
    (insert a s).sym n
have simp : ∀ (a_1 : ι),
  (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ a_1 = a ∨
      a_1 ∈ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))) →
    a_1 = a ∨ a_1 ∈ s
Tactic: simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
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 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm :
  Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
    (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦ s.sym (n - (↑a : ℕ))) m
⊢ ∀ (a_1 : ι),
    (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ a_1 = a ∨
        a_1 ∈ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))) →
      a_1 = a ∨ a_1 ∈ s
have hm₁ : ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s
Tactic: simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
Cleared hypotheses: 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
⊢ Eq.{u_1 + 1} (α := A) (∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i))
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
          s.sym (n - (↑a : ℕ)),
      dpow (↑(x_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
        ∏ i ∈ s,
          dpow (Multiset.count i (↑(x_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)) (x i))
have insert : ∀ (a_1 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ)))
  (ha :
    Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
      (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦ s.sym (n - (↑a : ℕ)))
      a_1),
  Sym.filterNe a
      (Sym.fill a (a_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
        (a_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
    a_1
Tactic: 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)
-- 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.insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
insert :
  ∀ (a_1 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ)))
    (ha :
      Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
        (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
          s.sym (n - (↑a : ℕ)))
        a_1),
    Sym.filterNe a
        (Sym.fill a (a_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
          (a_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
      a_1
⊢ Eq.{u_1 + 1} (α := A)
    (∑ k ∈ (Insert.insert a s).sym n, ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i))
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
          s.sym (n - (↑a : ℕ)),
      dpow (↑(x_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
        ∏ i ∈ s,
          dpow (Multiset.count i (↑(x_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)) (x i))
have insert₁ : ∀ (a_1 : Sym ι n) (ha : a_1 ∈ (Insert.insert a s).sym n),
  ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑a_1 : Multiset ι)) (x i) =
    dpow (↑((Sym.filterNe a a_1).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i
            (↑((Sym.filterNe a a_1).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)
Tactic: 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)
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
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 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm :
  Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
    (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦ s.sym (n - (↑a : ℕ))) m
⊢ Sym.filterNe a
      (Sym.fill a (m.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
        (m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
    m
have hm₁ : ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s
Tactic: simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
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
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i (↑m : Multiset ι)) (x i) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)
have hm₁ : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
Tactic: simp only [mem_sym_iff, mem_insert] at hm
Cleared hypotheses: 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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i (↑m : Multiset ι)) (x i) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)
have insert : dpow (Multiset.count a (↑m : Multiset ι)) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
  dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
    ∏ i ∈ s,
      dpow
        (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
        (x i)
Tactic: rw [prod_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 ι
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
⊢ dpow (Multiset.count a (↑m : Multiset ι)) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)
have insert : Eq.{u_1 + 1} (α := A) (∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1))
  (∏ i ∈ s,
    dpow (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
      (x i))
Tactic: apply congr_arg₂ _ rfl
-- 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
⊢ Eq.{u_1 + 1} (α := A) (∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1))
    (∏ i ∈ s,
      dpow
        (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
        (x i))
have insert : ∀ x_1 ∈ s,
  dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
    dpow
      (Multiset.count x_1 (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
      (x x_1)
Tactic: apply prod_congr rfl
-- 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
⊢ dpow (Multiset.count i (↑m : Multiset ι)) (x i) =
    dpow (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
      (x i)
have apply : Multiset.count i (↑m : Multiset ι) =
  Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)
Tactic: apply congr_arg₂ _ _ rfl
-- 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 ι)
have rw : 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 ι)
Tactic: rw [← m.fill_filterNe a]