case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → ∀ (i : ℕ), i ∈ c.blocks → i = 1

case mpr
n : ℕ
c✝ c : Composition n
⊢ (∀ (i : ℕ), i ∈ c.blocks → i = 1) → c = ones n
n : ℕ
c✝ c : Composition n
⊢ c = ones n ↔ ∀ (i : ℕ), i ∈ c.blocks → i = 1
constructor
case mp
n : ℕ
c : Composition n
⊢ ∀ (i : ℕ), i ∈ (ones n).blocks → i = 1
case mp
n : ℕ
c✝ c : Composition n
⊢ c = ones n → ∀ (i : ℕ), i ∈ c.blocks → i = 1
rintro rfl
no goals
case mp
n : ℕ
c : Composition n
⊢ ∀ (i : ℕ), i ∈ (ones n).blocks → i = 1
exact fun i => eq_of_mem_replicate
case mpr
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c = ones n
case mpr
n : ℕ
c✝ c : Composition n
⊢ (∀ (i : ℕ), i ∈ c.blocks → i = 1) → c = ones n
intro H
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c.blocks = (ones n).blocks
case mpr
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c = ones n
ext1
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ c.blocks = (ones n).blocks
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
⊢ c.blocks = (ones n).blocks
have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
this : List.length c.blocks = n
⊢ c.blocks = (ones n).blocks
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ c.blocks = (ones n).blocks
have : c.blocks.length = n := by
  conv_rhs => rw [← c.blocks_sum, A]
  simp
no goals
case mpr.blocks
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
this : List.length c.blocks = n
⊢ c.blocks = (ones n).blocks
rw [A, this, ones_blocks]
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ List.length c.blocks = sum (replicate (List.length c.blocks) 1)
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ List.length c.blocks = n
conv_rhs => rw [← c.blocks_sum, A]
no goals
n : ℕ
c✝ c : Composition n
H : ∀ (i : ℕ), i ∈ c.blocks → i = 1
A : c.blocks = replicate (List.length c.blocks) 1
⊢ List.length c.blocks = sum (replicate (List.length c.blocks) 1)
simp