-- 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
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, ⋯⟩})
      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)))
    {x : Fin (n - 1) |
      Membership.mem (γ := Finset (Fin n.succ))
        {x : Fin n.succ | (↑x : ℕ) = 0 ∨ (↑x : ℕ) = n ∨ ∃ j ∈ s, (↑x : ℕ) = (↑j : ℕ) + 1} ⟨(↑x : ℕ) + 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']