[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
⊢ (fun l => List.toFinset (permutations l)) l = (fun l => List.toFinset (permutations l)) l'
[PROOFSTEP]
ext sl
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
sl : List α
⊢ sl ∈ (fun l => List.toFinset (permutations l)) l ↔ sl ∈ (fun l => List.toFinset (permutations l)) l'
[PROOFSTEP]
simp only [mem_permutations, List.mem_toFinset]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l l' : List α
h : l ~ l'
sl : List α
⊢ sl ~ l ↔ sl ~ l'
[PROOFSTEP]
exact ⟨fun hs => hs.trans h, fun hs => hs.trans h.symm⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
l : List α
⊢ l ∈ lists s ↔ s = Quotient.mk (isSetoid α) l
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
l a✝ : List α
⊢ l ∈ lists (Quotient.mk (isSetoid α) a✝) ↔ Quotient.mk (isSetoid α) a✝ = Quotient.mk (isSetoid α) l
[PROOFSTEP]
simpa using perm_comm
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l
[PROOFSTEP]
suffices (∃ a : Finset α, a.val = ↑l) ↔ l.Nodup by simpa
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
this : (∃ a, a.val = ↑l) ↔ Nodup l
⊢ (l ∈ Finset.biUnion (Finset.powerset Finset.univ) fun s => Multiset.lists s.val) ↔ Nodup l
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) ↔ Nodup l
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) → Nodup l
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
s : Finset α
hs : s.val = ↑l
⊢ Nodup l
[PROOFSTEP]
simpa [← Multiset.coe_nodup, ← hs] using s.nodup
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
⊢ Nodup l → ∃ a, a.val = ↑l
[PROOFSTEP]
intro hl
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
hl : Nodup l
⊢ ∃ a, a.val = ↑l
[PROOFSTEP]
refine' ⟨⟨↑l, hl⟩, _⟩
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
hl : Nodup l
⊢ { val := ↑l, nodup := hl }.val = ↑l
[PROOFSTEP]
simp


[GOAL]
α : Type v
inst✝ : Fintype α
⊢ Small.{w, v} α
[PROOFSTEP]
rw [small_congr (Fintype.equivFin α)]
[GOAL]
α : Type v
inst✝ : Fintype α
⊢ Small.{w, 0} (Fin (Fintype.card α))
[PROOFSTEP]
infer_instance


[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ multinomial ∅ f = 1
[PROOFSTEP]
dsimp [multinomial]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ 1 / 1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
⊢ multinomial {a} f = 1
[PROOFSTEP]
simp [multinomial, Nat.div_self (factorial_pos (f a))]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ multinomial (insert a s) f = succ (Finset.sum s f) * multinomial s f
[PROOFSTEP]
simp only [multinomial, one_mul, factorial]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ i in insert a s, f i)! / ∏ i in insert a s, (f i)! = succ (Finset.sum s f) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
[PROOFSTEP]
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / (1! * ∏ x in s, (f x)!) =
    succ (Finset.sum s f) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
[PROOFSTEP]
simp only [factorial_one, one_mul, Function.comp_apply, factorial, mul_one, ← one_eq_succ_zero]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
h₁ : f a = 1
⊢ (∑ x in s, f x + 1) * (∑ x in s, f x)! / ∏ x in s, (f x)! =
    succ (Finset.sum s f) * ((∑ x in s, f x)! / ∏ x in s, (f x)!)
[PROOFSTEP]
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = choose (f a + Finset.sum s f) (f a) * multinomial s f
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (le.intro rfl)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ multinomial (insert a s) f = (f a + Finset.sum s f)! / ((f a)! * (f a + Finset.sum s f - f a)!) * multinomial s f
[PROOFSTEP]
simp only [multinomial, Nat.add_sub_cancel_left, Finset.sum_insert h, Finset.prod_insert h, Function.comp_apply]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ (f a + ∑ i in s, f i)! / ((f a)! * ∏ i in s, (f i)!) =
    (f a + Finset.sum s f)! / ((f a)! * (Finset.sum s f)!) * ((∑ i in s, f i)! / ∏ i in s, (f i)!)
[PROOFSTEP]
rw [div_mul_div_comm ((f a).factorial_mul_factorial_dvd_factorial_add (s.sum f)) (prod_factorial_dvd_factorial_sum _ _),
  mul_comm (f a)! (s.sum f)!, mul_assoc, mul_comm _ (s.sum f)!, Nat.mul_div_mul_left _ _ (factorial_pos _)]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ multinomial s f = multinomial s g
[PROOFSTEP]
simp only [multinomial]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ (∑ i in s, f i)! / ∏ i in s, (f i)! = (∑ i in s, g i)! / ∏ i in s, (g i)!
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ (∑ i in s, f i)! = (∑ i in s, g i)!
[PROOFSTEP]
rw [Finset.sum_congr rfl h]
[GOAL]
case e_a
α : Type u_1
s : Finset α
f✝ : α → ℕ
a b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
⊢ ∏ i in s, (f i)! = ∏ i in s, (g i)!
[PROOFSTEP]
exact Finset.prod_congr rfl fun a ha => by rw [h a ha]
[GOAL]
α : Type u_1
s : Finset α
f✝ : α → ℕ
a✝ b : α
n : ℕ
f g : α → ℕ
h : ∀ (a : α), a ∈ s → f a = g a
a : α
ha : a ∈ s
⊢ (f a)! = (g a)!
[PROOFSTEP]
rw [h a ha]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)
[PROOFSTEP]
simp [multinomial, Finset.sum_pair h, Finset.prod_pair h]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = choose (f a + f b) (f a)
[PROOFSTEP]
simp [binomial_eq _ h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
hab : a ≠ b
⊢ (f a)! * (f b)! * multinomial {a, b} f = (f a + f b)!
[PROOFSTEP]
simpa [Finset.sum_pair hab, Finset.prod_pair hab] using multinomial_spec { a, b } f
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
h₁ : f a = 1
⊢ multinomial {a, b} f = succ (f b)
[PROOFSTEP]
simp [multinomial_insert_one { b } f (Finset.not_mem_singleton.mpr h) h₁]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (succ (f a))) b (succ (f b))) =
    multinomial {a, b} (Function.update f a (succ (f a))) + multinomial {a, b} (Function.update f b (succ (f b)))
[PROOFSTEP]
simp only [binomial_eq_choose, Function.update_apply, h, Ne.def, ite_true, ite_false]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + if b = a then succ (f a) else f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
rw [if_neg h.symm]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
rw [add_succ, choose_succ_succ, succ_add_eq_succ_add]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ succ (f a + f b) * multinomial {a, b} f = succ (f a) * multinomial {a, b} (Function.update f a (succ (f a)))
[PROOFSTEP]
rw [binomial_eq_choose _ h, binomial_eq_choose _ h, mul_comm (f a).succ, Function.update_same,
  Function.update_noteq (ne_comm.mp h)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ succ (f a + f b) * choose (f a + f b) (f a) = choose (succ (f a) + f b) (succ (f a)) * succ (f a)
[PROOFSTEP]
rw [succ_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b : ℕ
⊢ multinomial Finset.univ ![a, b] = (a + b)! / (a ! * b !)
[PROOFSTEP]
rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
[PROOFSTEP]
rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ (Matrix.vecCons a ![b, c] 0 + Matrix.vecCons a ![b, c] 1 + Matrix.vecCons a ![b, c] 2)! /
      ((Matrix.vecCons a ![b, c] 0)! * (Matrix.vecCons a ![b, c] 1)! * (Matrix.vecCons a ![b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ multinomial f = choose (sum f fun x => id) (↑f a) * multinomial (update f a 0)
[PROOFSTEP]
simp only [multinomial_eq]
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
classical
by_cases a ∈ f.support
· rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _), Finset.add_sum_erase _ f h,
    support_update_zero]
  congr 1
  exact Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm
rw [not_mem_support_iff] at h
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
by_cases a ∈ f.support
[GOAL]
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
by_cases a ∈ f.support
[GOAL]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _), Finset.add_sum_erase _ f h,
  support_update_zero]
[GOAL]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ choose (∑ x in f.support, ↑f x) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
[PROOFSTEP]
congr 1
[GOAL]
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (Finset.erase f.support a) ↑f = Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
[PROOFSTEP]
exact Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm
[GOAL]
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ¬a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [not_mem_support_iff] at h
[GOAL]
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ↑f a = 0
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
[PROOFSTEP]
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ multinomial m = Nat.choose (↑card m) (count a m) * multinomial (filter ((fun x x_1 => x ≠ x_1) a) m)
[PROOFSTEP]
dsimp only [multinomial]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial (↑toFinsupp m) =
    Nat.choose (↑card m) (count a m) * Finsupp.multinomial (↑toFinsupp (filter (fun x => a ≠ x) m))
[PROOFSTEP]
convert Finsupp.multinomial_update a _
[GOAL]
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑card m = Finsupp.sum (↑toFinsupp m) fun x => id
[PROOFSTEP]
rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
[GOAL]
case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑toFinsupp (filter (fun x => a ≠ x) m) = Finsupp.update (↑toFinsupp m) a 0
[PROOFSTEP]
ext1 a
[GOAL]
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ ↑(↑toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ↑(Finsupp.update (↑toFinsupp m) a✝ 0) a
[PROOFSTEP]
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
[GOAL]
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
rw [Function.update_noteq h.symm, toFinsupp_apply]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (↑(↑toFinsupp m)) a✝ 0 a
[PROOFSTEP]
rw [not_ne_iff.1 h, Function.update_same]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
induction' s using Finset.induction with a s ha ih
[GOAL]
case empty
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum ∅ x ^ n =
      ∑ k : { x // x ∈ Finset.sym ∅ n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [sum_empty]
[GOAL]
case empty
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    0 ^ n =
      ∑ k : { x // x ∈ Finset.sym ∅ n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rintro
  (_ | n)
      -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
⊢ 0 ^ zero =
    ∑ k : { x // x ∈ Finset.sym ∅ zero },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
haveI : Subsingleton (Sym α 0) := Unique.instSubsingleton
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 0 ^ zero =
    ∑ k : { x // x ∈ Finset.sym ∅ zero },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [_root_.pow_zero, Fintype.sum_subsingleton]
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 1 =
    ↑(Multiset.multinomial ↑↑?empty.zero.a) *
      Multiset.noncommProd (Multiset.map x ↑↑?empty.zero.a)
        (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑?empty.zero.a} Commute)
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
swap
  -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
have : Zero (Sym α 0) := Sym.instZeroSym
[GOAL]
case empty.zero.a
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this✝ : Subsingleton (Sym α 0)
this : Zero (Sym α 0)
⊢ { x // x ∈ Finset.sym ∅ zero }
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this✝ : Subsingleton (Sym α 0)
this : Zero (Sym α 0)
⊢ 0 ∈ Finset.sym ∅ zero
[PROOFSTEP]
simp
[GOAL]
case empty.zero
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ 1 =
    ↑(Multiset.multinomial
          ↑↑(let_fun this_1 := Sym.instZeroSym;
              { val := 0, property := (_ : 0 ∈ {∅}) })) *
      Multiset.noncommProd
        (Multiset.map x
          ↑↑(let_fun this_1 := Sym.instZeroSym;
              { val := 0, property := (_ : 0 ∈ {∅}) }))
        (_ :
          Set.Pairwise
            {b |
              b ∈
                Multiset.map x
                  ↑↑(let_fun this_1 := Sym.instZeroSym;
                      { val := 0, property := (_ : 0 ∈ {∅}) })}
            Commute)
[PROOFSTEP]
convert (@one_mul R _ _).symm
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ ↑(Multiset.multinomial
        ↑↑(let_fun this_1 := Sym.instZeroSym;
            { val := 0, property := (_ : 0 ∈ {∅}) })) =
    1
[PROOFSTEP]
dsimp only
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
this : Subsingleton (Sym α 0)
⊢ ↑(Multiset.multinomial ↑0) = 1
[PROOFSTEP]
convert @Nat.cast_one R _
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
⊢ 0 ^ succ n =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [_root_.pow_succ, zero_mul]
  -- Porting note : Lean cannot infer this instance by itself
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
⊢ 0 =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
haveI : IsEmpty (Finset.sym (∅ : Finset α) (succ n)) := Finset.instIsEmpty
[GOAL]
case empty.succ
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s fun i j => Commute (x i) (x j)
hc : Set.Pairwise ↑∅ fun i j => Commute (x i) (x j)
n : ℕ
this : IsEmpty { x // x ∈ Finset.sym ∅ (succ n) }
⊢ 0 =
    ∑ k : { x // x ∈ Finset.sym ∅ (succ n) },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
apply (Fintype.sum_empty _).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
ih :
  ∀ (hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)) (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
⊢ ∀ (n : ℕ),
    Finset.sum (insert a s) x ^ n =
      ∑ k : { x // x ∈ Finset.sym (insert a s) n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
intro n
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
ih :
  ∀ (hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)) (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
⊢ Finset.sum (insert a s) x ^ n =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
specialize ih (hc.mono <| s.subset_insert a)
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ Finset.sum (insert a s) x ^ n =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ i : Fin (n + 1), x a ^ ↑i * (∑ i in s, x i) ^ (n - ↑i) * ↑(Nat.choose n ↑i) =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∀ (i : α), i ∈ s → Commute (x a) (x i)
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∀ (i : α), i ∈ s → Commute (x a) (x i)
[PROOFSTEP]
exact fun _ hb => hc (mem_insert_self a s) (mem_insert_of_mem hb) (ne_of_mem_of_not_mem hb ha).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ i : Fin (n + 1), x a ^ ↑i * (∑ i in s, x i) ^ (n - ↑i) * ↑(Nat.choose n ↑i) =
    ∑ k : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑k) *
        Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
[PROOFSTEP]
simp_rw [ih, mul_sum, sum_mul, sum_sigma', univ_sigma_univ]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
⊢ ∑ x_1 : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) },
      x a ^ ↑x_1.fst *
          (↑(Multiset.multinomial ↑↑x_1.snd) *
            Multiset.noncommProd (Multiset.map x ↑↑x_1.snd)
              (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x_1.snd} Commute)) *
        ↑(Nat.choose n ↑x_1.fst) =
    ∑ x_1 : { x // x ∈ Finset.sym (insert a s) n },
      ↑(Multiset.multinomial ↑↑x_1) *
        Multiset.noncommProd (Multiset.map x ↑↑x_1) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x_1} Commute)
[PROOFSTEP]
refine' (Fintype.sum_equiv (symInsertEquiv ha) _ _ fun m => _).symm
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial ↑↑m) *
      Multiset.noncommProd (Multiset.map x ↑↑m) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑m} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [m.1.1.multinomial_filter_ne a]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose (↑Multiset.card ↑↑m) (Multiset.count a ↑↑m) *
          Multiset.multinomial (Multiset.filter ((fun x x_1 => x ≠ x_1) a) ↑↑m)) *
      Multiset.noncommProd (Multiset.map x ↑↑m) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑m} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
conv in m.1.1.map _ => rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
| Multiset.map x ↑↑m
[PROOFSTEP]
rw [← m.1.1.filter_add_not ((· = ·) a), Multiset.map_add]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose (↑Multiset.card ↑↑m) (Multiset.count a ↑↑m) *
          Multiset.multinomial (Multiset.filter ((fun x x_1 => x ≠ x_1) a) ↑↑m)) *
      Multiset.noncommProd
        (Multiset.map x (Multiset.filter ((fun x x_1 => x = x_1) a) ↑↑m) +
          Multiset.map x (Multiset.filter (fun a_1 => ¬(fun x x_1 => x = x_1) a a_1) ↑↑m))
        (_ :
          Set.Pairwise
            {x_1 |
              x_1 ∈
                Multiset.map x (Multiset.filter ((fun x x_2 => x = x_2) a) ↑↑m) +
                  Multiset.map x (Multiset.filter (fun a_1 => ¬(fun x x_2 => x = x_2) a a_1) ↑↑m)}
            Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
simp_rw [Multiset.noncommProd_add, m.1.1.filter_eq, Multiset.map_replicate, m.1.2]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose n (Multiset.count a ↑↑m) * Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (Multiset.noncommProd (Multiset.replicate (Multiset.count a ↑↑m) (x a))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.replicate (Multiset.count a ↑↑m) (x a)} Commute) *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [Multiset.noncommProd_eq_pow_card _ _ _ fun _ => Multiset.eq_of_mem_replicate]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Nat.choose n (Multiset.count a ↑↑m) * Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (x a ^ ↑Multiset.card (Multiset.replicate (Multiset.count a ↑↑m) (x a)) *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
rw [Multiset.card_replicate, Nat.cast_mul, mul_assoc, Nat.cast_comm]
[GOAL]
case insert
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
        (x a ^ Multiset.count a ↑↑m *
          Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
            (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) *
      ↑(Nat.choose n (Multiset.count a ↑↑m)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
        (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
          Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
            (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)) *
      ↑(Nat.choose n ↑(↑(symInsertEquiv ha) m).fst)
[PROOFSTEP]
congr 1
[GOAL]
case insert.e_a
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      (x a ^ Multiset.count a ↑↑m *
        Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
          (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute)) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst *
      (↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
        Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
          (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute))
[PROOFSTEP]
simp_rw [← mul_assoc, Nat.cast_comm]
[GOAL]
case insert.e_a
α : Type u_1
inst✝¹ : DecidableEq α
s✝ : Finset α
R : Type u_2
inst✝ : Semiring R
x : α → R
hc✝ : Set.Pairwise ↑s✝ fun i j => Commute (x i) (x j)
a : α
s : Finset α
ha : ¬a ∈ s
hc : Set.Pairwise ↑(insert a s) fun i j => Commute (x i) (x j)
n : ℕ
ih :
  ∀ (n : ℕ),
    Finset.sum s x ^ n =
      ∑ k : { x // x ∈ Finset.sym s n },
        ↑(Multiset.multinomial ↑↑k) *
          Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ x a ^ Multiset.count a ↑↑m * ↑(Multiset.multinomial (Multiset.filter (fun x => a ≠ x) ↑↑m)) *
      Multiset.noncommProd (Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m))
        (_ : Set.Pairwise {x_1 | x_1 ∈ Multiset.map x (Multiset.filter (fun a_1 => ¬a = a_1) ↑↑m)} Commute) =
    x a ^ ↑(↑(symInsertEquiv ha) m).fst * ↑(Multiset.multinomial ↑↑(↑(symInsertEquiv ha) m).snd) *
      Multiset.noncommProd (Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd)
        (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑(↑(symInsertEquiv ha) m).snd} Commute)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
⊢ Finset.sum s x ^ n = ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
conv_rhs => rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
| ∑ k in Finset.sym s n, ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)
[PROOFSTEP]
rw [← sum_coe_sort]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
⊢ Finset.sum s x ^ n =
    ∑ i : { x // x ∈ Finset.sym s n }, ↑(Multiset.multinomial ↑↑i) * Multiset.prod (Multiset.map x ↑↑i)
[PROOFSTEP]
convert sum_pow_of_commute s x (fun _ _ _ _ _ => mul_comm _ _) n
[GOAL]
case h.e'_3.a.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
R : Type u_2
inst✝ : CommSemiring R
x : α → R
n : ℕ
x✝ : { x // x ∈ Finset.sym s n }
a✝ : x✝ ∈ univ
⊢ Multiset.prod (Multiset.map x ↑↑x✝) =
    Multiset.noncommProd (Multiset.map x ↑↑x✝) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑x✝} Commute)
[PROOFSTEP]
rw [Multiset.noncommProd_eq_prod]


[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
[PROOFSTEP]
let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * choose n m
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
⊢ (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
[PROOFSTEP]
change (x + y) ^ n = ∑ m in range (n + 1), t n m
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
  simp only [choose_zero_right, _root_.pow_zero, Nat.cast_one, mul_one, one_mul, tsub_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
n : ℕ
⊢ t n 0 = y ^ n
[PROOFSTEP]
simp only [choose_zero_right, _root_.pow_zero, Nat.cast_one, mul_one, one_mul, tsub_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by simp only [ge_iff_le, choose_succ_self, cast_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
n : ℕ
⊢ t n (succ n) = 0
[PROOFSTEP]
simp only [ge_iff_le, choose_succ_self, cast_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
have h_middle : ∀ n i : ℕ, i ∈ range n.succ → (t n.succ ∘ Nat.succ) i = x * t n i + y * t n i.succ :=
  by
  intro n i h_mem
  have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
  dsimp only
  rw [Function.comp_apply, choose_succ_succ, Nat.cast_add, mul_add]
  congr 1
  · rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
  · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
    by_cases h_eq : i = n
    · rw [h_eq, choose_succ_self, Nat.cast_zero, mul_zero, mul_zero]
    · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
      rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
⊢ ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
intro n i h_mem
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
⊢ (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
have h_le : i ≤ n := Nat.le_of_lt_succ (mem_range.mp h_mem)
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ ((fun m => x ^ m * y ^ (succ n - m) * ↑(Nat.choose (succ n) m)) ∘ succ) i =
    x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i)) + y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
rw [Function.comp_apply, choose_succ_succ, Nat.cast_add, mul_add]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n i) +
      x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i)) + y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n i) = x * (x ^ i * y ^ (n - i) * ↑(Nat.choose n i))
[PROOFSTEP]
rw [pow_succ x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    y * (x ^ succ i * y ^ (n - succ i) * ↑(Nat.choose n (succ i)))
[PROOFSTEP]
rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
by_cases h_eq : i = n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : i = n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [h_eq, choose_succ_self, Nat.cast_zero, mul_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ succ i * y ^ (succ n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
n i : ℕ
h_mem : i ∈ range (succ n)
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ succ i * y ^ succ (n - succ i) * ↑(Nat.choose n (succ i)) =
    x ^ succ i * y * y ^ (n - succ i) * ↑(Nat.choose n (succ i))
[PROOFSTEP]
rw [pow_succ y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ (x + y) ^ n = ∑ m in range (n + 1), t n m
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ (x + y) ^ zero = ∑ m in range (zero + 1), t zero m
[PROOFSTEP]
rw [_root_.pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ 1 = t zero zero
[PROOFSTEP]
dsimp only
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
⊢ 1 = x ^ zero * y ^ (zero - zero) * ↑(Nat.choose zero zero)
[PROOFSTEP]
rw [_root_.pow_zero, _root_.pow_zero, choose_self, Nat.cast_one, mul_one, mul_one]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ m in range (succ n + 1), t (succ n) m
[PROOFSTEP]
rw [sum_range_succ', h_first]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ k in range (n + 1), t (succ n) (k + 1) + y ^ succ n
[PROOFSTEP]
erw [sum_congr rfl (h_middle n), sum_add_distrib, add_assoc]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ (x + y) ^ succ n = ∑ x_1 in range (succ n), x * t n x_1 + (∑ x in range (succ n), y * t n (succ x) + y ^ succ n)
[PROOFSTEP]
rw [pow_succ (x + y), ih, add_mul, mul_sum, mul_sum]
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ ∑ x_1 in range (n + 1), x * t n x_1 + ∑ x in range (n + 1), y * t n x =
    ∑ x_1 in range (succ n), x * t n x_1 + (∑ x in range (succ n), y * t n (succ x) + y ^ succ n)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(Nat.choose n m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n (succ n) = 0
h_middle : ∀ (n i : ℕ), i ∈ range (succ n) → (t (succ n) ∘ succ) i = x * t n i + y * t n (succ i)
n : ℕ
ih : (x + y) ^ n = ∑ m in range (n + 1), t n m
⊢ ∑ x in range (n + 1), y * t n x = ∑ x in range (succ n), y * t n (succ x) + y ^ succ n
[PROOFSTEP]
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ]
[GOAL]
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m in Nat.antidiagonal n, Nat.choose n m.fst • (x ^ m.fst * y ^ m.snd)
[PROOFSTEP]
simp_rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ choose n m • (x ^ m * y ^ p), _root_.nsmul_eq_mul,
  cast_comm, h.add_pow]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
[PROOFSTEP]
have := (add_pow 1 1 n).symm
[GOAL]
R : Type u_1
n : ℕ
this : ∑ m in range (n + 1), 1 ^ m * 1 ^ (n - m) * ↑(choose n m) = (1 + 1) ^ n
⊢ ∑ m in range (n + 1), choose n m = 2 ^ n
[PROOFSTEP]
simpa [one_add_one_eq_two] using this
[GOAL]
R : Type u_1
m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1
[PROOFSTEP]
linarith [mem_range.1 hi]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * ∑ i in range (m + 1), choose (2 * m + 1) i =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i)
[PROOFSTEP]
rw [two_mul, this]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
{ rw [range_eq_Ico, sum_Ico_reflect]
  · congr
    have A : m + 1 ≤ 2 * m + 1 := by linarith
    rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
    congr
    rw [tsub_eq_iff_eq_add_of_le A]
    ring
  · linarith
}
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) =
    ∑ i in range (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
rw [range_eq_Ico, sum_Ico_reflect]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i +
      ∑ j in Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), choose (2 * m + 1) j =
    ∑ i in Ico 0 (m + 1), choose (2 * m + 1) i + ∑ i in Ico (m + 1) (2 * m + 2), choose (2 * m + 1) i
[PROOFSTEP]
congr
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
[PROOFSTEP]
have A : m + 1 ≤ 2 * m + 1 := by linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1
[PROOFSTEP]
linarith
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1
[PROOFSTEP]
rw [add_comm, add_tsub_assoc_of_le A, ← add_comm]
[GOAL]
case e_a.e_s.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) + 1 = m + 1
[PROOFSTEP]
congr
[GOAL]
case e_a.e_s.e_a.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 - (m + 1) = m
[PROOFSTEP]
rw [tsub_eq_iff_eq_add_of_le A]
[GOAL]
case e_a.e_s.e_a.e_a
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
A : m + 1 ≤ 2 * m + 1
⊢ 2 * m + 1 = m + (m + 1)
[PROOFSTEP]
ring
[GOAL]
case h
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 1 + 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ m + 1 ≤ 2 * m + 2
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m
[PROOFSTEP]
rw [pow_succ, pow_mul, mul_comm]
[GOAL]
R : Type u_1
m : ℕ
this : ∑ i in range (m + 1), choose (2 * m + 1) (2 * m + 1 - i) = ∑ i in range (m + 1), choose (2 * m + 1) i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
n : ℕ
⊢ choose (2 * n + 1) n ≤ 4 ^ n
[PROOFSTEP]
have t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i :=
  single_le_sum (fun x _ ↦ by linarith) (self_mem_range_succ n)
[GOAL]
R : Type u_1
n x : ℕ
x✝ : x ∈ range (n + 1)
⊢ 0 ≤ choose (2 * n + 1) x
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
n : ℕ
t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i
⊢ choose (2 * n + 1) n ≤ 4 ^ n
[PROOFSTEP]
simpa [sum_range_choose_halfway n] using t
[GOAL]
R : Type u_1
n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)
[PROOFSTEP]
simp only [pow_mul, one_add_one_eq_two]
[GOAL]
R : Type u_1
n : ℕ
⊢ 4 ^ n = (2 ^ 2) ^ n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
n : ℕ
⊢ (1 + 1) ^ (2 * n) = ∑ m in range (2 * n + 1), choose (2 * n) m
[PROOFSTEP]
simp [add_pow]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (2 * n + 1), choose (2 * n) m ≤ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2)
[PROOFSTEP]
gcongr
[GOAL]
case h
R : Type u_1
n i✝ : ℕ
a✝ : i✝ ∈ range (2 * n + 1)
⊢ choose (2 * n) i✝ ≤ choose (2 * n) (2 * n / 2)
[PROOFSTEP]
apply choose_le_middle
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2) = (2 * n + 1) * choose (2 * n) n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (n + 1), (-1) ^ m * ↑(Nat.choose n m) = if n = 0 then 1 else 0
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u_1
⊢ ∑ m in range (zero + 1), (-1) ^ m * ↑(Nat.choose zero m) = if zero = 0 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
n✝ : ℕ
⊢ ∑ m in range (Nat.succ n✝ + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n✝) m) = if Nat.succ n✝ = 0 then 1 else 0
[PROOFSTEP]
case succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, add_left_neg] at h
  rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
case succ n =>
  have h := add_pow (-1 : ℤ) 1 n.succ
  simp only [one_pow, mul_one, add_left_neg] at h
  rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
have h := add_pow (-1 : ℤ) 1 n.succ
[GOAL]
R : Type u_1
n : ℕ
h :
  (-1 + 1) ^ Nat.succ n = ∑ m in range (Nat.succ n + 1), (-1) ^ m * 1 ^ (Nat.succ n - m) * ↑(Nat.choose (Nat.succ n) m)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
simp only [one_pow, mul_one, add_left_neg] at h
[GOAL]
R : Type u_1
n : ℕ
h : 0 ^ Nat.succ n = ∑ x in range (Nat.succ n + 1), (-1) ^ x * ↑(Nat.choose (Nat.succ n) x)
⊢ ∑ m in range (Nat.succ n + 1), (-1) ^ m * ↑(Nat.choose (Nat.succ n) m) = if Nat.succ n = 0 then 1 else 0
[PROOFSTEP]
rw [← h, zero_pow (Nat.succ_pos n), if_neg (Nat.succ_ne_zero n)]
[GOAL]
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ ∑ m in range (n + 1), (-1) ^ m * ↑(Nat.choose n m) = 0
[PROOFSTEP]
rw [Int.alternating_sum_range_choose, if_neg h0]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) = ∑ m in range (card x + 1), Nat.choose (card x) m • f m
[PROOFSTEP]
trans ∑ m in range (x.card + 1), ∑ j in x.powerset.filter fun z ↦ z.card = m, f j.card
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) =
    ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j)
[PROOFSTEP]
refine' (sum_fiberwise_of_maps_to _ _).symm
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ (x_1 : Finset β), x_1 ∈ powerset x → card x_1 ∈ range (card x + 1)
[PROOFSTEP]
intro y hy
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ∈ range (card x + 1)
[PROOFSTEP]
rw [mem_range, Nat.lt_succ_iff]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ≤ card x
[PROOFSTEP]
rw [mem_powerset] at hy
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ card y ≤ card x
[PROOFSTEP]
exact card_le_of_subset hy
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j) =
    ∑ m in range (card x + 1), Nat.choose (card x) m • f m
[PROOFSTEP]
refine' sum_congr rfl fun y _ ↦ _
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = Nat.choose (card x) y • f y
[PROOFSTEP]
rw [← card_powersetLen, ← sum_const]
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = ∑ _x in powersetLen y x, f y
[PROOFSTEP]
refine' sum_congr powersetLen_eq_filter.symm fun z hz ↦ _
[GOAL]
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
z : Finset β
hz : z ∈ powersetLen y x
⊢ f (card z) = f y
[PROOFSTEP]
rw [(mem_powersetLen.1 hz).2]
[GOAL]
R : Type u_1
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in powerset x, (-1) ^ card m = if x = ∅ then 1 else 0
[PROOFSTEP]
rw [sum_powerset_apply_card]
[GOAL]
R : Type u_1
α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m in range (card x + 1), Nat.choose (card x) m • (-1) ^ m = if x = ∅ then 1 else 0
[PROOFSTEP]
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]
[GOAL]
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
[PROOFSTEP]
classical
rw [sum_powerset_neg_one_pow_card, if_neg]
rw [← Ne.def, ← nonempty_iff_ne_empty]
apply h0
[GOAL]
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
[PROOFSTEP]
rw [sum_powerset_neg_one_pow_card, if_neg]
[GOAL]
case hnc
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ ¬x = ∅
[PROOFSTEP]
rw [← Ne.def, ← nonempty_iff_ne_empty]
[GOAL]
case hnc
R : Type u_1
α : Type u_2
x : Finset α
h0 : Finset.Nonempty x
⊢ Finset.Nonempty x
[PROOFSTEP]
apply h0
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
have A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ (n.choose i)
[GOAL]
case A
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
[PROOFSTEP]
rw [prod_range_succ, prod_range_succ']
[GOAL]
case A
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x in range n, f (x + 1) (n - x) ^ Nat.choose n (x + 1)) * f (n + 1) (n - n) ^ Nat.choose n (n + 1) * f 0 (n + 1) =
    (∏ k in range n, f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose n (k + 1)) * f 0 (n + 1 - 0) ^ Nat.choose n 0
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ ∏ i in range (n + 2), f i (n + 1 - i) ^ Nat.choose (n + 1) i =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
rw [prod_range_succ']
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n (i + 1)) * f 0 (n + 1) =
    ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i
⊢ (∏ k in range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ Nat.choose (n + 1) (k + 1)) *
      f 0 (n + 1 - 0) ^ Nat.choose (n + 1) 0 =
    (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i
[PROOFSTEP]
simpa [Nat.choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using
  mul_comm _
    _
      -- porting note: new lemma
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij in Nat.antidiagonal (n + 1), f ij.fst ij.snd ^ Nat.choose (n + 1) ij.fst =
    (∏ ij in Nat.antidiagonal n, f ij.fst (ij.snd + 1) ^ Nat.choose n ij.fst) *
      ∏ ij in Nat.antidiagonal n, f (ij.fst + 1) ij.snd ^ Nat.choose n ij.snd
[PROOFSTEP]
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n
[PROOFSTEP]
simpa [Nat.lt_succ_iff] using hi
[GOAL]
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ (∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i) * ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    (∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x) *
      ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f i (n + 1 - i) ^ Nat.choose n i = ∏ x in range (succ n), f x (n - x + 1) ^ Nat.choose n x
[PROOFSTEP]
refine prod_congr rfl fun i hi ↦ ?_
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f i (n + 1 - i) ^ Nat.choose n i = f i (n - i + 1) ^ Nat.choose n i
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (this _ hi)]
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
⊢ ∏ i in range (n + 1), f (i + 1) (n - i) ^ Nat.choose n i =
    ∏ x in range (succ n), f (x + 1) (n - x) ^ Nat.choose n (n - x)
[PROOFSTEP]
refine prod_congr rfl fun i hi ↦ ?_
[GOAL]
case e_a
R✝ : Type u_1
M✝ : Type u_2
R : Type u_3
inst✝² : CommMonoid M✝
inst✝¹ : NonAssocSemiring R
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ (i : ℕ), i ∈ range (n + 1) → i ≤ n
i : ℕ
hi : i ∈ range (succ n)
⊢ f (i + 1) (n - i) ^ Nat.choose n i = f (i + 1) (n - i) ^ Nat.choose n (n - i)
[PROOFSTEP]
rw [Nat.choose_symm (this _ hi)]
  -- porting note: moved from `Mathlib.Analysis.Calculus.ContDiff`
[GOAL]
R✝ : Type u_1
M : Type u_2
R : Type u_3
inst✝¹ : CommMonoid M
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i in range (n + 2), ↑(Nat.choose (n + 1) i) * f i (n + 1 - i) =
    ∑ i in range (n + 1), ↑(Nat.choose n i) * f i (n + 1 - i) +
      ∑ i in range (n + 1), ↑(Nat.choose n i) * f (i + 1) (n - i)
[PROOFSTEP]
simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n
[GOAL]
R✝ : Type u_1
M : Type u_2
R : Type u_3
inst✝¹ : CommMonoid M
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij in Nat.antidiagonal (n + 1), ↑(Nat.choose (n + 1) ij.fst) * f ij.fst ij.snd =
    ∑ ij in Nat.antidiagonal n, ↑(Nat.choose n ij.fst) * f ij.fst (ij.snd + 1) +
      ∑ ij in Nat.antidiagonal n, ↑(Nat.choose n ij.snd) * f (ij.fst + 1) ij.snd
[PROOFSTEP]
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : Bool → α
⊢ ∏ b : Bool, f b = f true * f false
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i : ι, if i ∈ s then f i else 1) = ∏ i in s, f i
[PROOFSTEP]
rw [← prod_filter, filter_mem_eq_inter, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x : α, f x = f a * f b
[PROOFSTEP]
apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ¬a ∈ Finset.univ → f a = 1
[PROOFSTEP]
exact fun hc => (hc (Finset.mem_univ _)).elim
[GOAL]
case hb
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ¬b ∈ Finset.univ → f b = 1
[PROOFSTEP]
exact fun hc => (hc (Finset.mem_univ _)).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
⊢ Finset.card (piFinset t) = ∏ a : α, Finset.card (t a)
[PROOFSTEP]
simp [Fintype.piFinset, card_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α
[PROOFSTEP]
rw [Fintype.card_pi, Finset.prod_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card β ^ Finset.card univ = card β ^ card α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Vector α n) = Fintype.card α ^ n
[PROOFSTEP]
rw [Fintype.ofEquiv_card]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : CommMonoid β
f : { a // a ∈ univ } → β
x : { x // x ∈ univ }
⊢ f x =
    f
      { val := ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x,
        property := (_ : ↑(Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ∈ univ)) x ∈ univ) }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∏ x in pi univ t, f x = ∏ x in Fintype.piFinset t, f fun a x_1 => x a
[PROOFSTEP]
refine
  prod_bij (fun x _ a => x a (mem_univ _)) ?_ (by simp)
    (by simp (config := { contextual := true }) [Function.funext_iff]) fun x hx =>
    ⟨fun a _ => x a, by simp_all⟩
      -- Porting note: old proof was `by simp`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t),
    f a = f fun a_1 x => (fun x x_1 a => x a (_ : a ∈ univ)) a ha a_1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a₁ a₂ : (a : α) → a ∈ univ → δ a) (ha₁ : a₁ ∈ pi univ t) (ha₂ : a₂ ∈ pi univ t),
    (fun x x_1 a => x a (_ : a ∈ univ)) a₁ ha₁ = (fun x x_1 a => x a (_ : a ∈ univ)) a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
simp (config := { contextual := true }) [Function.funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
x : (a : α) → δ a
hx : x ∈ Fintype.piFinset t
⊢ ∃ ha, x = (fun x x_1 a => x a (_ : a ∈ univ)) (fun a x_1 => x a) ha
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
⊢ ∀ (a : (a : α) → a ∈ univ → δ a) (ha : a ∈ pi univ t), (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
[PROOFSTEP]
intro a ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun x x_1 a => x a (_ : a ∈ univ)) a ha ∈ Fintype.piFinset t
[PROOFSTEP]
simp only [Fintype.piFinset, mem_map, mem_pi, Function.Embedding.coeFn_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∃ a_1, (∀ (a : α) (h : a ∈ univ), a_1 a h ∈ t a) ∧ (fun a => a_1 a (_ : a ∈ univ)) = fun a_2 => a a_2 (_ : a_2 ∈ univ)
[PROOFSTEP]
exact ⟨a, by simpa using ha, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ ∀ (a_1 : α) (h : a_1 ∈ univ), a a_1 h ∈ t a_1
[PROOFSTEP]
simpa using ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : CommMonoid β
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : ((a : α) → a ∈ univ → δ a) → β
a : (a : α) → a ∈ univ → δ a
ha : a ∈ pi univ t
⊢ (fun a_1 => a a_1 (_ : a_1 ∈ univ)) = fun a_1 => a a_1 (_ : a_1 ∈ univ)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : CommSemiring β
δ : α → Type u_1
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
f : (a : α) → δ a → β
⊢ ∏ a : α, ∑ b in t a, f a b = ∑ p in Fintype.piFinset t, ∏ x : α, f x (p x)
[PROOFSTEP]
simp only [Finset.prod_attach_univ, prod_sum, Finset.sum_univ_pi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (i : Fin n), f ↑i = f ↑(↑(equivSubtype.trans (Equiv.subtypeEquivRight (_ : ∀ (a : ℕ), a < n ↔ a ∈ range n))) i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∏ i : { x // x ∈ range n }, f ↑i = ∏ i in range n, f i
[PROOFSTEP]
rw [← attach_eq_univ, prod_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i : Fin n, c i = ∏ i in range n, if h : i < n then c { val := i, isLt := h } else 1
[PROOFSTEP]
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ (x : Fin n), x ∈ univ → c x = if h : ↑x < n then c { val := ↑x, isLt := h } else 1
[PROOFSTEP]
rintro ⟨i, hi⟩ _
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : { val := i, isLt := hi } ∈ univ
⊢ c { val := i, isLt := hi } =
    if h : ↑{ val := i, isLt := hi } < n then c { val := ↑{ val := i, isLt := hi }, isLt := h } else 1
[PROOFSTEP]
simp only [hi, dif_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a in Set.toFinset {x | p x}, f a = ∏ a : Subtype p, f ↑a
[PROOFSTEP]
rw [← Finset.prod_subtype]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ Set.toFinset {x | p x} ↔ p x
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
[PROOFSTEP]
intro
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a = ∏ a : α, g a
[PROOFSTEP]
rw [← (Equiv.sigmaFiberEquiv f).prod_comp, ← univ_sigma_univ, prod_sigma]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
inst✝ : CommMonoid γ
f : α → β
g : α → γ
⊢ ∏ b : β, ∏ a : { a // f a = b }, g ↑a =
    ∏ a : β, ∏ s : { x // f x = a }, g (↑(Equiv.sigmaFiberEquiv f) { fst := a, snd := s })
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
simp only [prod_dite, attach_eq_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x)) *
      ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) =
    (∏ a : { a // p a }, f ↑a (_ : p ↑a)) * ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x (_ : p ↑x) = ∏ a : { a // p a }, f ↑a (_ : p ↑a)
[PROOFSTEP]
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // p x } => f x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x
[PROOFSTEP]
simp
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x (_ : ¬p ↑x) = ∏ a : { a // ¬p a }, g ↑a (_ : ¬p ↑a)
[PROOFSTEP]
exact (Equiv.subtypeEquivRight $ by simp).prod_comp fun x : { x // ¬p x } => g x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => ¬p x) univ ↔ ¬p x
[PROOFSTEP]
simp


[GOAL]
r : ℝ
hr : r < 0
⊢ sign r = -1
[PROOFSTEP]
rw [sign, if_pos hr]
[GOAL]
r : ℝ
hr : 0 < r
⊢ sign r = 1
[PROOFSTEP]
rw [sign, if_pos hr, if_neg hr.not_lt]
[GOAL]
⊢ sign 0 = 0
[PROOFSTEP]
rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]
[GOAL]
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
r : ℝ
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
exact Or.inl <| sign_of_neg hn
[GOAL]
case inr.inl
⊢ sign 0 = -1 ∨ sign 0 = 0 ∨ sign 0 = 1
[PROOFSTEP]
exact Or.inr <| Or.inl <| sign_zero
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r = -1 ∨ sign r = 0 ∨ sign r = 1
[PROOFSTEP]
exact Or.inr <| Or.inr <| sign_of_pos hp
[GOAL]
r : ℝ
⊢ sign r = 0 ↔ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
[GOAL]
r : ℝ
h : sign r = 0
⊢ r = 0
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
h : sign r = 0
hn : r < 0
⊢ r = 0
[PROOFSTEP]
rw [sign_of_neg hn, neg_eq_zero] at h
[GOAL]
case inl
r : ℝ
h : 1 = 0
hn : r < 0
⊢ r = 0
[PROOFSTEP]
exact (one_ne_zero h).elim
[GOAL]
case inr.inl
h : sign 0 = 0
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
r : ℝ
h : sign r = 0
hp : 0 < r
⊢ r = 0
[PROOFSTEP]
rw [sign_of_pos hp] at h
[GOAL]
case inr.inr
r : ℝ
h : 1 = 0
hp : 0 < r
⊢ r = 0
[PROOFSTEP]
exact (one_ne_zero h).elim
[GOAL]
z : ℤ
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy z (0 : ℤ)
[GOAL]
case inl
z : ℤ
hn : z < 0
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
rw [sign_of_neg (Int.cast_lt_zero.mpr hn), Int.sign_eq_neg_one_of_neg hn, Int.cast_neg, Int.cast_one]
[GOAL]
case inr.inl
⊢ sign ↑0 = ↑(Int.sign 0)
[PROOFSTEP]
rw [Int.cast_zero, sign_zero, Int.sign_zero, Int.cast_zero]
[GOAL]
case inr.inr
z : ℤ
hp : 0 < z
⊢ sign ↑z = ↑(Int.sign z)
[PROOFSTEP]
rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]
[GOAL]
r : ℝ
⊢ sign (-r) = -sign r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign (-r) = -sign r
[PROOFSTEP]
rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
[GOAL]
case inr.inl
⊢ sign (-0) = -sign 0
[PROOFSTEP]
rw [sign_zero, neg_zero, sign_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign (-r) = -sign r
[PROOFSTEP]
rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]
[GOAL]
r : ℝ
⊢ 0 ≤ sign r * r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ sign r * r
[PROOFSTEP]
rw [sign_of_neg hn]
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r
[PROOFSTEP]
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hn.le
[GOAL]
r : ℝ
hn : r < 0
⊢ -1 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
case inr.inl
⊢ 0 ≤ sign 0 * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ sign r * r
[PROOFSTEP]
rw [sign_of_pos hp, one_mul]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r
[PROOFSTEP]
exact hp.le
[GOAL]
r : ℝ
hr : r ≠ 0
⊢ 0 < sign r * r
[PROOFSTEP]
refine' lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr _
[GOAL]
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
⊢ r = 0
[PROOFSTEP]
have hs0 := (zero_eq_mul.mp h).resolve_right hr
[GOAL]
r : ℝ
hr : r ≠ 0
h : 0 = sign r * r
hs0 : sign r = 0
⊢ r = 0
[PROOFSTEP]
exact sign_eq_zero_iff.mp hs0
[GOAL]
r : ℝ
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
obtain hn | hz | hp := sign_apply_eq r
[GOAL]
case inl
r : ℝ
hn : sign r = -1
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hn]
[GOAL]
case inl
r : ℝ
hn : sign r = -1
⊢ (-1)⁻¹ = -1
[PROOFSTEP]
norm_num
[GOAL]
case inr.inl
r : ℝ
hz : sign r = 0
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hz]
[GOAL]
case inr.inl
r : ℝ
hz : sign r = 0
⊢ 0⁻¹ = 0
[PROOFSTEP]
exact inv_zero
[GOAL]
case inr.inr
r : ℝ
hp : sign r = 1
⊢ (sign r)⁻¹ = sign r
[PROOFSTEP]
rw [hp]
[GOAL]
case inr.inr
r : ℝ
hp : sign r = 1
⊢ 1⁻¹ = 1
[PROOFSTEP]
exact inv_one
[GOAL]
r : ℝ
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
[GOAL]
case inl
r : ℝ
hn : r < 0
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]
[GOAL]
case inr.inl
⊢ sign 0⁻¹ = sign 0
[PROOFSTEP]
rw [sign_zero, inv_zero, sign_zero]
[GOAL]
case inr.inr
r : ℝ
hp : 0 < r
⊢ sign r⁻¹ = sign r
[PROOFSTEP]
rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x✝¹ x✝ : (a : α) → a ∈ univ → δ a
⊢ (fun f a => f a (_ : a ∈ univ)) x✝¹ = (fun f a => f a (_ : a ∈ univ)) x✝ → x✝¹ = x✝
[PROOFSTEP]
simp (config := { contextual := true }) [Function.funext_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a
[PROOFSTEP]
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ, exists_imp, mem_pi]
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a (_ : a ∈ univ) ∈ t a) →
      ↑{ toFun := fun f a => f a (_ : a ∈ univ),
                inj' :=
                  (_ :
                    ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                      ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
            x =
          f →
        ∀ (a : α), f a ∈ t a
[PROOFSTEP]
rintro g hg hgf a
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a (_ : a ∈ univ) ∈ t a
hgf :
  ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g =
    f
a : α
⊢ f a ∈ t a
[PROOFSTEP]
rw [← hgf]
[GOAL]
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a (_ : a ∈ univ) ∈ t a
hgf :
  ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g =
    f
a : α
⊢ ↑{ toFun := fun f a => f a (_ : a ∈ univ),
          inj' :=
            (_ :
              ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
      g a ∈
    t a
[PROOFSTEP]
exact hg a
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
[PROOFSTEP]
simp only [piFinset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi]
[GOAL]
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) →
    ∃ a,
      (∀ (a_1 : α), a a_1 (_ : a_1 ∈ univ) ∈ t a_1) ∧
        ↑{ toFun := fun f a => f a (_ : a ∈ univ),
                inj' :=
                  (_ :
                    ∀ (x x_1 : (a : α) → a ∈ univ → δ a),
                      ((fun a => x a (_ : a ∈ univ)) = fun a => x_1 a (_ : a ∈ univ)) → x = x_1) }
            a =
          f
[PROOFSTEP]
exact fun hf => ⟨fun a _ => f a, hf, rfl⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.pi Set.univ fun a => ↑(t a)
[PROOFSTEP]
rw [Set.mem_univ_pi]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
[PROOFSTEP]
exact Fintype.mem_piFinset
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_2
inst✝ : Nonempty α
x✝ : (a : α) → δ a
⊢ ¬x✝ ∈ piFinset fun x => ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
f x✝ : (a : α) → δ a
⊢ (x✝ ∈ piFinset fun i => {f i}) ↔ x✝ ∈ {f}
[PROOFSTEP]
simp only [Function.funext_iff, Fintype.mem_piFinset, mem_singleton]
[GOAL]
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ ∀ (x : (a : α) → β a), x ∈ Fintype.piFinset fun x => univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
α : Type ?u.21193
β : Type ?u.21196
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)
[PROOFSTEP]
classical. exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
[GOAL]
α✝ : Type u_1
α : Type ?u.21193
β : Type ?u.21196
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)
[PROOFSTEP]
exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
[GOAL]
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (pi univ fun a => univ) = univ
[PROOFSTEP]
ext
[GOAL]
case a
α✝ : Type u_1
α : Type u_2
β : α → Type u_3
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ pi univ fun a => univ) ↔ a✝ ∈ univ
[PROOFSTEP]
simp


[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
convert (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = sup (Set.toFinset s) fun i => a ⊓ id i
[PROOFSTEP]
rw [Finset.sup_eq_iSup]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊓ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ s), a ⊓ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = inf (Set.toFinset s) fun i => a ⊔ id i
[PROOFSTEP]
rw [Finset.inf_eq_iInf]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊔ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
src✝ : CompleteLattice α := toCompleteLattice α
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ s), a ⊔ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
convert (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = sup (Set.toFinset s) fun i => a ⊓ id i
[PROOFSTEP]
rw [Finset.sup_eq_iSup]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊓ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨆ (b : α) (_ : b ∈ s), a ⊓ b = ⨆ (a_1 : α) (_ : a_1 ∈ s), a ⊓ id a_1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b ≤ a ⊔ sInf s
[PROOFSTEP]
convert (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = inf (Set.toFinset s) fun i => a ⊔ id i
[PROOFSTEP]
rw [Finset.inf_eq_iInf]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ Set.toFinset s), a ⊔ id a_1
[PROOFSTEP]
simp_rw [Set.mem_toFinset]
[GOAL]
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype α
inst✝ : BooleanAlgebra α
src✝¹ : CompleteLattice α := toCompleteLattice α
src✝ : BooleanAlgebra α := inst✝
a : α
s : Set α
⊢ ⨅ (b : α) (_ : b ∈ s), a ⊔ b = ⨅ (a_1 : α) (_ : a_1 ∈ s), a ⊔ id a_1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
classical
obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
obtain ⟨z, hz⟩ := D.finset_le (Finset.image g Finset.univ)
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
β : Type u_2
γ : Type u_3
inst✝¹ : Nonempty γ
f : γ → α
inst✝ : Fintype β
D : Directed r f
g : β → γ
z : γ
hz : ∀ (i : γ), i ∈ image g univ → r (f i) (f z)
⊢ ∃ z, ∀ (i : β), r (f (g i)) (f z)
[PROOFSTEP]
exact ⟨z, fun i => hz (g i) (Finset.mem_image_of_mem g (Finset.mem_univ i))⟩
[GOAL]
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
⊢ BddAbove (Set.range f)
[PROOFSTEP]
obtain ⟨M, hM⟩ := Fintype.exists_le f
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)
[PROOFSTEP]
refine' ⟨M, fun a ha => _⟩
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≤ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
b : β
⊢ f b ≤ M
[PROOFSTEP]
exact hM b
[GOAL]
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
⊢ BddBelow (Set.range f)
[PROOFSTEP]
obtain ⟨M, hM⟩ := Fintype.exists_ge f
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)
[PROOFSTEP]
refine' ⟨M, fun a ha => _⟩
[GOAL]
case intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
a : α
ha : a ∈ Set.range f
⊢ M ≤ a
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x x_1 => x ≥ x_1
β : Type u_2
inst✝ : Fintype β
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b
[PROOFSTEP]
exact hM b