awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
obtain :
  ∀ (i : ℕ) (hi : i ∈ c.blocks) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₁ :
  ∀ (i : ℕ) (hi : ∃ (y : Fin c.length), c.blocksFun y = i) (i_blocks : 1 < i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₂ :
  ∀ (i : ℕ) (i_blocks : 1 < i) (j : Fin c.length) (hj : c.blocksFun j = i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
obtain₃ :
  ∀ (i : ℕ) (j : Fin c.length) (i_blocks : 1 < c.blocksFun j) (hj : c.blocksFun j = i),
    LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
⊢ LT.lt (α := ℕ) (∑ 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
        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⟩
        }

Premises used: Composition.ofFn_blocksFun, Set.mem_range, Composition.length, Composition.blocks, Composition.blocksFun, Composition.ne_ones_iff, Iff.mp, Fin, List.mem_ofFn'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ ∑ i : Fin c.length, c.blocksFun i = n

Tactic:
c.sum_blocksFun

Premises used: Composition.sum_blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
n₁ : n = ∑ i : Fin c.length, 1
n₂ : LT.lt (α := ℕ) (∑ i : Fin c.length, 1) (∑ i : Fin c.length, c.blocksFun i)
⊢ 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

Premises used: Composition.sum_blocksFun, Composition.length, Fin
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c = ones n ↔ n ≤ c.length

Tactic:
simp [eq_ones_iff_length, le_antisymm_iff, c.length_le]

Premises used: Composition.eq_ones_iff_length, le_antisymm_iff, Composition.length_le
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
h : 0 < n
⊢ ∀ {i : ℕ}, i ∈ [n] → 0 < i

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c : Composition n_1
n : ℕ
h : 0 < n
⊢ [n].sum = n

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
⊢ (single n h).length = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
⊢ (single n h).blocks = [n]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
i : Fin (single n h).length
⊢ (single n h).blocksFun i = n

Tactic:
simp [blocksFun, single]

Premises used: Composition.blocksFun, Composition.single
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
i : Fin n
h₁ : (↑(((single n h).embedding 0 : (a : Fin ((single n h).blocksFun 0)) → Fin n) i) : ℕ) = (↑i : ℕ)
⊢ ((single n h).embedding 0 : (a : Fin ((single n h).blocksFun 0)) → Fin n) i = i

Tactic:
ext
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
i : Fin n
⊢ (↑(((single n h).embedding 0 : (a : Fin ((single n h).blocksFun 0)) → Fin n) i) : ℕ) = (↑i : ℕ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
mp : c = single n h → c.length = 1
mpr : c.length = 1 → c = single n h
⊢ c = single n h ↔ c.length = 1

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
mp : (single n h).length = 1
⊢ c.length = 1

Tactic:
rw [H]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ (single n h).length = 1

Tactic:
single_length h

Premises used: Composition.single_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ (single n h).length = 1

Tactic:
exact single_length h

Premises used: Composition.single_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
mpr : c.blocks = (single n h).blocks
⊢ c = single n h

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c.blocks.length = 1

Tactic:
have A : c.blocks.length = 1 := H ▸ c.blocks_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
⊢ c.blocks.sum = n

Tactic:
have B : c.blocks.sum = n := c.blocks_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : c.blocks.sum = n
mpr :
  ∀ (B : [c.blocks.get (⟨0, ⋯⟩ : Fin c.blocks.length)].sum = n),
    [c.blocks.get (⟨0, ⋯⟩ : Fin c.blocks.length)] = (single n h).blocks
⊢ c.blocks = (single n h).blocks

Tactic:
rw [eq_cons_of_length_one A] at B ⊢

Premises used: List.eq_cons_of_length_one
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get (⟨0, ⋯⟩ : Fin c.blocks.length)].sum = n
⊢ [c.blocks.get (⟨0, ⋯⟩ : Fin c.blocks.length)] = (single n h).blocks

Tactic:
simpa [single_blocks] using B

Premises used: Composition.single_blocks
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
contrapose! : c = single n hn ↔ ∃ (i : Fin c.length), n ≤ c.blocksFun i
⊢ c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
mp : c = single n hn → ∃ (i : Fin c.length), n ≤ c.blocksFun i
mpr : (∃ (i : Fin c.length), n ≤ c.blocksFun i) → c = single n hn
⊢ c = single n hn ↔ ∃ (i : Fin c.length), n ≤ c.blocksFun i

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
⊢ 0 < (single n hn).length

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
⊢ n ≤ (single n hn).blocksFun ⟨0, ⋯⟩

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
⊢ ∃ (i : Fin (single n hn).length), n ≤ (single n hn).blocksFun i

Tactic:
exact ⟨⟨0, by simp⟩, by simp⟩
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
mpr : c.length = 1
⊢ c = single n hn

Tactic:
rw [eq_single_iff_length]

Premises used: Composition.eq_single_iff_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
by_contra : ∀ (ji : ¬j = i), False
⊢ j = i

Tactic:
by_contra ji
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
apply : LT.lt (α := ℕ) (∑ k : Fin c.length, c.blocksFun k) (∑ k : Fin c.length, c.blocksFun k)
⊢ False

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

Premises used: lt_irrefl, Finset.univ, Composition.blocksFun, Finset.sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
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]

Premises used: Composition.sum_blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ c.blocksFun i < ∑ k : Fin c.length, c.blocksFun k

Tactic:
Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j)
            fun _ _ _ => zero_le

Premises used: zero_le, Finset.mem_univ, Finset.single_lt_sum, Composition.one_le_blocksFun
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
k : ∑ k : Fin c.length, c.blocksFun k ≤ c.blocksFun i
⊢ LT.lt (α := ℕ) (∑ 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

Premises used: zero_le, Finset.mem_univ, Composition.blocksFun, Finset.single_lt_sum
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ ∀ (j : Fin c.length), j = i

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
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
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

Premises used: Fintype.card_eq_one_of_forall_eq
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.cast ⋯ = c

Tactic:
rfl

Premises used: Composition.cast, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n m : ℕ
c : Composition m
hmn : m = n
subst : ∀ (c : Composition n), c.cast ⋯ ≍ c
⊢ c.cast hmn ≍ c

Tactic:
subst m
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.cast ⋯ ≍ c

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n m : ℕ
c : Composition m
hmn : m = n
subst : ∀ (c : Composition n), c.cast ⋯ = cast ⋯ c
⊢ c.cast hmn = cast ⋯ c

Tactic:
subst m
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.cast ⋯ = cast ⋯ c

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
i : ℕ
hi : i ∈ c₁.blocks ++ c₂.blocks
⊢ i ∈ c₁.blocks ∨ i ∈ c₂.blocks

Tactic:
rw [mem_append] at hi

Premises used: List.mem_append
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
i : ℕ
hi : i ∈ c₁.blocks ∨ i ∈ c₂.blocks
⊢ 0 < i

Tactic:
hi.elim c₁.blocks_pos c₂.blocks_pos

Premises used: Composition.blocks_pos, Or.elim
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
i : ℕ
hi : i ∈ c₁.blocks ∨ i ∈ c₂.blocks
⊢ 0 < i

Tactic:
exact hi.elim c₁.blocks_pos c₂.blocks_pos

Premises used: Composition.blocks_pos, Or.elim
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ (c₁.blocks ++ c₂.blocks).sum = m + n

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c_1 : Composition n
m : ℕ
c : Composition n
⊢ c.blocks.reverse.sum = n

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.reverse.reverse = c

Tactic:
Composition.ext <| List.reverse_reverse _

Premises used: Composition.ext, List.reverse_reverse
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Function.Involutive (α := Composition n) reverse

Tactic:
reverse_reverse

Premises used: Function.Involutive, Composition.reverse_reverse
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Function.Bijective (α := Composition n) reverse

Tactic:
reverse_involutive.bijective

Premises used: Composition.reverse_involutive, Function.Involutive.bijective
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Function.Injective (α := Composition n) reverse

Tactic:
reverse_involutive.injective

Premises used: Composition.reverse_involutive, Function.Involutive.injective
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Function.Surjective (α := Composition n) reverse

Tactic:
reverse_involutive.surjective

Premises used: Function.Involutive.surjective, Composition.reverse_involutive
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c₁ c₂ : Composition n
⊢ c₁.reverse = c₂.reverse ↔ c₁ = c₂

Tactic:
reverse_injective.eq_iff

Premises used: Function.Injective.eq_iff, Composition.reverse_injective
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
blocks : (ones n).reverse.blocks = (ones n).blocks
⊢ (ones n).reverse = ones n

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ (ones n).reverse.blocks = (ones n).blocks

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
blocks : (single n hn).reverse.blocks = (single n hn).blocks
⊢ (single n hn).reverse = single n hn

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
⊢ (single n hn).reverse.blocks = (single n hn).blocks

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : Composition n
⊢ c.reverse = ones n ↔ c = ones n

Tactic:
reverse_injective.eq_iff' reverse_ones

Premises used: Function.Injective.eq_iff', Composition.reverse_injective, Composition.reverse_ones
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c.reverse = single n hn ↔ c = single n hn

Tactic:
reverse_injective.eq_iff' <| reverse_single _

Premises used: Function.Injective.eq_iff', Composition.reverse_injective, Composition.reverse_single
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ (c₁.append c₂).reverse.blocks = ((c₂.reverse.append c₁.reverse).cast ⋯).blocks

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n : ℕ
c : Composition n
zero : motive 0 (ones 0)
single_append : (k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((single (k + 1) ⋯).append c)
blocks tail : List ℕ
blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i
⊢ motive (0 :: tail).sum
    { blocks := 0 :: tail, blocks_pos := @blocks_pos, blocks_sum := ⋯ : Composition (0 :: tail).sum }

Tactic:
simp at blocks_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
k : ℕ
l : List ℕ
blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i
⊢ l.sum < (k.succ :: l).sum

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
k : ℕ
l : List ℕ
blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i
⊢ l.sum < (k.succ :: l).sum

Tactic:
decreasing_by simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n_2 : ℕ
c_2 : Composition n_2
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
h : k + 1 + n = n + (k + 1)
h₁ : k + 1 + n = n + (k + 1) → ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)
⊢ motive (k + 1 + n) ((single (k + 1) ⋯).append c).reverse

Tactic:
convert! append_single k n c.reverse ih using 1

Premises used: Composition.reverse
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n_2 : ℕ
c_2 : Composition n_2
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ k + 1 + n = n + (k + 1)

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n_2 : ℕ
c_2 : Composition n_2
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1 : k + 1 + n = n + (k + 1)
h : (c.reverse.append (single (k + 1) ⋯)).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
rw [reverse_append, reverse_single]

Premises used: Composition.reverse_append, Composition.reverse_single
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 : ℕ
c_1 : Composition n_1
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n_2 : ℕ
c_2 : Composition n_2
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1 : k + 1 + n = n + (k + 1)
⊢ (c.reverse.append (single (k + 1) ⋯)).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
apply cast_heq

Premises used: Composition.cast_heq
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
n : ℕ
ns : List ℕ
⊢ l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns

Tactic:
simp [splitWrtCompositionAux]

Premises used: List.splitWrtCompositionAux
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
ns : List ℕ
nil : ∀ (l : List α), (l.splitWrtCompositionAux []).length = length (α := ℕ) []
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (l : List α), (l.splitWrtCompositionAux tail).length = tail.length) →
      ∀ (l : List α), (l.splitWrtCompositionAux (head :: tail)).length = (head :: tail).length
⊢ (l.splitWrtCompositionAux ns).length = ns.length

Tactic:
induction ns generalizing l
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = length (α := ℕ) []

Tactic:
simp [splitWrtCompositionAux, *]

Premises used: List.splitWrtCompositionAux
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α), (l.splitWrtCompositionAux tail).length = tail.length
l : List α
⊢ (l.splitWrtCompositionAux (head :: tail)).length = (head :: tail).length

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
α : Type u_1
l : List α
c : Composition n
⊢ (l.splitWrtComposition c).length = c.length

Tactic:
length_splitWrtCompositionAux _ _

Premises used: List.length_splitWrtCompositionAux, List.splitWrtComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
⊢ ∀ {l : List α}, sum [] ≤ l.length → map length (l.splitWrtCompositionAux []) = []

Tactic:
simp [splitWrtCompositionAux]

Premises used: List.splitWrtCompositionAux
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
⊢ ∀ {l : List α}, (n :: ns).sum ≤ l.length → map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns

Tactic:
grind [splitWrtCompositionAux_cons]

Premises used: List.splitWrtCompositionAux_cons
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
ns : List ℕ
nil : ∀ {l : List α}, sum [] ≤ l.length → map length (l.splitWrtCompositionAux []) = []
cons :
  ∀ (n : ℕ) (ns : List ℕ) (IH : ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns)
    {l : List α}, (n :: ns).sum ≤ l.length → map length (l.splitWrtCompositionAux (n :: ns)) = n :: ns
⊢ ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns

Tactic:
induction ns with
  | nil => simp [splitWrtCompositionAux]
  | cons n ns IH => grind [splitWrtCompositionAux_cons]

Premises used: List.cons, List.splitWrtCompositionAux, List.splitWrtCompositionAux_cons, List.nil
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
c : Composition l.length
⊢ map length (l.splitWrtComposition c) = c.blocks

Tactic:
map_length_splitWrtCompositionAux (le_of_eq c.blocks_sum)

Premises used: Composition.blocks_sum, List.splitWrtComposition, le_of_eq, List.map_length_splitWrtCompositionAux
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
⊢ l'.length ∈ map length (l.splitWrtComposition c)

Tactic:
have : l'.length ∈ (l.splitWrtComposition c).map List.length :=
    List.mem_map_of_mem h
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ map length (l.splitWrtComposition c)
⊢ l'.length ∈ c.blocks

Tactic:
rw [map_length_splitWrtComposition] at this

Premises used: List.map_length_splitWrtComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ c.blocks
⊢ 0 < l'.length

Tactic:
c.blocks_pos this

Premises used: Composition.blocks_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ c.blocks
⊢ 0 < l'.length

Tactic:
exact c.blocks_pos this

Premises used: Composition.blocks_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
e_a : map length (l.splitWrtComposition c) = c.blocks
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ map length (l.splitWrtComposition c) = c.blocks

Tactic:
map_length_splitWrtComposition l c

Premises used: List.map_length_splitWrtComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ map length (l.splitWrtComposition c) = c.blocks

Tactic:
exact map_length_splitWrtComposition l c

Premises used: List.map_length_splitWrtComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
i : ℕ
hi : i < (l.splitWrtCompositionAux []).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux []) i hi =
    drop (sum (take i [])) (take (sum (take (i + 1) [])) l)

Tactic:
cases hi