[GOAL]
α : Type u_1
n : ℕ
p q : Partition n
⊢ Decidable (p = q)
[PROOFSTEP]
simp [Partition.ext_iff]
[GOAL]
α : Type u_1
n : ℕ
p q : Partition n
⊢ Decidable (p.parts = q.parts)
[PROOFSTEP]
exact decidableEq p.parts q.parts
[GOAL]
α : Type u_1
n : ℕ
c : Composition n
⊢ sum ↑c.blocks = n
[PROOFSTEP]
rw [Multiset.coe_sum, c.blocks_sum]
[GOAL]
α : Type u_1
n : ℕ
⊢ Function.Surjective (ofComposition n)
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case mk
α : Type u_1
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : sum b = n
⊢ ∃ a, ofComposition n a = { parts := b, parts_pos := hb₁, parts_sum := hb₂ }
[PROOFSTEP]
rcases Quotient.exists_rep b with ⟨b, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ Quotient.mk (List.isSetoid ℕ) b → 0 < i
hb₂ : sum (Quotient.mk (List.isSetoid ℕ) b) = n
⊢ ∃ a, ofComposition n a = { parts := Quotient.mk (List.isSetoid ℕ) b, parts_pos := hb₁, parts_sum := hb₂ }
[PROOFSTEP]
refine' ⟨⟨b, fun {i} hi => hb₁ hi, _⟩, Partition.ext _ _ rfl⟩
[GOAL]
case mk.intro
α : Type u_1
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ Quotient.mk (List.isSetoid ℕ) b → 0 < i
hb₂ : sum (Quotient.mk (List.isSetoid ℕ) b) = n
⊢ List.sum b = n
[PROOFSTEP]
simpa using hb₂
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
i : ℕ
hi : i ∈ filter (fun x => x ≠ 0) l
⊢ i ≠ 0
[PROOFSTEP]
apply of_mem_filter hi
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
have lt : l.filter (· = 0) + l.filter (· ≠ 0) = l := filter_add_not _ l
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l = l
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
apply_fun Multiset.sum at lt 
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
have lz : (l.filter (· = 0)).sum = 0 := by
  rw [Multiset.sum_eq_zero_iff]
  simp
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ sum (filter (fun x => x = 0) l) = 0
[PROOFSTEP]
rw [Multiset.sum_eq_zero_iff]
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ ∀ (x : ℕ), x ∈ filter (fun x => x = 0) l → x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
lz : sum (filter (fun x => x = 0) l) = 0
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
rwa [sum_add (filter (fun x => x = 0) l) (filter (fun x => ¬x = 0) l), lz, hl, zero_add] at lt 
