internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.coincide_on_smul
Proof state before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y =
    ∑ k ∈ Finset.antidiagonal n, hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
Theorem: DividedPowers.coincide_on_smul
Proof state before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
Tactic:
intro k _
Proof state after:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ Finset.antidiagonal n
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Theorem: DividedPowers.coincide_on_smul
Proof state before:
case add
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
a✝ : k ∈ Finset.antidiagonal n
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic:
rw [hx', hy']
Proof state after:
no goals
Theorem: DividedPowers.mul_dpow
Proof state before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
s : Finset ι
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
Tactic:
classical
induction s using Finset.induction with
| empty =>
  simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
  rw [hI.dpow_zero ha]
| insert hi hrec =>
  rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
    mul_assoc, dpow_mul _ _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
  apply congr_arg₂ _ _ rfl
  rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
Proof state after:
no goals
Theorem: DividedPowers.mul_dpow
Proof state before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
s : Finset ι
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
Tactic:
induction s using Finset.induction with
| empty =>
  simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
  rw [hI.dpow_zero ha]
| insert hi hrec =>
  rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
    mul_assoc, dpow_mul _ _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
  apply congr_arg₂ _ _ rfl
  rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
Proof state after:
no goals
Theorem: DividedPowers.mul_dpow
Proof state before:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = ↑(Nat.multinomial ∅ n) * hI.dpow (∅.sum n) a
Tactic:
simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
Proof state after:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ 1 = hI.dpow 0 a
Theorem: DividedPowers.mul_dpow
Proof state before:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ 1 = hI.dpow 0 a
Tactic:
rw [hI.dpow_zero ha]
Proof state after:
no goals
Theorem: DividedPowers.mul_dpow
Proof state before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ∏ i ∈ insert a✝ s✝, hI.dpow (n i) a = ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Tactic:
rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
  mul_assoc, dpow_mul _ _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
Proof state after:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Theorem: DividedPowers.mul_dpow
Proof state before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(Nat.multinomial (insert a✝ s✝) n)
Theorem: DividedPowers.mul_dpow
Proof state before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(Nat.multinomial (insert a✝ s✝) n)
Tactic:
rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ antidiagonal n, dpow k.1 x * dpow k.2 y
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
Tactic:
simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
Proof state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case empty
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n (∅.sum x) = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dpow (Multiset.count i ↑k) (x i)
Tactic:
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
Proof state after:
case empty
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n 0 = ↑(∅.sym n).card
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case empty
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n 0 = ↑(∅.sym n).card
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(∅.sym n).card

case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(∅.sym n).card
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(∅.sym n).card
Tactic:
rw [hn]
Proof state after:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow 0 0 = ↑(∅.sym 0).card
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow 0 0 = ↑(∅.sym 0).card
Tactic:
rw [dpow_zero I.zero_mem]
Proof state after:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ 1 = ↑(∅.sym 0).card
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ 1 = ↑(∅.sym 0).card
Tactic:
simp only [sym_zero, card_singleton, Nat.cast_one]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(∅.sym n).card
Tactic:
rw [dpow_eval_zero hn]
Proof state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ 0 = ↑(∅.sym n).card
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ 0 = ↑(∅.sym n).card
Tactic:
apply symm
Proof state after:
case neg.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(∅.sym n).card = 0
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(∅.sym n).card = 0
Tactic:
rw [← Nat.cast_zero]
Proof state after:
case neg.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(∅.sym n).card = ↑0
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(∅.sym n).card = ↑0
Tactic:
apply congr_arg
Proof state after:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ (∅.sym n).card = 0
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ (∅.sym n).card = 0
Tactic:
rw [card_eq_zero]
Proof state after:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ∅.sym n = ∅
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ∅.sym n = ∅
Tactic:
rw [sym_eq_empty]
Proof state after:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case neg.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Tactic:
exact ⟨hn, rfl⟩
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case insert
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (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) (x i)
Tactic:
have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi => hx i (Finset.mem_insert_of_mem hi)
Proof state after:
case insert
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (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) (x i)
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case insert
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (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) (x i)
Tactic:
simp_rw [sum_insert ha,
  dpow_add n (hx a (Finset.mem_insert_self a s)) (I.sum_mem fun i => hx' i),
  sum_range, ih hx', mul_sum, sum_sigma']
Proof state after:
case insert
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1 ∈ univ.sigma fun a => s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case insert
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1 ∈ univ.sigma fun a => s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
Tactic:
apply symm
Proof state after:
case insert.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i) =
    ∑ x_1 ∈ univ.sigma fun a => s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i)