Theorem: DividedPowers.dpow_sum_aux (DividedPowers/Basic.lean)

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
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)

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]
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

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
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

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]
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

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]
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

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]
State after:
no goals

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]
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

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
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

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]
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

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
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

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]
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 = ∅

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]
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 ∧ ∅ = ∅

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⟩
State after:
no goals

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)
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)

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']
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)

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
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)

State before:
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)
Tactic:
apply sum_bij'
  (fun m _ => Sym.filterNe a m)
  (fun m _ => m.2.fill a m.1)
  (fun m hm => Finset.mem_sigma.2 ⟨mem_univ _, _⟩)
  (fun m hm => by
    rw [mem_sym_iff]
    intro i hi
    rw [Sym.mem_fill_iff] at hi
    cases hi with
    | inl hi =>
      rw [hi.2]
      exact mem_insert_self a s
    | inr hi =>
      simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
      exact mem_insert_of_mem (hm i hi))
  (fun m _ => Sym.fill_filterNe a _ )
State after:
case insert.a.right_inv
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
⊢ ∀ a_1 ∈ univ.sigma fun a => s.sym (n - ↑a), Sym.filterNe a (Sym.fill a a_1.fst a_1.snd) = a_1

case insert.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
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
⊢ ∀ a_1 ∈ (insert a s).sym n,
    ∏ i ∈ insert a s, dpow (Multiset.count i ↑a_1) (x i) =
      dpow (↑(Sym.filterNe a a_1).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a a_1).snd) (x i)

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
⊢ ∀ (m : Sym ι n) (hm : m ∈ (insert a s).sym n),
    ((fun m x => Sym.filterNe a m) m hm).snd ∈ s.sym (n - ↑((fun m x => Sym.filterNe a m) m hm).fst)

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_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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ (fun m x => Sym.fill a m.fst m.snd) m hm ∈ (insert a s).sym n
Tactic:
rw [mem_sym_iff]
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 ι
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ ∀ a_1 ∈ (fun m x => Sym.fill a m.fst m.snd) m hm, a_1 ∈ insert a s

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_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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ ∀ a_1 ∈ (fun m x => Sym.fill a m.fst m.snd) m hm, a_1 ∈ insert a s
Tactic:
intro i hi
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 ι
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ (fun m x => Sym.fill a m.fst m.snd) m hm
⊢ i ∈ insert a s

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_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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ (fun m x => Sym.fill a m.fst m.snd) m hm
⊢ i ∈ insert a s
Tactic:
rw [Sym.mem_fill_iff] at hi
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 ι
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a ∨ i ∈ m.snd
⊢ i ∈ insert a s

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_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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a ∨ i ∈ m.snd
⊢ i ∈ insert a s
Tactic:
cases hi with
| inl hi =>
  rw [hi.2]
  exact mem_insert_self a s
| inr hi =>
  simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
  exact mem_insert_of_mem (hm i hi)
State after:
no goals

State before:
case inl
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ i ∈ insert a s
Tactic:
rw [hi.2]
State after:
case inl
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ a ∈ insert a s

State before:
case inl
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ a ∈ insert a s
Tactic:
exact mem_insert_self a s
State after:
no goals

State before:
case inr
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ m.snd
⊢ i ∈ insert a s
Tactic:
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
State after:
case inr
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
i : ι
hi : i ∈ m.snd
hm : ∀ a ∈ m.snd, a ∈ s
⊢ i ∈ insert a s

State before:
case inr
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
i : ι
hi : i ∈ m.snd
hm : ∀ a ∈ m.snd, a ∈ s
⊢ i ∈ insert a s
Tactic:
exact mem_insert_of_mem (hm i hi)
State after:
no goals

State before:
case insert.a.right_inv
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
⊢ ∀ a_1 ∈ univ.sigma fun a => s.sym (n - ↑a), Sym.filterNe a (Sym.fill a a_1.fst a_1.snd) = a_1
Tactic:
intro m hm
State after:
case insert.a.right_inv
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m

State before:
case insert.a.right_inv
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Tactic:
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
State after:
case insert.a.right_inv
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : ∀ a ∈ m.snd, a ∈ s
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m

State before:
case insert.a.right_inv
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
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : ∀ a ∈ m.snd, a ∈ s
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Tactic:
exact Sym.filter_ne_fill a m fun a_1 => ha (hm a a_1)
State after:
no goals

State before:
case insert.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
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
⊢ ∀ a_1 ∈ (insert a s).sym n,
    ∏ i ∈ insert a s, dpow (Multiset.count i ↑a_1) (x i) =
      dpow (↑(Sym.filterNe a a_1).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a a_1).snd) (x i)
Tactic:
intro m hm
State after:
case insert.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
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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i ↑m) (x i) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

State before:
case insert.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
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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i ↑m) (x i) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
simp only [mem_sym_iff, mem_insert] at hm
State after:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i ↑m) (x i) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

State before:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ i ∈ insert a s, dpow (Multiset.count i ↑m) (x i) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
rw [Finset.prod_insert ha]
State after:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dpow (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

State before:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dpow (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) =
    dpow (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply congr_arg₂ _ rfl
State after:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

State before:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply Finset.prod_congr rfl
State after:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = dpow (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)

State before:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dpow (Multiset.count x_1 ↑m) (x x_1) = dpow (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)
Tactic:
intro i hi
State after:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dpow (Multiset.count i ↑m) (x i) = dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)

State before:
case insert.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
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dpow (Multiset.count i ↑m) (x i) = dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply congr_arg₂ _ _ rfl
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 ι
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑m = Multiset.count i ↑(Sym.filterNe a m).snd

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_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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑m = Multiset.count i ↑(Sym.filterNe a m).snd
Tactic:
conv_lhs => rw [← Sym.fill_filterNe a m, Sym.coe_fill]
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 ι
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i (↑(Sym.filterNe a m).snd + ↑(Sym.replicate (↑(Sym.filterNe a m).fst) a)) =
    Multiset.count i ↑(Sym.filterNe a m).snd

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_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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i (↑(Sym.filterNe a m).snd + ↑(Sym.replicate (↑(Sym.filterNe a m).fst) a)) =
    Multiset.count i ↑(Sym.filterNe a m).snd
Tactic:
simp only [Multiset.count_add, add_right_eq_self, Multiset.count_eq_zero,
  Sym.mem_coe, Sym.mem_replicate, not_and]
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 ι
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ ↑(Sym.filterNe a m).fst ≠ 0 → ¬i = a

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_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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ ↑(Sym.filterNe a m).fst ≠ 0 → ¬i = a
Tactic:
exact fun _ => ne_of_mem_of_not_mem hi ha
State after:
no goals

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_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
⊢ ∀ (m : Sym ι n) (hm : m ∈ (insert a s).sym n),
    ((fun m x => Sym.filterNe a m) m hm).snd ∈ s.sym (n - ↑((fun m x => Sym.filterNe a m) m hm).fst)
Tactic:
intro m hm
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 ι
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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ((fun m x => Sym.filterNe a m) m hm).snd ∈ s.sym (n - ↑((fun m x => Sym.filterNe a m) m hm).fst)

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_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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ((fun m x => Sym.filterNe a m) m hm).snd ∈ s.sym (n - ↑((fun m x => Sym.filterNe a m) m hm).fst)
Tactic:
convert sym_filterNe_mem a hm
State after:
case h.e'_5.h.e'_3
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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = (insert a s).erase a

State before:
case h.e'_5.h.e'_3
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
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ s = (insert a s).erase a
Tactic:
rw [erase_insert ha]
State after:
no goals