n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ ¬c ≠ single n hn ↔ ¬∀ (i : Fin (length c)), blocksFun c i < n
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin (length c)), blocksFun c i < n
rw [← not_iff_not]
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ blocksFun c i
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ ¬c ≠ single n hn ↔ ¬∀ (i : Fin (length c)), blocksFun c i < n
push_neg
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ blocksFun c i

case mpr
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ blocksFun c i) → c = single n hn
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ blocksFun c i
constructor
case mp
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ blocksFun (single n hn) i
case mp
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ blocksFun c i
rintro rfl
no goals
case mp
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ blocksFun (single n hn) i
exact ⟨⟨0, by simp⟩, by simp⟩
no goals
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ 0 < length (single n hn)
simp
no goals
n✝ : ℕ
c : Composition n✝
n : ℕ
hn : 0 < n
⊢ n ≤ blocksFun (single n hn) { val := 0, isLt := (_ : 0 < 1) }
simp
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ c = single n hn
case mpr
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ blocksFun c i) → c = single n hn
rintro ⟨i, hi⟩
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ length c = 1
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ c = single n hn
rw [eq_single_iff_length]
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
this : ∀ (j : Fin (length c)), j = i
⊢ length c = 1
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ length c = 1
have : ∀ j : Fin c.length, j = i := by
  intro j
  by_contra ji
  apply lt_irrefl (∑ k, c.blocksFun k)
  calc
    (∑ k, c.blocksFun k) ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
    _ < ∑ k, c.blocksFun k :=
      Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j)
        fun _ _ _ => zero_le _
no goals
case mpr.intro
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
this : ∀ (j : Fin (length c)), j = i
⊢ length c = 1
simpa using Fintype.card_eq_one_of_forall_eq this
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
⊢ j = i
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
⊢ ∀ (j : Fin (length c)), j = i
intro j
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ False
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
⊢ j = i
by_contra ji
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ ∑ k : Fin (length c), blocksFun c k < ∑ k : Fin (length c), blocksFun c k
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ False
apply lt_irrefl (∑ k, c.blocksFun k)
no goals
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ ∑ k : Fin (length c), blocksFun c k < ∑ k : Fin (length c), blocksFun c k
calc
  (∑ k, c.blocksFun k) ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
  _ < ∑ k, c.blocksFun k :=
    Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j)
      fun _ _ _ => zero_le _
no goals
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
hn : 0 < n
c : Composition n
i : Fin (length c)
hi : n ≤ blocksFun c i
j : Fin (length c)
ji : ¬j = i
⊢ ∑ k : Fin (length c), blocksFun c k ≤ blocksFun c i
simp only [c.sum_blocksFun, hi]