-- Module: Mathlib.MeasureTheory.Function.Piecewise
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)
neg₆ 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) (x : α),
    Tendsto
      (fun (n : ℕ) ↦
        ((fun (n : ℕ) ↦
                ((G n).simpleFunc_piecewise (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) ⋯
                    fun (i : Fin (n + 1)) ↦ StronglyMeasurable.approx (f := f ((e : (a : ℕ) → ι) (↑i : ℕ))) ⋯ n :
                  SimpleFunc α β))
              n :
            (a : α) → β)
          x)
      atTop (nhds (hs.piecewise (s := s) f x))
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) (x : α),
    Tendsto
      (fun (n : ℕ) ↦
        (StronglyMeasurable.approx (f :=
              f ((e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ))) ⋯ n :
            (a : α) → β)
          x)
      atTop (nhds (f (hs.index (s := s) x) x))
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) (x : α)
    (this :
      ∀ᶠ (n : ℕ) in atTop,
        (e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ) =
          hs.index (s := s) x),
    Tendsto
      (fun (n : ℕ) ↦
        (StronglyMeasurable.approx (f :=
              f ((e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ))) ⋯ n :
            (a : α) → β)
          x)
      atTop (nhds (f (hs.index (s := s) x) x))
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) (x : α)
    (this :
      ∀ᶠ (n : ℕ) in atTop,
        (e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ) =
          hs.index (s := s) x)
    (this :
      ∀ᶠ (n : ℕ) in atTop,
        Eq.{u_3 + 1} (α := β) ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) ⋯ n : (a : α) → β) x : β)
          ((StronglyMeasurable.approx (f :=
                  f ((e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ))) ⋯
                  n :
                (a : α) → β)
              x :
            β)),
    Tendsto
      (fun (n : ℕ) ↦
        (StronglyMeasurable.approx (f :=
              f ((e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ))) ⋯ n :
            (a : α) → β)
          x)
      atTop (nhds (f (hs.index (s := s) x) x))
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

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])

Premises used: IndexedPartition.simpleFunc_piecewise, MeasureTheory.SimpleFunc.coe_mk, IndexedPartition.piecewise_apply