-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
neg neg₁ neg₂ : StronglyMeasurable (hs.piecewise (s := s) f)
neg₃ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n)), StronglyMeasurable (hs.piecewise (s := s) f)
neg₄ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
    (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i),
    StronglyMeasurable (hs.piecewise (s := s) f)
neg₅ :
  let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n;
  ∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
    (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) (n : ℕ) (i : Fin (n + 1)),
    MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg₆ : let g : (n : ℕ) → (i : ι) → Fin (n + 1) := fun (n : ℕ) (i : ι) ↦
  if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), sorry⟩
  else Fin.last n;
∀ (sg : ∀ (n : ℕ), Function.Surjective (g n))
  (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) (x : α),
  Tendsto
    (fun (n : ℕ) ↦
      ((fun (n : ℕ) ↦
              ((G n).simpleFunc_piecewise (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) sorry
                  fun (i : Fin (n + 1)) ↦ StronglyMeasurable.approx (f := f ((e : (a : ℕ) → ι) (↑i : ℕ))) sorry n :
                SimpleFunc α β))
            n :
          (a : α) → β)
        x)
    atTop (nhds (hs.piecewise (s := s) f x))
Tactic: classical
  let g (n : ℕ) (i : ι) : Fin (n + 1) :=
    if hi : ∃ m < n, i = e m then ⟨hi.choose, by grind⟩ else Fin.last n
  have sg (n : ℕ) : (g n).Surjective := by
    intro b
    unfold g
    refine ⟨e b, ?_⟩
    by_cases hb : b < n
    · have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using e.injective this.choose_spec.2.symm
    · simp [hb]
      grind
  have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
  refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
  · exact .biUnion (to_countable _) fun _ _ ↦ hm _
  simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]
  have : ∀ᶠ n in atTop, e ((G n).index x) = hs.index x := by
    obtain ⟨y, hy⟩ := e.bijective.2 (hs.index x)
    refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩
    have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
    rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]
    have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
    simpa [g, hs.mem_iff_index_eq, this] using e.injective (hy.trans this.choose_spec.2).symm
  have : ∀ᶠ n in atTop, (hf (hs.index x)).approx n x = (hf (e ((G n).index x))).approx n x := by
    filter_upwards [this] with n hn using by rw [hn]
  exact (Filter.tendsto_congr' this).mp (by simp [StronglyMeasurable.tendsto_approx])