awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
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
have this : (↑i : ℕ) + 1 ≠ n
Tactic: have : (i : ℕ) + 1 ≠ n := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
⊢ 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
have h : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : 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})
          (⟨1 + (↑i : ℕ), sorry⟩ : Fin n.succ)})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
h h₁ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ)})
      i ↔
    i ∈ s
⊢ 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
have h₂ : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : 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})
          ⟨(↑i : ℕ) + 1, sorry⟩})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
h h₁ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ)})
      i ↔
    i ∈ s
h₂ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
⊢ 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
have h₃ : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : 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})
          ⟨(↑i : ℕ) + 1, sorry⟩})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
h h₁ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ)})
      i ↔
    i ∈ s
h₂ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₃ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
⊢ 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
have h₄ : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : 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})
          ⟨(↑i : ℕ) + 1, sorry⟩})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
h h₁ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ)})
      i ↔
    i ∈ s
h₂ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₃ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₄ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
⊢ 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
have h₅ : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : Fin (n - 1) |
        Membership.mem (γ := Finset (Fin n.succ))
          (Set.toFinset
            {i : Fin n.succ | (↑i : ℕ) = 0 ∨ (↑i : ℕ) = n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1})
          ⟨(↑i : ℕ) + 1, sorry⟩})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n_1 n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : (↑i : ℕ) + 1 ≠ n
h h₁ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            (⟨1 + (↑i : ℕ), ⋯⟩ : Fin n.succ)})
      i ↔
    i ∈ s
h₂ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₃ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₄ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : 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})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
h₅ :
  Membership.mem (γ := Finset (Fin (n - 1)))
      (Set.toFinset
        {i : Fin (n - 1) |
          Membership.mem (γ := Finset (Fin n.succ))
            (Set.toFinset
              {i : Fin n.succ | (↑i : ℕ) = 0 ∨ (↑i : ℕ) = n ∨ ∃ (j : Fin (n - 1)) (_ : j ∈ s), (↑i : ℕ) = (↑j : ℕ) + 1})
            ⟨(↑i : ℕ) + 1, ⋯⟩})
      i ↔
    i ∈ s
⊢ 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
have h₆ : Membership.mem (γ := Finset (Fin (n - 1)))
    (Set.toFinset
      {i : Fin (n - 1) |
        Membership.mem (γ := Finset (Fin n.succ))
          (Set.toFinset {i : Fin n.succ | (↑i : ℕ) = 0 ∨ (↑i : ℕ) = n ∨ ∃ j ∈ s, (↑i : ℕ) = (↑j : ℕ) + 1})
          ⟨(↑i : ℕ) + 1, sorry⟩})
    i ↔
  i ∈ s
Tactic: simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_setOf,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
⊢ Fintype.card (CompositionAsSet n) = HPow.hPow (α := ℕ) 2 (n - 1)
have this : Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = HPow.hPow (α := ℕ) 2 (n - 1)
⊢ Fintype.card (CompositionAsSet n) = HPow.hPow (α := ℕ) 2 (n - 1)
have rw : Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.boundaries.card
have rw : c.length < c.length + 1
Tactic: rw [c.card_boundaries_eq_succ_length]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
⊢ Eq (α := Fin (n + 1)) ((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, ⋯⟩ : Fin (n + 1))
    (0 : Fin (n + 1))
have rw : c.boundaries.min' sorry = 0
Tactic: rw [boundary, Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
⊢ (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨c.length, ⋯⟩ = Fin.last n
have h : Fin.last n = c.boundaries.max' sorry
Tactic: convert! Finset.orderEmbOfFin_last rfl c.card_boundaries_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
⊢ i < c.blocks.length
have h₁ : i + 1 < c.length + 1
Tactic: rw [c.card_boundaries_eq_succ_length] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
have A : i < c.blocks.length
Tactic: have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
have B : i < c.boundaries.card
Tactic: have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
IH :
  ∀ (h : i < c.boundaries.card),
    (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
have succ : (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨i, B⟩ : Fin c.boundaries.card)) : ℕ) +
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) c.blocks i A =
  (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
Tactic: rw [sum_take_succ _ _ A, IH B]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < c.boundaries.card
⊢ (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
have zero : ∀ (h : 0 < c.boundaries.card),
  (take 0 c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, h⟩) : ℕ)
Tactic: induction i with
  | zero => simp
  | succ i IH =>
    have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
    have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
    rw [sum_take_succ _ _ A, IH B]
    simp [blocks, blocksFun]
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
i : ℕ
h : i < c.boundaries.card
zero :
  ∀ (h : 0 < c.boundaries.card),
    (take 0 c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨0, h⟩) : ℕ)
⊢ (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ)
have succ : ∀ (i : ℕ)
  (IH :
    ∀ (h : i < c.boundaries.card),
      (take i c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, h⟩) : ℕ))
  (h : i + 1 < c.boundaries.card),
  (take (i + 1) c.blocks).sum = (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i + 1, h⟩) : ℕ)
Tactic: induction i with
  | zero => simp
  | succ i IH =>
    have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]
    have B : i < c.boundaries.card := lt_of_lt_of_le A (by simp [blocks, length])
    rw [sum_take_succ _ _ A, IH B]
    simp [blocks, blocksFun]
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
have mp : j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
mp : j ∈ c.boundaries → ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
have mpr : (∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)) → j ∈ c.boundaries
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
have mp : ∀ (i : Fin c.boundaries.card)
  (hi :
    (c.boundaries.orderIsoOfFin sorry : (a : Fin c.boundaries.card) → ↥c.boundaries) i =
      Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj),
  ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
Tactic: rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi :
  (c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i =
    Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
have hi₁ : (↑((c.boundaries.orderIsoOfFin sorry : (a : Fin c.boundaries.card) → ↥c.boundaries) i) : Fin n.succ) =
  (↑(Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj) : Fin n.succ)
Tactic: rw [Subtype.ext_iff, Subtype.coe_mk] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi :
  (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) i) : Fin n.succ) =
    (↑(Subtype.mk (p := fun (x : Fin n.succ) ↦ x ∈ c.boundaries) j hj) : Fin n.succ)
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = (↑j : ℕ)
have mp : (take (↑i : ℕ) c.blocks).sum = (↑j : ℕ)
Tactic: refine ⟨i.1, i.2, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯ : (a : Fin c.boundaries.card) → Fin (n + 1)) i = j
⊢ (take (↑i : ℕ) c.blocks).sum = (↑j : ℕ)
have mp : (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨(↑i : ℕ), sorry⟩ : Fin c.boundaries.card)) : ℕ) =
  (↑((c.boundaries.orderEmbOfFin sorry : (a : Fin c.boundaries.card) → Fin (n + 1)) i) : ℕ)
Tactic: rw [← hi, c.blocks_partial_sum i.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
⊢ j ∈ c.boundaries
have h : j = (↑((c.boundaries.orderIsoOfFin sorry : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ)
Tactic: convert! (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
⊢ (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j
have rwa : (↑((c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) (⟨i, hi⟩ : Fin c.boundaries.card)) : ℕ) = (↑j : ℕ)
Tactic: rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = (↑j : ℕ)
⊢ j = (↑((c.boundaries.orderIsoOfFin ⋯ : (a : Fin c.boundaries.card) → ↥c.boundaries) ⟨i, hi⟩) : Fin n.succ)
have this : (c.boundary : (a : Fin c.boundaries.card) → Fin (n + 1)) ⟨i, hi⟩ = j
Tactic: have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (hypothesis)
Goal:
n : ℕ
c : CompositionAsSet n
⊢ c.blocks.sum = n
have this : take c.length c.blocks = c.blocks
Tactic: have : c.blocks.take c.length = c.blocks := take_of_length_le (by simp [blocks])
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Composition (goal)
Goal:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ c.blocks.sum = n
have rw : (↑(Fin.last n) : ℕ) = n
Tactic: rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]