-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
hn :
  ∀ m ≤ n,
    ∀ (i : @cell _ t C D _ m),
      ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell (C := C) (D := D) m_1 j
i : @cell _ t C D _ (n + 1)
hi :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
hi₁ :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j)
    (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
    (hp :
      ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
hi₂ :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j)
    (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
    (hp :
      ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
h :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j)
    (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
    (hp :
      ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
    let I : (m : ℕ) → Finset (@cell _ t C D _ m) := fun (m : ℕ) ↦
      J m ∪
        (Finset.range n.succ).biUnion fun (l : ℕ) ↦
          (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅;
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
h₁ :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j)
    (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
    (hp :
      ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
    let I : (m : ℕ) → Finset (@cell _ t C D _ m) := fun (m : ℕ) ↦
      J m ∪
        (Finset.range n.succ).biUnion fun (l : ℕ) ↦
          (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅;
    ∀ ⦃x : X⦄ (hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i),
      x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
have h₂ : ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
  (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
  (hp :
    ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
      cellFrontier (C := C) (D := D) m i ⊆
        D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
  let I : (m : ℕ) → Finset (@cell _ t C D _ m) := fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅;
  ∀ ⦃x : X⦄ (hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i)
    (hJ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j),
    x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
Tactic: classical
    obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i
    choose p hp using hn
    let I m := J m ∪ ((Finset.range n.succ).biUnion
      (fun l ↦ (J l).biUnion (fun y ↦ if h : l ≤ n then p l h y m else ∅)))
    use I
    intro x hx
    specialize hJ hx
    simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢
    rcases hJ with hJ | hJ
    · exact .inl hJ
    obtain ⟨l, hln, j, hj, hxj⟩ := hJ
    rw [← cellFrontier_union_openCell_eq_closedCell] at hxj
    rcases hxj with hxj | hxj
    · specialize hp l (Nat.le_of_lt_succ hln) j hxj
      simp_rw [mem_union, mem_iUnion, exists_prop] at hp
      refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
      simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
      exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩
    · right
      use l, hln, j
      simp only [Nat.succ_eq_add_one, Finset.mem_union, I]
      exact ⟨Or.intro_left _ hj, hxj⟩
Cleared hypotheses: hn