awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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 (γ :=
    Finset (Sym ι (n - (↑((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ))))
    (((insert a s).erase a).sym
      (n - (↑((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 : ℕ))))

Tactic:
sym_filterNe_mem a hm

Premises used: Finset.sym_filterNe_mem
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
h : s = (insert a s).erase a
⊢ 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)) :
            ℕ)))

Tactic:
convert! sym_filterNe_mem a hm

Premises used: Finset.sym_filterNe_mem
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
h h₁ : s = s
⊢ s = (insert a s).erase a

Tactic:
rw [erase_insert ha]

Premises used: Finset.erase_insert
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
⊢ hI.dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, hI.dpow (Multiset.count i (↑k : Multiset ι)) (x i)

Tactic:
dpow_sum' hI.dpow hI.dpow_zero hI.dpow_add hI.dpow_eval_zero hx

Premises used: DividedPowers.dpow_sum', DividedPowers.dpow_add, DividedPowers.dpow_eval_zero, DividedPowers.dpow_zero, DividedPowers.dpow
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_2
inst_1 : DecidableEq ι
x : ι →₀ A
hx : ∀ (i : ι), Membership.mem (α := A) I ((x : (a : ι) → A) i : A)
n : ℕ
⊢ hI.dpow n (x.sum fun (x : ι) (r : A) ↦ r) =
    ∑ k ∈ x.support.sym n, x.prod fun (i : ι) (r : A) ↦ hI.dpow (Multiset.count i (↑k : Multiset ι)) r

Tactic:
simp [Finsupp.sum, hI.dpow_sum (fun i _ ↦ hx i), Finsupp.prod]

Premises used: Finsupp.sum, DividedPowers.dpow_sum, Finsupp.prod
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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 : ℕ
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))
⊢ 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)

Tactic:
rw [Finsupp.sum, hJ.dpow_sum (fun i hi ↦ Submodule.smul_of_tower_mem J _ (hx i hi))]

Premises used: Finsupp.sum, DividedPowers.dpow_sum, Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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 : ℕ
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))
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
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)
⊢ 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.prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [Algebra.smul_def, hJ.dpow_mul (hx i hi), ← map_pow, ← Algebra.smul_def]

Premises used: map_pow, DividedPowers.dpow_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
hs : Finset.Nonempty.{u_3} (α := ι) ∅
hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I
⊢ hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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.insert a s).Nonempty
hs' : ∀ i ∈ Insert.insert a s, r i ∈ I
insert :
  hI.dpow n (r a * ∏ x ∈ s, r x) =
    HSMul.hSMul (β := A) (n ! ^ (#(Insert.insert a s) - 1)) (∏ i ∈ Insert.insert a s, hI.dpow n (r i))
⊢ hI.dpow n (∏ i ∈ Insert.insert a s, r i) =
    HSMul.hSMul (β := A) (n ! ^ (#(Insert.insert a s) - 1)) (∏ i ∈ Insert.insert a s, hI.dpow n (r i))

Tactic:
rw [Finset.prod_insert has]

Premises used: Finset.prod_insert
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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))
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))
⊢ 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

Premises used: Finset.Nonempty
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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))
pos₁ : ∏ x ∈ s, r x ∈ 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))

Tactic:
rw [dpow_mul]

Premises used: DividedPowers.dpow_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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 * 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)
⊢ 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:
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]

Premises used: Finset.prod_insert, mul_assoc, Finset.card_insert_of_notMem, Finset.mem_insert_of_mem, nsmul_eq_mul, add_tsub_cancel_right, Nat.cast_pow
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
apply : r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a)
⊢ 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:
apply congr_arg₂ _ _ rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
⊢ #s = #s - 1 + 1

Tactic:
grind
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
⊢ #s = #s - 1 + 1

Tactic:
have : #s = #s - 1 + 1 := by grind
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
this : #s = #s - 1 + 1
nth_rewrite :
  r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) (#s - 1 + 1) * hI.dpow n (r a)
⊢ r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a)

Tactic:
nth_rewrite 2 [this]
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
this : #s = #s - 1 + 1
⊢ r a ∈ I

Tactic:
hs' a (mem_insert_self a s)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
this : #s = #s - 1 + 1
⊢ r a ∈ I

Tactic:
exact hs' a (mem_insert_self a s)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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 : ∀ (j : ι) (hj : j ∈ s), ∏ x ∈ s, r x ∈ I
⊢ ∏ x ∈ s, r x ∈ I

Tactic:
obtain ⟨j, hj⟩ := h
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
j : ι
hj : j ∈ s
pos : (∏ x ∈ s \ {j}, r x) * r j ∈ I
⊢ ∏ x ∈ s, r x ∈ I

Tactic:
rw [Finset.prod_eq_prod_diff_singleton_mul hj]

Premises used: Finset.prod_eq_prod_diff_singleton_mul
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
j : ι
hj : j ∈ s
⊢ (∏ x ∈ s \ {j}, r x) * r j ∈ I

Tactic:
I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))

Premises used: Set.Mem, Finset.mem_insert_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
j : ι
hj : j ∈ s
⊢ (∏ x ∈ s \ {j}, r x) * r j ∈ I

Tactic:
exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))

Premises used: Finset.mem_insert_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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))

Tactic:
simp [not_nonempty_iff_eq_empty.mp h]

Premises used: Finset.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
empty :
  ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
    hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
insert :
  ∀ (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.insert a s).Nonempty) (hs' : ∀ i ∈ Insert.insert a s, r i ∈ I),
    hI.dpow n (∏ i ∈ Insert.insert a s, r i) =
      HSMul.hSMul (β := A) (n ! ^ (#(Insert.insert a s) - 1)) (∏ i ∈ Insert.insert a s, hI.dpow n (r i))
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))

Tactic:
induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · 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]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, pow_succ, mul_assoc, Insert.insert, DividedPowers.dpow_mul, Finset.Nonempty, mul_comm, nsmul_eq_mul, add_tsub_cancel_right, Nat.cast_pow, rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
empty :
  ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
    hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
insert :
  ∀ (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.insert a s).Nonempty) (hs' : ∀ i ∈ Insert.insert a s, r i ∈ I),
    hI.dpow n (∏ i ∈ Insert.insert a s, r i) =
      HSMul.hSMul (β := A) (n ! ^ (#(Insert.insert a s) - 1)) (∏ i ∈ Insert.insert a s, hI.dpow n (r i))
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · 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]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, pow_succ, mul_assoc, Insert.insert, DividedPowers.dpow_mul, Finset.Nonempty, mul_comm, nsmul_eq_mul, add_tsub_cancel_right, Nat.cast_pow, rfl, congr_arg₂