n : ℕ
c✝ c : Composition n
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
n : ℕ
c✝ c : Composition n
⊢ c ≠ ones n ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
refine' (not_congr eq_ones_iff).trans _
n : ℕ
c✝ c : Composition n
this : ∀ (j : ℕ), j ∈ c.blocks → (j = 1 ↔ j ≤ 1)
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
n : ℕ
c✝ c : Composition n
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
have : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1 := fun j hj => by simp [le_antisymm_iff, c.one_le_blocks hj]
no goals
n : ℕ
c✝ c : Composition n
this : ∀ (j : ℕ), j ∈ c.blocks → (j = 1 ↔ j ≤ 1)
⊢ (¬∀ (i : ℕ), i ∈ c.blocks → i = 1) ↔ ∃ i, i ∈ c.blocks ∧ 1 < i
simp (config := { contextual := true }) [this]
no goals
n : ℕ
c✝ c : Composition n
j : ℕ
hj : j ∈ c.blocks
⊢ j = 1 ↔ j ≤ 1
simp [le_antisymm_iff, c.one_le_blocks hj]