If you write refine' ⟨fun i ↦ ⟨swap g i, _⟩, _, _⟩, then you can move hf_extb as an extra goal from the refine.

I like the other two refactors, but I think that it is clearer if we explicitly name our witness and show how it is constructed. I think it would take longer for someone to go through the proof if they have to make the realization themself that swap g i is the desired extension. One sticking point in the proof for us was also this translation back and forth between functions from alpha to iota to R and functions from alpha to l^infty(iota, R). Here it is clear that we get from a function from alpha to iota to R to one from alpha to l^infty(iota, R) by bundling it with a certificate that it is bound. If we instead leave it as inferred and it pops up as an extra goal I think that is more confusing. Also, with no explicit mention of f_ext the term hf_extb ("hypothesis that f_ext is bounded") would have to be changed and given that I cannot think of a meaningful way to name it I think that that is strong evidence that the way the proof is structured now is fairly natural.

However, I am very new and if I've completely misunderstood this suggestion or there is a general consensus on this type of issue I'm certainly open to the change.

Now that we have replaced all mentions of f_ext with swap g i, I do think we should replace f_ext' with f_ext.

You wouldn't have to choose a new name for hf_extb, since it would just become an extra goal:

    refine' ⟨fun i ↦ ⟨swap g i, _⟩, _, _⟩
    . apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
      use ‖f a₀‖
      rintro - ⟨i, rfl⟩
      simp_rw [←hgeq i ha₀_in_s]
      exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
    · rw [LipschitzWith.coordinate]
      exact hgl
    · intro a hyp
      ext i
      exact (hgeq i) hyp

But I do see what you're saying about how it's nice to make it clear what the extension is, and I'm fine with keeping the current proof structure. I do like renaming f_ext' to f_ext, and using refine' rather than refine:

    let f_ext : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩
    refine' ⟨f_ext, _, _⟩

Ah I see! Thanks for all the helpful comments!