-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem ne_single_iff {n : ℕ} (hn : 0 < n) {c : Composition n} :
    c ≠ single n hn ↔ ∀ i, c.blocksFun i < n

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ False

Tactic:
apply lt_irrefl (∑ k, c.blocksFun k)

Result:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k : Fin c.length, c.blocksFun k < ∑ k : Fin c.length, c.blocksFun k

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ ∀ (j : Fin c.length), j = i

Tactic:
intro j

Result:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
⊢ j = i

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k : Fin c.length, c.blocksFun k < ∑ k : Fin c.length, c.blocksFun k

Tactic:
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 _

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ c.blocksFun i

Tactic:
constructor

Result:
case mp
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ c.blocksFun i

case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
⊢ j = i

Tactic:
by_contra ji

Result:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ False

Proof state:
case mp
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ c.blocksFun i

Tactic:
rintro rfl

Result:
case mp
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ (single n hn).blocksFun i

Proof state:
n : ℕ
hn : 0 < n
⊢ 0 < (single n hn).length

Tactic:
simp

Result:
no goals

Proof state:
case mp
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ (single n hn).blocksFun i

Tactic:
exact ⟨⟨0, by simp⟩, by simp⟩

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
⊢ n ≤ (single n hn).blocksFun ⟨0, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c.length = 1

Tactic:
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 _

Result:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
this : ∀ (j : Fin c.length), j = i
⊢ c.length = 1

Proof state:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
this : ∀ (j : Fin c.length), j = i
⊢ c.length = 1

Tactic:
simpa using Fintype.card_eq_one_of_forall_eq this

Result:
no goals

Proof state:
case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn

Tactic:
rintro ⟨i, hi⟩

Result:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c = single n hn

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k : Fin c.length, c.blocksFun k ≤ c.blocksFun i

Tactic:
simp only [c.sum_blocksFun, hi]

Result:
no goals

Proof state:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c = single n hn

Tactic:
rw [eq_single_iff_length]

Result:
case mpr.intro
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c.length = 1

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n

Tactic:
rw [← not_iff_not]

Result:
n : ℕ
hn : 0 < n
c : Composition n
⊢ ¬c ≠ single n hn ↔ ¬∀ (i : Fin c.length), c.blocksFun i < n

Proof state:
n : ℕ
hn : 0 < n
c : Composition n
⊢ ¬c ≠ single n hn ↔ ¬∀ (i : Fin c.length), c.blocksFun i < n

Tactic:
push_neg

Result:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ c.blocksFun i