-- Lean 4 proof step from Mathlib.Combinatorics.Compactness (goal)
Goal:
α : Type u_1
β : α → Type u_2
inst : ∀ (a : α), Finite.{u_2 + 1} (β a)
g : Finset α → (a : α) → β a
let let₁ let₂ : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₃ let₄ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₅ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
      {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
    ∀
      (this :
        ∀ (s : Finset α),
          s.restrict (π := β) ⁻¹'
              {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
            e s),
      ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
let₆ :
  let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
  ∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
    let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
      {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
    ∀
      (this :
        ∀ (s : Finset α),
          s.restrict (π := β) ⁻¹'
              {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
            e s)
      (he' : ∀ (s : Finset α), IsClosed (e s)),
      ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
⊢ ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
have let₇ : let instTop : (a : α) → TopologicalSpace (β a) := fun (a : α) ↦ ⊥;
∀ (instDiscr : ∀ (a : α), DiscreteTopology.{u_2} (β a)),
  let e : (s : Finset α) → Set ((a : α) → β a) := fun (s : Finset α) ↦
    {f : (a : α) → β a | ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, f x = g t x};
  ∀
    (this :
      ∀ (s : Finset α),
        s.restrict (π := β) ⁻¹' {f : (i : ↥s) → β (↑i : α) | ∃ (t : Finset α), s ⊆ t ∧ ∀ (x : ↥s), f x = g t (↑x : α)} =
          e s)
    (he' : ∀ (s : Finset α), IsClosed (e s))
    (he'' : ∀ (B : Finset (Finset α)), Set.Nonempty (α := (a : α) → β a) (⋂ i ∈ B, e i)),
    ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Tactic: classical
  let instTop (a : α) : TopologicalSpace (β a) := ⊥
  have instDiscr (a : α) : DiscreteTopology (β a) := discreteTopology_bot _
  let e (s : Finset α) : Set ((a : α) → β a) := {f | ∃ t, s ⊆ t ∧ ∀ x ∈ s, f x = g t x}
  have (s : Finset α) : s.restrict ⁻¹' {f | ∃ t, s ⊆ t ∧ ∀ x, f x = g t x} = e s := by simp [e]
  have he' (s : Finset α) : IsClosed (e s) := by
    rw [← this]
    exact (isClosed_discrete _).preimage (by fun_prop)
  have he'' (B : Finset (Finset α)) : (⋂ i ∈ B, e i).Nonempty := by
    refine ⟨g (B.biUnion id), ?_⟩
    simp only [Set.mem_iInter, Set.mem_setOf_eq, e]
    intro i hi
    exact ⟨_, subset_biUnion_of_mem id hi, by simp⟩
  simpa using CompactSpace.iInter_nonempty he' he''