awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
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 : ℕ ≃ ι
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
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have sg : ∀ (n : ℕ), Function.Surjective (g n)
Tactic: 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
-- 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 : ℕ ≃ ι
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)
have neg : ∀ (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i),
  StronglyMeasurable (hs.piecewise (s := s) f)
Tactic: have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
-- 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 : ℕ ≃ ι
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)
have neg : ∀ (n : ℕ) (i : Fin (n + 1)), MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)
Tactic: refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
-- 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 : ℕ ≃ ι
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
neg : ∀ (n : ℕ) (i : Fin (n + 1)), MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg₁ : ∀ (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: refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
-- 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 : ℕ ≃ ι
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))
have neg : 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) : ℕ))) sorry n :
        (a : α) → β)
      x)
  atTop (nhds (f (hs.index (s := s) x) x))
Tactic: simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]
-- 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 : ℕ ≃ ι
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 : α
⊢ ∀ᶠ (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
have obtain : ∀ (y : ℕ) (hy : (e : (a : ℕ) → ι) y = hs.index (s := s) x),
  ∀ᶠ (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
Tactic: obtain ⟨y, hy⟩ := e.bijective.2 (hs.index x)
-- 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 : ℕ ≃ ι
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 : α
y : ℕ
hy : (e : (a : ℕ) → ι) y = hs.index (s := s) x
⊢ ∀ᶠ (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
have refine : ∀ (b : ℕ) (hb : b ≥ y + 1),
  (e : (a : ℕ) → ι) (↑((G b).index (s := fun (k : Fin (b + 1)) ↦ ⋃ i ∈ g b ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x
Tactic: refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
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 : ℕ ≃ ι
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 : α
y : ℕ
hy : (e : (a : ℕ) → ι) y = hs.index (s := s) x
b : ℕ
hb : b ≥ y + 1
⊢ (e : (a : ℕ) → ι) (↑((G b).index (s := fun (k : Fin (b + 1)) ↦ ⋃ i ∈ g b ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x
have this : y = (↑(⟨y, sorry⟩ : Fin (b + 1)) : ℕ)
Tactic: have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
-- 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 : ℕ ≃ ι
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 : α
y : ℕ
hy : (e : (a : ℕ) → ι) y = hs.index (s := s) x
b : ℕ
hb : b ≥ y + 1
this : y = (↑(⟨y, ⋯⟩ : Fin (b + 1)) : ℕ)
⊢ (e : (a : ℕ) → ι) (↑((G b).index (s := fun (k : Fin (b + 1)) ↦ ⋃ i ∈ g b ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x
have rw : Membership.mem (γ := Set α) (⋃ i ∈ g b ⁻¹' {(⟨y, sorry⟩ : Fin (b + 1))}, s i) x
Tactic: rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
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 : ℕ ≃ ι
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 : α
y : ℕ
hy : (e : (a : ℕ) → ι) y = hs.index (s := s) x
b : ℕ
hb : b ≥ y + 1
this : y = (↑(⟨y, ⋯⟩ : Fin (b + 1)) : ℕ)
⊢ Membership.mem (γ := Set α) (⋃ i ∈ g b ⁻¹' {(⟨y, ⋯⟩ : Fin (b + 1))}, s i) x
have this₁ : ∃ m < b, hs.index (s := s) x = (e : (a : ℕ) → ι) m
Tactic: have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
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 : ℕ ≃ ι
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))
have 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
Tactic: 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
-- 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 : ℕ ≃ ι
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
n : ℕ
hn :
  (e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x
⊢ 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 :
      β)
have rw : Eq.{u_3 + 1} (α := β) ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) sorry n : (a : α) → β) x : β)
  ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) sorry n : (a : α) → β) x : β)
Tactic: rw [hn]
-- 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 : ℕ ≃ ι
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
⊢ ∀ᶠ (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 :
        β)
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x_1 : ℕ |
      Membership.mem (γ := Set ℕ)
          {x_2 : ℕ |
            (fun (n : ℕ) ↦
                (e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ) =
                  hs.index (s := s) x)
              x_2}
          x_1 →
        Membership.mem (γ := Set ℕ)
          {x_2 : ℕ |
            (fun (n : ℕ) ↦
                Eq.{u_3 + 1} (α := β)
                  ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) sorry 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) : ℕ)))
                          sorry n :
                        (a : α) → β)
                      x :
                    β))
              x_2}
          x_1}
    a
Tactic: filter_upwards [this] with n hn using by rw [hn]
-- 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 : ℕ ≃ ι
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
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ |
        Membership.mem (γ := Set ℕ)
            {x_2 : ℕ |
              (fun (n : ℕ) ↦
                  (e : (a : ℕ) → ι) (↑((G n).index (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) x) : ℕ) =
                    hs.index (s := s) x)
                x_2}
            x_1 →
          Membership.mem (γ := Set ℕ)
            {x_2 : ℕ |
              (fun (n : ℕ) ↦
                  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 :
                      β))
                x_2}
            x_1}
      a
⊢ ∀ᶠ (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 :
        β)
have h₁ : ∀ (a : ℕ),
  (e : (a : ℕ) → ι) (↑((G a).index (s := fun (k : Fin (a + 1)) ↦ ⋃ i ∈ g a ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x →
    Eq.{u_3 + 1} (α := β) ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) sorry a : (a : α) → β) x : β)
      ((StronglyMeasurable.approx (f :=
              f ((e : (a : ℕ) → ι) (↑((G a).index (s := fun (k : Fin (a + 1)) ↦ ⋃ i ∈ g a ⁻¹' {k}, s i) x) : ℕ))) sorry a :
            (a : α) → β)
          x :
        β)
Tactic: filter_upwards [this] with n hn using by rw [hn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
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 : ℕ ≃ ι
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))
have this₁ : ∀ᶠ (n : ℕ) in atTop,
  Eq.{u_3 + 1} (α := β) ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) sorry 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) : ℕ))) sorry n :
          (a : α) → β)
        x :
      β)
Tactic: 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]
-- 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)
⊢ 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)), 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])