case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → length c = n

case mpr
n : ℕ
c✝ c : Composition n
⊢ length c = n → c = ones n
n : ℕ
c✝ c : Composition n
⊢ c = ones n ↔ length c = n
constructor
case mp
n : ℕ
c : Composition n
⊢ length (ones n) = n
case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → length c = n
rintro rfl
no goals
case mp
n : ℕ
c : Composition n
⊢ length (ones n) = n
exact ones_length n
case mpr
n : ℕ
c✝ c : Composition n
⊢ ¬c = ones n → ¬length c = n
case mpr
n : ℕ
c✝ c : Composition n
⊢ length c = n → c = ones n
contrapose
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ False
case mpr
n : ℕ
c✝ c : Composition n
⊢ ¬c = ones n → ¬length c = n
intro H length_n
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ n < n
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ False
apply lt_irrefl n
no goals
case mpr
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ n < n
calc
  n = ∑ i : Fin c.length, 1 := by simp [length_n]
  _ < ∑ i : Fin c.length, c.blocksFun i := by
    {
    obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
    rw [← ofFn_blocksFun, mem_ofFn c.blocksFun, Set.mem_range] at hi
    obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
    rw [← hj] at i_blocks
    exact Finset.sum_lt_sum (fun i _ => by simp [blocksFun]) ⟨j, Finset.mem_univ _, i_blocks⟩
    }
  _ = n := c.sum_blocksFun
no goals
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
⊢ n = ∑ i : Fin (length c), 1
simp [length_n]
no goals
n : ℕ
c✝ c : Composition n
H : ¬c = ones n
length_n : length c = n
i✝ : ℕ
j : Fin (length c)
i_blocks : 1 < blocksFun c j
hj : blocksFun c j = i✝
i : Fin (length c)
x✝ : i ∈ Finset.univ
⊢ 1 ≤ blocksFun c i
simp [blocksFun]