awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
      drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i < (l.splitWrtCompositionAux (n :: ns)).length
cons :
  ∀ (hi : 0 < (l.splitWrtCompositionAux (n :: ns)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) 0 hi =
      drop (take 0 (n :: ns)).sum (take (take (HAdd.hAdd (α := ℕ) 0 1) (n :: ns)).sum l)
cons₁ :
  ∀ (i : ℕ) (hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) (i + 1)
        hi =
      drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) i hi =
    drop (take i (n :: ns)).sum (take (take (i + 1) (n :: ns)).sum l)

Tactic:
rcases i with - | i
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
      drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
hi : 0 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) 0 hi =
    drop (take 0 (n :: ns)).sum (take (take (HAdd.hAdd (α := ℕ) 0 1) (n :: ns)).sum l)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
      drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
cons :
  take ((take (i + 1) ns).sum - (take i ns).sum) (drop (n + (take i ns).sum) l) =
    take (n + (take (i + 1) ns).sum - (n + (take i ns).sum)) (drop (n + (take i ns).sum) l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) (i + 1) hi =
    drop (take (i + 1) (n :: ns)).sum (take (take (i + 1 + 1) (n :: ns)).sum l)

Tactic:
simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]

Premises used: List.drop_drop, List.drop_take, List.splitAt_eq, List.sum_cons, List.splitWrtCompositionAux, List.take, List.getElem_cons_succ
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
      drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
i : ℕ
hi : i + 1 < (l.splitWrtCompositionAux (n :: ns)).length
cons cons₁ :
  take ((take (i + 1) ns).sum - (take i ns).sum) (drop (n + (take i ns).sum) l) =
    take ((take (i + 1) ns).sum - (take i ns).sum) (drop (n + (take i ns).sum) l)
⊢ take ((take (i + 1) ns).sum - (take i ns).sum) (drop (n + (take i ns).sum) l) =
    take (n + (take (i + 1) ns).sum - (n + (take i ns).sum)) (drop (n + (take i ns).sum) l)

Tactic:
rw [Nat.add_sub_add_left]

Premises used: Nat.add_sub_add_left
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
ns : List ℕ
i : ℕ
hi : i < (l.splitWrtCompositionAux ns).length
nil :
  ∀ (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)
cons :
  ∀ (n : ℕ) (ns : List ℕ)
    (IH :
      ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
        getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
          drop (take i ns).sum (take (take (i + 1) ns).sum l))
    (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux (n :: ns)).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux (n :: ns)) i hi =
      drop (take i (n :: ns)).sum (take (take (i + 1) (n :: ns)).sum l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtCompositionAux ns) i hi =
    drop (take i ns).sum (take (take (i + 1) ns).sum l)

Tactic:
induction ns generalizing l i with
  | nil => cases hi
  | cons n ns IH =>
    rcases i with - | i
    · simp
    · simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]
      rw [Nat.add_sub_add_left]

Premises used: List.drop_drop, List.drop_take, Nat.add_sub_add_left, List.splitAt_eq, List.cons, List.sum_cons, List.splitWrtCompositionAux, List.take, List.getElem_cons_succ, List.nil
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
α : Type u_1
l : List α
c : Composition n
i : ℕ
hi : i < (l.splitWrtComposition c).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtComposition c) i hi =
    drop (c.sizeUpTo i) (take (c.sizeUpTo (i + 1)) l)

Tactic:
getElem_splitWrtCompositionAux _ _ hi

Premises used: List.splitWrtComposition, Composition.sizeUpTo, List.getElem_splitWrtCompositionAux
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
α : Type u_1
l : List α
c : Composition n
i : ℕ
h : i < (l.splitWrtComposition c).length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (l.splitWrtComposition c) i h =
    drop (c.sizeUpTo i) (take (c.sizeUpTo (i + 1)) l)

Tactic:
getElem_splitWrtComposition' _ _ h

Premises used: List.getElem_splitWrtComposition'
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
⊢ sum [] = l.length → (l.splitWrtCompositionAux []).flatten = l

Tactic:
fun h ↦ (length_eq_zero_iff.1 h.symm).symm

Premises used: Iff.mp, Eq.symm, List.length_eq_zero_iff, List.flatten
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
⊢ ∀ {l : List α}, sum [] = l.length → (l.splitWrtCompositionAux []).flatten = l

Tactic:
exact fun h ↦ (length_eq_zero_iff.1 h.symm).symm

Premises used: Iff.mp, Eq.symm, List.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : (n :: ns).sum = l.length
⊢ n + ns.sum = l.length

Tactic:
rw [sum_cons] at h

Premises used: List.sum_cons
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
cons : (take n l :: (drop n l).splitWrtCompositionAux ns).flatten = l
⊢ (l.splitWrtCompositionAux (n :: ns)).flatten = l

Tactic:
simp only [splitWrtCompositionAux_cons]

Premises used: List.splitWrtCompositionAux_cons
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
cons : take n l ++ drop n l = l
cons₁ : ns.sum = (drop n l).length
⊢ take n l ++ ((drop n l).splitWrtCompositionAux ns).flatten = l

Tactic:
rw [IH]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ drop n l = l

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
cons : ns.sum = l.length - n
cons₁ : ns.sum = n + ns.sum - n
cons₂ cons₃ : ns.sum = ns.sum
⊢ ns.sum = (drop n l).length

Tactic:
rw [length_drop, ← h, add_tsub_cancel_left]

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

Tactic:
induction ns with
  | nil => exact fun h ↦ (length_eq_zero_iff.1 h.symm).symm
  | cons n ns IH =>
    intro l h; rw [sum_cons] at h
    simp only [splitWrtCompositionAux_cons]; dsimp
    rw [IH]
    · simp
    · rw [length_drop, ← h, add_tsub_cancel_left]

Premises used: List.length_drop, add_tsub_cancel_left, List.cons, List.sum_cons, Iff.mp, List.splitWrtCompositionAux_cons, Eq.symm, List.length_eq_zero_iff, List.nil
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
l : List α
c : Composition l.length
⊢ (l.splitWrtComposition c).flatten = l

Tactic:
flatten_splitWrtCompositionAux c.blocks_sum

Premises used: List.flatten_splitWrtCompositionAux, Composition.blocks_sum, List.splitWrtComposition
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
α : Type u_1
L : List (List α)
c : Composition L.flatten.length
h : map length L = c.blocks
⊢ L.flatten.splitWrtComposition c = L

Tactic:
simp only [and_self_iff, eq_iff_flatten_eq, flatten_splitWrtComposition,
    map_length_splitWrtComposition, h]

Premises used: List.eq_iff_flatten_eq, List.map_length_splitWrtComposition, List.flatten_splitWrtComposition, and_self_iff
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin (n - 1)
⊢ 1 + (↑i : ℕ) < n.succ

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
⊢ Membership.mem (γ := Finset (Fin n.succ))
    (Set.toFinset {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1})
    0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
⊢ Membership.mem (γ := Finset (Fin n.succ))
    (Set.toFinset {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1})
    (Fin.last n)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
boundaries :
  ∀ (i : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ))
        (CompositionAsSet.boundaries
          ((fun (s : Finset (Fin (n - 1))) ↦
              {
                boundaries :=
                  Set.toFinset
                    {i : Fin n.succ |
                      i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1},
                zero_mem := ⋯, getLast_mem := ⋯ : CompositionAsSet n })
            ((fun (c : CompositionAsSet n) ↦
                (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ) ∈ c.boundaries} :
                  Finset (Fin (n - 1))))
              c)))
        i ↔
      i ∈ c.boundaries
⊢ (fun (s : Finset (Fin (n - 1))) ↦
        {
          boundaries :=
            Set.toFinset
              {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1},
          zero_mem := ⋯, getLast_mem := ⋯ : CompositionAsSet n })
      ((fun (c : CompositionAsSet n) ↦
          (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ) ∈ c.boundaries} : Finset (Fin (n - 1))))
        c) =
    c

Tactic:
ext i
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
boundaries :
  (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) ↔
    i ∈ c.boundaries
⊢ Membership.mem (γ := Finset (Fin n.succ))
      (CompositionAsSet.boundaries
        ((fun (s : Finset (Fin (n - 1))) ↦
            {
              boundaries :=
                Set.toFinset
                  {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1},
              zero_mem := ⋯, getLast_mem := ⋯ : CompositionAsSet n })
          ((fun (c : CompositionAsSet n) ↦
              (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ) ∈ c.boundaries} : Finset (Fin (n - 1))))
            c)))
      i ↔
    i ∈ c.boundaries

Tactic:
simp only [add_comm, Set.toFinset_setOf, Finset.mem_univ,
     Finset.mem_filter, true_and, exists_prop]

Premises used: Finset.mem_univ, exists_prop, add_comm, Finset.mem_filter, Set.toFinset_setOf, true_and
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
boundaries :
  (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) →
    i ∈ c.boundaries
boundaries₁ :
  i ∈ c.boundaries →
    i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) ↔
    i ∈ c.boundaries

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries

Tactic:
c.zero_mem

Premises used: CompositionAsSet.zero_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ 0 ∈ c.boundaries

Tactic:
exact c.zero_mem

Premises used: CompositionAsSet.zero_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

Tactic:
c.getLast_mem

Premises used: CompositionAsSet.getLast_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

Tactic:
exact c.getLast_mem

Premises used: CompositionAsSet.getLast_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries
hj2 : (↑i : ℕ) = (↑j : ℕ) + 1
⊢ ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries

Tactic:
hj1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries
hj2 : (↑i : ℕ) = (↑j : ℕ) + 1
⊢ i ∈ c.boundaries

Tactic:
convert! hj1
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
boundaries :
  i ∈ c.boundaries →
    (∃ (y : Fin n), y.succ = i) →
      i ≠ Fin.last n → ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1
⊢ i ∈ c.boundaries →
    i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1

Tactic:
simp only [or_iff_not_imp_left, ← ne_eq, ← Fin.exists_succ_eq]

Premises used: ne_eq, Classical.or_iff_not_imp_left, Fin.exists_succ_eq
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet n
j : Fin n
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last n
boundaries :
  ∀ (n : ℕ) (c : CompositionAsSet (n + 1)) (j : Fin (n + 1)) (i_mem : j.succ ∈ c.boundaries)
    (i_ne_last : j.succ ≠ Fin.last (n + 1)),
    ∃ (j_1 : Fin (n + 1 - 1)), ⟨(↑j_1 : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1
⊢ ∃ (j_1 : Fin (n - 1)), ⟨(↑j_1 : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1

Tactic:
rcases Nat.exists_add_one_eq.mpr j.pos with ⟨n, rfl⟩

Premises used: Iff.mpr, Fin.pos, Nat.exists_add_one_eq, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet (n + 1)
j : Fin (n + 1)
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last (n + 1)
⊢ ∃ (k : Fin n), k.castSucc = j

Tactic:
simpa [Fin.exists_castSucc_eq] using i_ne_last

Premises used: Fin.exists_castSucc_eq
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet (n + 1)
j : Fin (n + 1)
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last (n + 1)
boundaries :
  ∀ (k : Fin n) (i_mem : k.castSucc.succ ∈ c.boundaries) (i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)),
    ∃ (j : Fin (n + 1 - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑j : ℕ) + 1
⊢ ∃ (j_1 : Fin (n + 1 - 1)), ⟨(↑j_1 : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1

Tactic:
obtain ⟨k, rfl⟩ : ∃ k : Fin n, k.castSucc = j := by
        simpa [Fin.exists_castSucc_eq] using i_ne_last

Premises used: Fin, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet (n + 1)
k : Fin n
i_mem : k.castSucc.succ ∈ c.boundaries
i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)
h : ⟨(↑k : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑k : ℕ) + 1
⊢ ∃ (j : Fin (n + 1 - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑j : ℕ) + 1

Tactic:
use k
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
c : CompositionAsSet (n + 1)
k : Fin n
i_mem : k.castSucc.succ ∈ c.boundaries
i_ne_last : k.castSucc.succ ≠ Fin.last (n + 1)
⊢ ⟨(↑k : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑k : ℕ) + 1

Tactic:
simpa using i_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
h :
  ∀ (i : Fin (n - 1)),
    Membership.mem (γ := Finset (Fin (n - 1)))
        ((fun (c : CompositionAsSet n) ↦
            (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ) ∈ c.boundaries} : Finset (Fin (n - 1))))
          ((fun (s : Finset (Fin (n - 1))) ↦
              {
                boundaries :=
                  Set.toFinset
                    {i : Fin n.succ |
                      i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1},
                zero_mem := ⋯, getLast_mem := ⋯ : CompositionAsSet n })
            s))
        i ↔
      i ∈ s
⊢ (fun (c : CompositionAsSet n) ↦
        (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ) ∈ c.boundaries} : Finset (Fin (n - 1))))
      ((fun (s : Finset (Fin (n - 1))) ↦
          {
            boundaries :=
              Set.toFinset
                {i : Fin n.succ | i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1},
            zero_mem := ⋯, getLast_mem := ⋯ : CompositionAsSet n })
        s) =
    s

Tactic:
ext i
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ (↑i : ℕ) + 1 ≠ n

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
⊢ (↑i : ℕ) + 1 ≠ n

Tactic:
have : (i : ℕ) + 1 ≠ n := by lia
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
⊢ Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)
rw : Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
⊢ Fintype.card (CompositionAsSet n) = HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
rw [← this]
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))

Tactic:
Fintype.card_congr (compositionAsSetEquiv n)

Premises used: Fintype.card_congr, compositionAsSetEquiv
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))

Tactic:
exact Fintype.card_congr (compositionAsSetEquiv n)

Premises used: Fintype.card_congr, compositionAsSetEquiv
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.Nonempty

Tactic:
⟨0, c.zero_mem⟩

Premises used: CompositionAsSet.zero_mem, Exists.intro, Finset.Nonempty, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ 0 < c.boundaries.card

Tactic:
Finset.card_pos.mpr c.boundaries_nonempty

Premises used: Iff.mpr, CompositionAsSet.boundaries_nonempty, Finset.card_pos
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.card = c.length + 1

Tactic:
(tsub_eq_iff_eq_add_of_le (Nat.succ_le_of_lt c.card_boundaries_pos)).mp rfl

Premises used: CompositionAsSet.card_boundaries_pos, Nat.succ_le_of_lt, tsub_eq_iff_eq_add_of_le, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
rw : c.length < c.length + 1
⊢ c.length < c.boundaries.card

Tactic:
rw [c.card_boundaries_eq_succ_length]

Premises used: CompositionAsSet.card_boundaries_eq_succ_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.length + 1

Tactic:
Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.length + 1

Tactic:
exact Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : Fin c.length
⊢ (↑i : ℕ) + 1 < c.boundaries.card

Tactic:
lt_tsub_iff_right.mp i.2

Premises used: lt_tsub_iff_right, Fin.isLt, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
i : Fin c.length
⊢ (↑i : ℕ) < c.boundaries.card

Tactic:
lt_of_le_of_lt (Nat.le_succ i) (c.lt_length i)

Premises used: lt_of_le_of_lt, Nat.le_succ, Fin.val, CompositionAsSet.lt_length
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
rw : c.boundaries.min' ⋯ = 0
⊢ Eq (α := Fin (n + 1)) ((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, ⋯⟩ : Fin (n + 1))
    (0 : Fin (n + 1))

Tactic:
rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]

Premises used: CompositionAsSet.card_boundaries_pos, CompositionAsSet.boundary, Finset.orderEmbOfFin_zero, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0

Tactic:
le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)

Premises used: Finset.min'_le, Fin.zero_le, le_antisymm, CompositionAsSet.zero_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0

Tactic:
exact le_antisymm (Finset.min'_le _ _ c.zero_mem) (Fin.zero_le _)

Premises used: Finset.min'_le, Fin.zero_le, le_antisymm, CompositionAsSet.zero_mem
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
⊢ (c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin n.succ) ⟨c.boundaries.card - 1, ⋯⟩ =
    c.boundaries.max' ⋯

Tactic:
Finset.orderEmbOfFin_last rfl c.card_boundaries_pos

Premises used: CompositionAsSet.card_boundaries_pos, Finset.orderEmbOfFin_last, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Composition
Goal:
n : ℕ
c : CompositionAsSet n
h : Fin.last n = c.boundaries.max' ⋯
⊢ (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨c.length, ⋯⟩ = Fin.last n

Tactic:
convert! Finset.orderEmbOfFin_last rfl c.card_boundaries_pos

Premises used: CompositionAsSet.card_boundaries_pos, Finset.orderEmbOfFin_last, rfl