case mk
α : Type ?u.1285
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₂ }
α : Type ?u.1285
n : ℕ
⊢ Function.Surjective (ofComposition n)
rintro ⟨b, hb₁, hb₂⟩
case mk.intro
α : Type ?u.1285
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₂ }
case mk
α : Type ?u.1285
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₂ }
rcases Quotient.exists_rep b with ⟨b, rfl⟩
case mk.intro
α : Type ?u.1285
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
case mk.intro
α : Type ?u.1285
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₂ }
refine' ⟨⟨b, fun {i} hi => hb₁ hi, _⟩, Partition.ext _ _ rfl⟩
no goals
case mk.intro
α : Type ?u.1285
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
simpa using hb₂