-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem eq_ones_iff_length {c : Composition n} : c = ones n ↔ c.length = n

Proof state:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Tactic:
obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H

Result:
case intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Proof state:
case intro.intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
i_blocks : 1 < i
j : Fin c.length
hj : c.blocksFun j = i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Tactic:
rw [← hj] at i_blocks

Result:
case intro.intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
j : Fin c.length
i_blocks : 1 < c.blocksFun j
hj : c.blocksFun j = i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Proof state:
case mp
n : ℕ
c : Composition n
⊢ c = ones n → c.length = n

Tactic:
rintro rfl

Result:
case mp
n : ℕ
⊢ (ones n).length = n

Proof state:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ False

Tactic:
apply lt_irrefl n

Result:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n < n

Proof state:
case mpr
n : ℕ
c : Composition n
⊢ ¬c = ones n → ¬c.length = n

Tactic:
intro H length_n

Result:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ False

Proof state:
n : ℕ
c : Composition n
⊢ c = ones n ↔ c.length = n

Tactic:
constructor

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

case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n

Proof state:
case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n

Tactic:
contrapose

Result:
case mpr
n : ℕ
c : Composition n
⊢ ¬c = ones n → ¬c.length = n

Proof state:
case mp
n : ℕ
⊢ (ones n).length = n

Tactic:
exact ones_length n

Result:
no goals

Proof state:
case intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : ∃ y, c.blocksFun y = i
i_blocks : 1 < i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Tactic:
obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi

Result:
case intro.intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
i_blocks : 1 < i
j : Fin c.length
hj : c.blocksFun j = i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Proof state:
case intro.intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
j : Fin c.length
i_blocks : 1 < c.blocksFun j
hj : c.blocksFun j = i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Tactic:
exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩

Result:
no goals

Proof state:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n < n

Tactic:
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 _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
    }
  _ = n := c.sum_blocksFun

Result:
no goals

Proof state:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n = ∑ i : Fin c.length, 1

Tactic:
simp [length_n]

Result:
no goals

Proof state:
case intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ c.blocks
i_blocks : 1 < i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i

Tactic:
rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi

Result:
case intro.intro
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : ∃ y, c.blocksFun y = i
i_blocks : 1 < i
⊢ ∑ i : Fin c.length, 1 < ∑ i : Fin c.length, c.blocksFun i