awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ LT.lt (α := ℕ) (∑ k : Fin c.length, c.blocksFun k) (∑ k : Fin c.length, c.blocksFun k)
have k : ∑ k : Fin c.length, c.blocksFun k ≤ c.blocksFun i
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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ c.length = 1
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn ≍ c
have subst : ∀ (c : Composition n), c.cast sorry ≍ c
Tactic: subst m
Cleared hypotheses: m, c, hmn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn = cast ⋯ c
have subst : ∀ (c : Composition n), c.cast sorry = cast sorry c
Tactic: subst m
Cleared hypotheses: m, c, hmn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
i : ℕ
hi : i ∈ c₁.blocks ++ c₂.blocks
⊢ 0 < i
have hi₁ : i ∈ c₁.blocks ∨ i ∈ c₂.blocks
Tactic: rw [mem_append] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
⊢ (ones n).reverse = ones n
have blocks : (ones n).reverse.blocks = (ones n).blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ (single n hn).reverse = single n hn
have blocks : (single n hn).reverse.blocks = (single n hn).blocks
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ motive (k + 1 + n) ((single (k + 1) ⋯).append c).reverse
have h : k + 1 + n = n + (k + 1)
Tactic: convert! append_single k n c.reverse ih using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ motive (k + 1 + n) ((single (k + 1) ⋯).append c).reverse
have h₁ : k + 1 + n = n + (k + 1) → ((single (k + 1) sorry).append c).reverse ≍ c.reverse.append (single (k + 1) sorry)
Tactic: convert! append_single k n c.reverse ih using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)
have h : (c.reverse.append (single (k + 1) sorry)).cast sorry ≍ c.reverse.append (single (k + 1) sorry)
Tactic: rw [reverse_append, reverse_single]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
l : List α
ns : List ℕ
⊢ (l.splitWrtCompositionAux ns).length = ns.length
have nil : ∀ (l : List α), (l.splitWrtCompositionAux []).length = length (α := ℕ) []
Tactic: induction ns generalizing l
Cleared hypotheses: l, ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
l : List α
ns : List ℕ
nil : ∀ (l : List α), (l.splitWrtCompositionAux []).length = length (α := ℕ) []
⊢ (l.splitWrtCompositionAux ns).length = ns.length
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (l : List α), (l.splitWrtCompositionAux tail).length = tail.length) →
    ∀ (l : List α), (l.splitWrtCompositionAux (head :: tail)).length = (head :: tail).length
Tactic: induction ns generalizing l
Cleared hypotheses: l, ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
have nil : ∀ {l : List α}, sum [] ≤ l.length → map length (l.splitWrtCompositionAux []) = []
Tactic: induction ns with
  | nil => simp [splitWrtCompositionAux]
  | cons n ns IH => grind [splitWrtCompositionAux_cons]
Cleared hypotheses: ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
ns : List ℕ
nil : ∀ {l : List α}, sum [] ≤ l.length → map length (l.splitWrtCompositionAux []) = []
⊢ ∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns
have 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
Tactic: induction ns with
  | nil => simp [splitWrtCompositionAux]
  | cons n ns IH => grind [splitWrtCompositionAux_cons]
Cleared hypotheses: ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
⊢ 0 < l'.length
have this : l'.length ∈ map length (l.splitWrtComposition c)
Tactic: have : l'.length ∈ (l.splitWrtComposition c).map List.length :=
    List.mem_map_of_mem h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ map length (l.splitWrtComposition c)
⊢ 0 < l'.length
have this₁ : l'.length ∈ c.blocks
Tactic: rw [map_length_splitWrtComposition] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i
have e_a : map length (l.splitWrtComposition c) = c.blocks
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ 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)
have 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)
Tactic: rcases i with - | i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ 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)
have 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)
Tactic: rcases i with - | i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ 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)
have 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)
Tactic: simp only [splitWrtCompositionAux, getElem_cons_succ, IH, take,
          sum_cons, splitAt_eq, drop_take, drop_drop]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ 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)
have 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)
Tactic: rw [Nat.add_sub_add_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
l : List α
ns : 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)
have 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)
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]
Cleared hypotheses: l, ns, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ 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)
have 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)
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]
Cleared hypotheses: l, ns, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
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
⊢ (l.splitWrtCompositionAux (n :: ns)).flatten = l
have h₁ : n + ns.sum = l.length
Tactic: rw [sum_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ (l.splitWrtCompositionAux (n :: ns)).flatten = l
have cons : (take n l :: (drop n l).splitWrtCompositionAux ns).flatten = l
Tactic: simp only [splitWrtCompositionAux_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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).splitWrtCompositionAux ns).flatten = l
have cons : take n l ++ drop n l = l
Tactic: rw [IH]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ take n l ++ ((drop n l).splitWrtCompositionAux ns).flatten = l
have cons₁ : ns.sum = (drop n l).length
Tactic: rw [IH]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ ns.sum = (drop n l).length
have cons : ns.sum = l.length - n
Tactic: rw [length_drop, ← h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ ns.sum = (drop n l).length
have cons₁ : ns.sum = n + ns.sum - n
Tactic: rw [length_drop, ← h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ ns.sum = (drop n l).length
have cons₂ : ns.sum = ns.sum
Tactic: rw [length_drop, ← h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
ns : List ℕ
⊢ ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
have nil : ∀ {l : List α}, sum [] = l.length → (l.splitWrtCompositionAux []).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]
Cleared hypotheses: ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
α : Type u_1
ns : List ℕ
nil : ∀ {l : List α}, sum [] = l.length → (l.splitWrtCompositionAux []).flatten = l
⊢ ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
have 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
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]
Cleared hypotheses: ns
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
⊢ (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
have 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 := sorry, getLast_mem := sorry : CompositionAsSet n })
          ((fun (c : CompositionAsSet n) ↦
              (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), sorry⟩ : Fin n.succ) ∈ c.boundaries} : Finset (Fin (n - 1))))
            c)))
      i ↔
    i ∈ c.boundaries
Tactic: ext i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
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
have boundaries : (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, sorry⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) ↔
  i ∈ c.boundaries
Tactic: simp only [add_comm, Set.toFinset_setOf, Finset.mem_univ,
     Finset.mem_filter, true_and, exists_prop]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) ↔
    i ∈ c.boundaries
have boundaries : (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, sorry⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) →
  i ∈ c.boundaries
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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
⊢ (i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1) ↔
    i ∈ c.boundaries
have boundaries₁ : i ∈ c.boundaries →
  i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, sorry⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries →
    i = 0 ∨ i = Fin.last n ∨ ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1
have boundaries : i ∈ c.boundaries →
  (∃ (y : Fin n), y.succ = i) →
    i ≠ Fin.last n → ∃ (j : Fin (n - 1)), ⟨(↑j : ℕ) + 1, sorry⟩ ∈ c.boundaries ∧ (↑i : ℕ) = (↑j : ℕ) + 1
Tactic: simp only [or_iff_not_imp_left, ← ne_eq, ← Fin.exists_succ_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
c : CompositionAsSet n
j : Fin n
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last n
⊢ ∃ (j_1 : Fin (n - 1)), ⟨(↑j_1 : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1
have 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, sorry⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1
Tactic: rcases Nat.exists_add_one_eq.mpr j.pos with ⟨n, rfl⟩
Cleared hypotheses: n, c, j, i_mem, i_ne_last
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ ∃ (j_1 : Fin (n + 1 - 1)), ⟨(↑j_1 : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑j.succ : ℕ) = (↑j_1 : ℕ) + 1
have 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, sorry⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑j : ℕ) + 1
Tactic: obtain ⟨k, rfl⟩ : ∃ k : Fin n, k.castSucc = j := by
        simpa [Fin.exists_castSucc_eq] using i_ne_last
Cleared hypotheses: j, i_mem, i_ne_last
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
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)
⊢ ∃ (j : Fin (n + 1 - 1)), ⟨(↑j : ℕ) + 1, ⋯⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑j : ℕ) + 1
have h : ⟨(↑k : ℕ) + 1, sorry⟩ ∈ c.boundaries ∧ (↑k.castSucc.succ : ℕ) = (↑k : ℕ) + 1
Tactic: use k
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : 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) =
    s
have h : ∀ (i : Fin (n - 1)),
  Membership.mem (γ := Finset (Fin (n - 1)))
      ((fun (c : CompositionAsSet n) ↦
          (Set.toFinset {i : Fin (n - 1) | (⟨1 + (↑i : ℕ), sorry⟩ : 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 := sorry, getLast_mem := sorry : CompositionAsSet n })
          s))
      i ↔
    i ∈ s
Tactic: ext i